1.9. Walsh inversion and Parseval
Theorem1.9.1
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.9.1●2 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter02/Fourier.leancomplete
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.leancomplete
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.9.2
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.9.2●4 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter02/Fourier.leancomplete
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.leancomplete
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.leancomplete
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)²`.
-
theoremdefined in CryptBoolean/Carlet/Chapter02/Fourier.leancomplete
theorem CryptBoolean.exists_walshTransform_ne_zero {n : ℕ} (f : CryptBoolean.BooleanFunction n) : ∃ a, CryptBoolean.walshTransform f a ≠ 0
theorem CryptBoolean.exists_walshTransform_ne_zero {n : ℕ} (f : CryptBoolean.BooleanFunction n) : ∃ a, CryptBoolean.walshTransform f a ≠ 0
Every Boolean function has a nonzero raw Walsh coefficient.
Equivalently, the normalized coefficients satisfy
\sum_a\widetilde{f_\chi}(a)^2=1.