1.2. Walsh inversion and Parseval🔗

Theorem1.2.1

uses 1used by 0✓L∃∀N

Tagscarletchapter-2corollary-2page-25fidelity-exact-sign-specialization

Walsh inversion (Carlet, Corollary 2, Relation (19), p. 25). For every f:V_n\to\mathbb F_2 and x\in V_n, f_\chi(x) =2^{-n}\sum_{a\in V_n}W_f(a)(-1)^{a\mathbin\cdot x}. Equivalently, 2^n f_\chi(x)=\sum_{a\in V_n}W_f(a)(-1)^{a\mathbin\cdot x}.

Lean code for Theorem1.2.1●2 theorems

theoremdefined in CryptBoolean/Carlet/Chapter02/Fourier.lean

complete

theorem CryptBoolean.two_pow_mul_realSignView_eq_sum_walshTransform_mul_character
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n) :
  2 ^ n * CryptBoolean.realSignView f x =
    ∑ a,
      ↑(CryptBoolean.walshTransform f a) *
        (FABL.vectorWalshCharacter a) x

theorem CryptBoolean.two_pow_mul_realSignView_eq_sum_walshTransform_mul_character
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  2 ^ n * CryptBoolean.realSignView f x =
    ∑ a,
      ↑(CryptBoolean.walshTransform f a) *
        (FABL.vectorWalshCharacter a) x

The Walsh-weighted expansion of the sign view: `2^n (-1)^{f(x)} = ∑ₐ W_f(a) χ_a(x)`.

theoremdefined in CryptBoolean/Carlet/Chapter02/Fourier.lean

complete

theorem CryptBoolean.realSignView_eq_inv_two_pow_mul_sum_walshTransform_mul_character
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n) :
  CryptBoolean.realSignView f x =
    (2 ^ n)⁻¹ *
      ∑ a,
        ↑(CryptBoolean.walshTransform f a) *
          (FABL.vectorWalshCharacter a) x

theorem CryptBoolean.realSignView_eq_inv_two_pow_mul_sum_walshTransform_mul_character
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  CryptBoolean.realSignView f x =
    (2 ^ n)⁻¹ *
      ∑ a,
        ↑(CryptBoolean.walshTransform f
              a) *
          (FABL.vectorWalshCharacter a) x

Carlet's Walsh inversion for the sign view: `(-1)^{f(x)} = 2^{-n} ∑ₐ W_f(a) χ_a(x)`.

Theorem1.2.2

uses 1used by 0✓L∃∀N

Tagscarletchapter-2corollary-3relation-23page-27fidelity-exact

Parseval for Boolean sign functions (Carlet, Corollary 3, Relation (23), p. 27). For every f:V_n\to\mathbb F_2, \sum_{a\in V_n}W_f(a)^2=2^{2n}.

Lean code for Theorem1.2.2●3 theorems

theoremdefined in CryptBoolean/Carlet/Chapter02/Fourier.lean

complete

theorem CryptBoolean.realSignView_mul_self {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n) :
  CryptBoolean.realSignView f x * CryptBoolean.realSignView f x = 1

theorem CryptBoolean.realSignView_mul_self {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  CryptBoolean.realSignView f x *
      CryptBoolean.realSignView f x =
    1

The real sign view is `±1`, so its pointwise square is `1`.

theoremdefined in CryptBoolean/Carlet/Chapter02/Fourier.lean

complete

theorem CryptBoolean.sum_vectorFourierCoeff_realSignView_sq {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ a, FABL.vectorFourierCoeff (CryptBoolean.realSignView f) a ^ 2 = 1

theorem CryptBoolean.sum_vectorFourierCoeff_realSignView_sq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ a,
      FABL.vectorFourierCoeff
          (CryptBoolean.realSignView f)
          a ^
        2 =
    1

Parseval for the normalized coefficients of the sign view: the spectral squares sum to one.

theoremdefined in CryptBoolean/Carlet/Chapter02/Fourier.lean

complete

theorem CryptBoolean.sum_walshTransform_sq_eq_two_pow_sq {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ a, ↑(CryptBoolean.walshTransform f a) ^ 2 = (2 ^ n) ^ 2

theorem CryptBoolean.sum_walshTransform_sq_eq_two_pow_sq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ a,
      ↑(CryptBoolean.walshTransform f a) ^
        2 =
    (2 ^ n) ^ 2

Parseval for Carlet's raw integer Walsh transform: `∑ₐ W_f(a)² = (2^n)²`.

Formalization note. Through the explicit normalization bridge, the same theorem is represented internally by \sum_a\widetilde{f_\chi}(a)^2=1 before rescaling to Carlet's raw integer spectrum.