Cryptographic Boolean Functions in Lean

5.2. The dual🔗

Definition5.2.1
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 1.7.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 12
Reverse dependency previews
Preview
Theorem 5.2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6dualitysection-6-1page-79fidelity-exact

Bent dual (Carlet, Section 6.1, p. 79). Let n be even and let f:V_n\to\mathbb F_2 be bent. Its dual is the unique Boolean function \widetilde f:V_n\to\mathbb F_2 satisfying W_f(u)=2^{n/2}(-1)^{\widetilde f(u)} \qquad(u\in V_n). The function \widetilde f is bent and satisfies W_{\widetilde f}(a)=2^{n/2}(-1)^{f(a)}, \qquad \widetilde{\widetilde f}=f.

Lean code for Definition5.2.1●6 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/Dual.lean
    complete
    def CryptBoolean.bentDual {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.bentDual {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.BooleanFunction n
    The bit-valued dual selected by the sign of the raw Walsh coefficient.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Dual.lean
    complete
    theorem CryptBoolean.walshTransform_eq_two_pow_half_mul_bitSignInt_bentDual
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) (a : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f a =
    2 ^ (n / 2) * CryptBoolean.bitSignInt (CryptBoolean.bentDual f a)
    theorem CryptBoolean.walshTransform_eq_two_pow_half_mul_bitSignInt_bentDual
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (a : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f a =
    2 ^ (n / 2) *
      CryptBoolean.bitSignInt
        (CryptBoolean.bentDual f a)
    For a bent function, the raw Walsh coefficient is its dual sign scaled by
`2^(n/2)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Dual.lean
    complete
    theorem CryptBoolean.realSignView_bentDual {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f) :
  CryptBoolean.realSignView (CryptBoolean.bentDual f) =
    FABL.bentDual (CryptBoolean.realSignView f)
    theorem CryptBoolean.realSignView_bentDual {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) :
  CryptBoolean.realSignView
      (CryptBoolean.bentDual f) =
    FABL.bentDual
      (CryptBoolean.realSignView f)
    The real sign view of Carlet's bit-valued dual is FABL's normalized
Fourier dual.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Dual.lean
    complete
    theorem CryptBoolean.isBent_bentDual {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f) :
  CryptBoolean.IsBent (CryptBoolean.bentDual f)
    theorem CryptBoolean.isBent_bentDual {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) :
  CryptBoolean.IsBent
    (CryptBoolean.bentDual f)
    The dual of a bent Boolean function is bent.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Dual.lean
    complete
    theorem CryptBoolean.walshTransform_bentDual {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (a : FABL.F₂Cube n) :
  CryptBoolean.walshTransform (CryptBoolean.bentDual f) a =
    2 ^ (n / 2) * CryptBoolean.bitSignInt (f a)
    theorem CryptBoolean.walshTransform_bentDual
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (a : FABL.F₂Cube n) :
  CryptBoolean.walshTransform
      (CryptBoolean.bentDual f) a =
    2 ^ (n / 2) *
      CryptBoolean.bitSignInt (f a)
    The raw Walsh transform of the dual recovers the original sign.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Dual.lean
    complete
    theorem CryptBoolean.bentDual_bentDual {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f) :
  CryptBoolean.bentDual (CryptBoolean.bentDual f) = f
    theorem CryptBoolean.bentDual_bentDual {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) :
  CryptBoolean.bentDual
      (CryptBoolean.bentDual f) =
    f
    Duality is an involution on bent Boolean functions.
Theorem5.2.2
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 1.4.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-6dualityrelation-44page-79fidelity-exact

Relation (44) (Carlet, p. 79). If f,g:V_n\to\mathbb F_2 are bent, then W_{\widetilde f+\widetilde g}(0)=W_{f+g}(0). Consequently, d_H(\widetilde f,\widetilde g)=d_H(f,g), so duality preserves pairwise Hamming distance on bent functions.

Lean code for Theorem5.2.2●2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualIsometry.lean
    complete
    theorem CryptBoolean.walshTransform_zero_bentDual_add {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (hg : CryptBoolean.IsBent g) :
  CryptBoolean.walshTransform
      (CryptBoolean.bentDual f + CryptBoolean.bentDual g) 0 =
    CryptBoolean.walshTransform (f + g) 0
    theorem CryptBoolean.walshTransform_zero_bentDual_add
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (hg : CryptBoolean.IsBent g) :
  CryptBoolean.walshTransform
      (CryptBoolean.bentDual f +
        CryptBoolean.bentDual g)
      0 =
    CryptBoolean.walshTransform (f + g) 0
    Carlet Relation (44): the imbalance of the sum of two bent duals equals
the imbalance of the original sum.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualIsometry.lean
    complete
    theorem CryptBoolean.hammingDistance_bentDual {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (hg : CryptBoolean.IsBent g) :
  CryptBoolean.hammingDistance (CryptBoolean.bentDual f)
      (CryptBoolean.bentDual g) =
    CryptBoolean.hammingDistance f g
    theorem CryptBoolean.hammingDistance_bentDual
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (hg : CryptBoolean.IsBent g) :
  CryptBoolean.hammingDistance
      (CryptBoolean.bentDual f)
      (CryptBoolean.bentDual g) =
    CryptBoolean.hammingDistance f g
    Bent duality preserves Hamming distance.
Theorem5.2.3
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Proposition 1.8.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6dualityrelation-45pages-79-80fidelity-exact

Relation (45) (Carlet, pp. 79--80). Let f:V_n\to\mathbb F_2 be bent and let a,b\in V_n. The function g(x)=f(x+b)+a\mathbin\cdot x is bent, and its dual is \widetilde g(x)=\widetilde f(x+a)+b\mathbin\cdot(x+a). Writing \ell_c(x)=c\mathbin\cdot x, one has W_{D_a\widetilde f+\ell_b}(0) =W_{D_bf+\ell_a}(0).

Lean code for Theorem5.2.3●5 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualAffine.lean
    complete
    theorem CryptBoolean.isBent_domainTranslate {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (b : FABL.F₂Cube n) : CryptBoolean.IsBent (FABL.domainTranslate f b)
    theorem CryptBoolean.isBent_domainTranslate
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (b : FABL.F₂Cube n) :
  CryptBoolean.IsBent
    (FABL.domainTranslate f b)
    Translating the input of a bent Boolean function preserves bentness.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualAffine.lean
    complete
    theorem CryptBoolean.isBent_domainTranslate_add_linear {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (b a : FABL.F₂Cube n) :
  CryptBoolean.IsBent
    (FABL.domainTranslate f b + FABL.affineFunction 0 a)
    theorem CryptBoolean.isBent_domainTranslate_add_linear
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (b a : FABL.F₂Cube n) :
  CryptBoolean.IsBent
    (FABL.domainTranslate f b +
      FABL.affineFunction 0 a)
    Translating a bent function and adding a linear function preserves bentness.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualAffine.lean
    complete
    theorem CryptBoolean.bentDual_domainTranslate_add_linear {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (b a x : FABL.F₂Cube n) :
  CryptBoolean.bentDual
      (FABL.domainTranslate f b + FABL.affineFunction 0 a) x =
    CryptBoolean.bentDual f (x + a) + FABL.f₂DotProduct b (x + a)
    theorem CryptBoolean.bentDual_domainTranslate_add_linear
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (b a x : FABL.F₂Cube n) :
  CryptBoolean.bentDual
      (FABL.domainTranslate f b +
        FABL.affineFunction 0 a)
      x =
    CryptBoolean.bentDual f (x + a) +
      FABL.f₂DotProduct b (x + a)
    Carlet's affine action on bent duals.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualAffine.lean
    complete
    theorem CryptBoolean.bentDual_add_constant {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (c : FABL.𝔽₂) (a : FABL.F₂Cube n) :
  CryptBoolean.bentDual (f + FABL.affineFunction c 0) a =
    CryptBoolean.bentDual f a + c
    theorem CryptBoolean.bentDual_add_constant {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (c : FABL.𝔽₂) (a : FABL.F₂Cube n) :
  CryptBoolean.bentDual
      (f + FABL.affineFunction c 0) a =
    CryptBoolean.bentDual f a + c
    Adding a constant to a bent function adds the same constant to its dual.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualAffine.lean
    complete
    theorem CryptBoolean.walshTransform_zero_bentDual_derivative_add_linear {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (a b : FABL.F₂Cube n) :
  CryptBoolean.walshTransform
      (FABL.booleanDerivative (CryptBoolean.bentDual f) a +
        FABL.affineFunction 0 b)
      0 =
    CryptBoolean.walshTransform
      (FABL.booleanDerivative f b + FABL.affineFunction 0 a) 0
    theorem CryptBoolean.walshTransform_zero_bentDual_derivative_add_linear
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (a b : FABL.F₂Cube n) :
  CryptBoolean.walshTransform
      (FABL.booleanDerivative
          (CryptBoolean.bentDual f) a +
        FABL.affineFunction 0 b)
      0 =
    CryptBoolean.walshTransform
      (FABL.booleanDerivative f b +
        FABL.affineFunction 0 a)
      0
    Carlet Relation (45): the two derivative-linear sums have equal imbalance.
Theorem5.2.4
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.6.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Proposition 5.2.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6dualitynumerical-normal-formpages-79-80fidelity-exact

Numerical normal form of the dual (Carlet, pp. 79--80). Let f:V_n\to\mathbb F_2 be bent, and write its numerical normal form as f(x)=\sum_{S\subseteq[n]}\lambda_Sx^S. If \delta_0(x) is one at x=0 and zero elsewhere, then \widetilde f(x) =\frac12-\frac{2^{n/2}}2\,\delta_0(x) +\frac{(-1)^{w_H(x)}}{2^{n/2}} \sum_{\operatorname{supp}(x)\subseteq S} 2^{n-|S|}\lambda_S. This identity determines the numerical normal form of \widetilde f.

Lean code for Theorem5.2.4●2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualNNF.lean
    complete
    theorem CryptBoolean.booleanRealEmbedding_bentDual_eq_rawFourierTransform
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding (CryptBoolean.bentDual f) x =
    (1 / 2 - if x = 0 then 2 ^ (n / 2) / 2 else 0) +
      CryptBoolean.rawFourierTransform (FABL.booleanRealEmbedding f) x /
        2 ^ (n / 2)
    theorem CryptBoolean.booleanRealEmbedding_bentDual_eq_rawFourierTransform
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding
      (CryptBoolean.bentDual f) x =
    (1 / 2 -
        if x = 0 then 2 ^ (n / 2) / 2
        else 0) +
      CryptBoolean.rawFourierTransform
          (FABL.booleanRealEmbedding f)
          x /
        2 ^ (n / 2)
    The zero-one embedding of the dual is an affine rescaling of the raw
Fourier transform of the zero-one embedding of the original bent function.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualNNF.lean
    complete
    theorem CryptBoolean.booleanRealEmbedding_bentDual_eq_numericalCoeff_sum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding (CryptBoolean.bentDual f) x =
    (1 / 2 - if x = 0 then 2 ^ (n / 2) / 2 else 0) +
      ((-1) ^ (FABL.f₂Support x).card *
          ∑ S with FABL.f₂Support x ⊆ S,
            2 ^ (n - S.card) *
              FABL.numericalCoeff (FABL.booleanRealEmbedding f) S) /
        2 ^ (n / 2)
    theorem CryptBoolean.booleanRealEmbedding_bentDual_eq_numericalCoeff_sum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding
      (CryptBoolean.bentDual f) x =
    (1 / 2 -
        if x = 0 then 2 ^ (n / 2) / 2
        else 0) +
      ((-1) ^ (FABL.f₂Support x).card *
          ∑ S with FABL.f₂Support x ⊆ S,
            2 ^ (n - S.card) *
              FABL.numericalCoeff
                (FABL.booleanRealEmbedding
                  f)
                S) /
        2 ^ (n / 2)
    Carlet's dual-NNF relation in the canonical coefficient notation.
Proposition5.2.5
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Proposition 1.6.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Corollary 5.2.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6dualitynumerical-normal-formproposition-17page-80fidelity-exact

Proposition 17 (Carlet, p. 80). Let f:V_n\to\mathbb F_2 be bent, where n is even, and let \lambda_I and \widetilde\lambda_I be the integer numerical-normal-form coefficients of f and \widetilde f. For every proper subset I\subsetneq[n] with |I|>n/2, 2^{|I|-n/2}\mid\lambda_I, \qquad 2^{|I|-n/2}\mid\widetilde\lambda_I.

Lean code for Proposition5.2.5●1 theorem
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualCoefficientDivisibility.lean
    complete
    theorem CryptBoolean.bentDual_and_self_nnfCoefficient_divisibility {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (I : Finset (Fin n)) (hI : I ≠ Finset.univ)
  (hIhalf : n / 2 < I.card) :
  2 ^ (I.card - n / 2) ∣
      FABL.booleanNumericalCoeffInt (CryptBoolean.bentDual f) I ∧
    2 ^ (I.card - n / 2) ∣ FABL.booleanNumericalCoeffInt f I
    theorem CryptBoolean.bentDual_and_self_nnfCoefficient_divisibility
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (I : Finset (Fin n))
  (hI : I ≠ Finset.univ)
  (hIhalf : n / 2 < I.card) :
  2 ^ (I.card - n / 2) ∣
      FABL.booleanNumericalCoeffInt
        (CryptBoolean.bentDual f) I ∧
    2 ^ (I.card - n / 2) ∣
      FABL.booleanNumericalCoeffInt f I
    Carlet Proposition 17: away from the top monomial, every NNF
coefficient above half dimension has the stated power-of-two divisor, for
both a bent function and its dual.
Corollary5.2.6
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6dualityalgebraic-normal-formpage-81fidelity-exact-with-dual-symmetry

Complementary half-degree ANF coefficients (Carlet, p. 81). Let n\ge4, let f:V_n\to\mathbb F_2 be bent, and let c_{f,I} denote the coefficient of x^I in the ANF of f. For every I\subseteq[n] with |I|=n/2, c_{\widetilde f,I}=c_{f,[n]\setminus I}, \qquad c_{f,I}=c_{\widetilde f,[n]\setminus I}.

Lean code for Corollary5.2.6●2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualCoefficientDivisibility.lean
    complete
    theorem CryptBoolean.anfCoeff_bentDual_eq_complement_of_card_eq_half {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (hn : 4 ≤ n) (I : Finset (Fin n)) (hIcard : I.card = n / 2) :
  FABL.anfCoeff (CryptBoolean.bentDual f) I =
    FABL.anfCoeff f (Finset.univ \ I)
    theorem CryptBoolean.anfCoeff_bentDual_eq_complement_of_card_eq_half
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (hn : 4 ≤ n) (I : Finset (Fin n))
  (hIcard : I.card = n / 2) :
  FABL.anfCoeff (CryptBoolean.bentDual f)
      I =
    FABL.anfCoeff f (Finset.univ \ I)
    For a bent function in dimension at least four, the half-degree ANF
coefficient of the dual is the coefficient of the complementary monomial of
the original function.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualCoefficientDivisibility.lean
    complete
    theorem CryptBoolean.anfCoeff_eq_bentDual_complement_of_card_eq_half {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (hn : 4 ≤ n) (I : Finset (Fin n)) (hIcard : I.card = n / 2) :
  FABL.anfCoeff f I =
    FABL.anfCoeff (CryptBoolean.bentDual f) (Finset.univ \ I)
    theorem CryptBoolean.anfCoeff_eq_bentDual_complement_of_card_eq_half
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (hn : 4 ≤ n) (I : Finset (Fin n))
  (hIcard : I.card = n / 2) :
  FABL.anfCoeff f I =
    FABL.anfCoeff
      (CryptBoolean.bentDual f)
      (Finset.univ \ I)
    The complementary half-degree ANF coefficient relation is symmetric
between a bent function and its dual.
Theorem5.2.7
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Corollary 1.8.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Proposition 5.4.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6dualitypoisson-summationrelation-46page-81fidelity-exact

Relation (46) (Carlet, p. 81). Let f:V_n\to\mathbb F_2 be bent, let E\le V_n, and let a,b\in V_n. Then \sum_{x\in a+E}(-1)^{\widetilde f(x)+b\mathbin\cdot x} =2^{-n/2}|E|(-1)^{a\mathbin\cdot b} \sum_{x\in b+E^\perp}(-1)^{f(x)+a\mathbin\cdot x}.

Lean code for Theorem5.2.7●1 theorem
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DualPoisson.lean
    complete
    theorem CryptBoolean.bentDual_poissonSummationFormula {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a b : FABL.F₂Cube n) :
  ∑ u,
      CryptBoolean.realSignView (CryptBoolean.bentDual f) (a + ↑u) *
        (FABL.vectorWalshCharacter b) (a + ↑u) =
    (2 ^ (n / 2))⁻¹ * ↑(Nat.card ↥E) * (FABL.vectorWalshCharacter b) a *
      ∑ x,
        CryptBoolean.realSignView f (b + ↑x) *
          (FABL.vectorWalshCharacter a) (b + ↑x)
    theorem CryptBoolean.bentDual_poissonSummationFormula
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a b : FABL.F₂Cube n) :
  ∑ u,
      CryptBoolean.realSignView
          (CryptBoolean.bentDual f)
          (a + ↑u) *
        (FABL.vectorWalshCharacter b)
          (a + ↑u) =
    (2 ^ (n / 2))⁻¹ * ↑(Nat.card ↥E) *
        (FABL.vectorWalshCharacter b) a *
      ∑ x,
        CryptBoolean.realSignView f
            (b + ↑x) *
          (FABL.vectorWalshCharacter a)
            (b + ↑x)
    Carlet Relation (46): Poisson summation exchanges a bent function and
its dual across perpendicular affine subspaces.