1.8. Fourier operations and subspaces
Discrete Fourier transform (Carlet, Relation (11), p. 21). For a pseudo-Boolean
function \varphi:V_n\to\mathbb R, define
\mathcal F\varphi(a)
=\widehat\varphi(a)
=\sum_{x\in V_n}\varphi(x)(-1)^{a\mathbin\cdot x}
\qquad(a\in V_n).
If \widetilde\varphi(a)=2^{-n}\widehat\varphi(a) denotes the normalized
coefficient, then
\widehat\varphi(a)=2^n\widetilde\varphi(a).
Lean code for Definition1.8.1●2 declarations
Associated Lean declarations
-
defdefined in CryptBoolean/Carlet/Chapter02/FourierOperations.leancomplete
def CryptBoolean.rawFourierTransform {n : ℕ} (φ : FABL.F₂Cube n → ℝ) (a : FABL.F₂Cube n) : ℝ
def CryptBoolean.rawFourierTransform {n : ℕ} (φ : FABL.F₂Cube n → ℝ) (a : FABL.F₂Cube n) : ℝ
Carlet's unnormalized Fourier transform of a pseudo-Boolean function.
-
theoremdefined in CryptBoolean/Carlet/Chapter02/FourierOperations.leancomplete
theorem CryptBoolean.rawFourierTransform_eq_two_pow_mul_vectorFourierCoeff {n : ℕ} (φ : FABL.F₂Cube n → ℝ) (a : FABL.F₂Cube n) : CryptBoolean.rawFourierTransform φ a = 2 ^ n * FABL.vectorFourierCoeff φ a
theorem CryptBoolean.rawFourierTransform_eq_two_pow_mul_vectorFourierCoeff {n : ℕ} (φ : FABL.F₂Cube n → ℝ) (a : FABL.F₂Cube n) : CryptBoolean.rawFourierTransform φ a = 2 ^ n * FABL.vectorFourierCoeff φ a
Carlet's raw transform is the cardinality-scaled normalized FABL coefficient.
Proposition 6 (Carlet, p. 24). Let \varphi:V_n\to\mathbb R and
a,b,u\in V_n. If
\psi(x)=(-1)^{a\mathbin\cdot x}\varphi(x+b),
then
\widehat\psi(u)
=(-1)^{b\mathbin\cdot(a+u)}\widehat\varphi(a+u).
Lean code for Proposition1.8.2●2 theorems
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter02/FourierOperations.leancomplete
theorem CryptBoolean.vectorFourierCoeff_mul_vectorWalshCharacter {n : ℕ} (φ : FABL.F₂Cube n → ℝ) (a u : FABL.F₂Cube n) : FABL.vectorFourierCoeff (fun x => (FABL.vectorWalshCharacter a) x * φ x) u = FABL.vectorFourierCoeff φ (a + u)
theorem CryptBoolean.vectorFourierCoeff_mul_vectorWalshCharacter {n : ℕ} (φ : FABL.F₂Cube n → ℝ) (a u : FABL.F₂Cube n) : FABL.vectorFourierCoeff (fun x => (FABL.vectorWalshCharacter a) x * φ x) u = FABL.vectorFourierCoeff φ (a + u)
Multiplying by a Walsh character shifts the normalized Fourier index.
-
theoremdefined in CryptBoolean/Carlet/Chapter02/FourierOperations.leancomplete
theorem CryptBoolean.rawFourierTransform_modulate_translate {n : ℕ} (φ : FABL.F₂Cube n → ℝ) (a b u : FABL.F₂Cube n) : CryptBoolean.rawFourierTransform (fun x => (FABL.vectorWalshCharacter a) x * φ (x + b)) u = (FABL.vectorWalshCharacter (a + u)) b * CryptBoolean.rawFourierTransform φ (a + u)
theorem CryptBoolean.rawFourierTransform_modulate_translate {n : ℕ} (φ : FABL.F₂Cube n → ℝ) (a b u : FABL.F₂Cube n) : CryptBoolean.rawFourierTransform (fun x => (FABL.vectorWalshCharacter a) x * φ (x + b)) u = (FABL.vectorWalshCharacter (a + u)) b * CryptBoolean.rawFourierTransform φ (a + u)
Carlet Proposition 6: modulation and translation shift the raw spectrum.
Corollary 2 (Carlet, Relation (19), p. 25). For every
\varphi:V_n\to\mathbb R and x\in V_n,
\widehat{\widehat\varphi}(x)=2^n\varphi(x).
Lean code for Theorem1.8.3●1 theorem
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter02/FourierOperations.leancomplete
theorem CryptBoolean.rawFourierTransform_involution {n : ℕ} (φ : FABL.F₂Cube n → ℝ) (x : FABL.F₂Cube n) : CryptBoolean.rawFourierTransform (CryptBoolean.rawFourierTransform φ) x = 2 ^ n * φ x
theorem CryptBoolean.rawFourierTransform_involution {n : ℕ} (φ : FABL.F₂Cube n → ℝ) (x : FABL.F₂Cube n) : CryptBoolean.rawFourierTransform (CryptBoolean.rawFourierTransform φ) x = 2 ^ n * φ x
Carlet Corollary 2: applying the raw Fourier transform twice multiplies by `2^n`.
Proposition 7 (Carlet, Relation (16), pp. 24--25). Let E\le V_n, let
E^\perp=\{u\in V_n:u\mathbin\cdot x=0\text{ for every }x\in E\}, and let
\mathbf 1_E be the real-valued indicator of E. Then, for every u\in V_n,
\widehat{\mathbf 1_E}(u)
=
\begin{cases}
|E|,&u\in E^\perp,\\
0,&u\notin E^\perp.
\end{cases}
Equivalently, \widehat{\mathbf 1_E}=|E|\mathbf 1_{E^\perp}.
Lean code for Proposition1.8.4●2 theorems
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter02/Subspaces.leancomplete
theorem CryptBoolean.two_pow_mul_inversePerpendicularCard_eq_card {n : ℕ} (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) : 2 ^ n * FABL.inversePerpendicularCard E = ↑(Nat.card ↥E)
theorem CryptBoolean.two_pow_mul_inversePerpendicularCard_eq_card {n : ℕ} (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) : 2 ^ n * FABL.inversePerpendicularCard E = ↑(Nat.card ↥E)
The raw scaling factor for a subspace is its cardinality.
-
theoremdefined in CryptBoolean/Carlet/Chapter02/Subspaces.leancomplete
theorem CryptBoolean.rawFourierTransform_setIndicator_submodule {n : ℕ} (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (u : FABL.F₂Cube n) : CryptBoolean.rawFourierTransform (FABL.setIndicator ↑E) u = if u ∈ FABL.perpendicularSubspace E then ↑(Nat.card ↥E) else 0
theorem CryptBoolean.rawFourierTransform_setIndicator_submodule {n : ℕ} (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (u : FABL.F₂Cube n) : CryptBoolean.rawFourierTransform (FABL.setIndicator ↑E) u = if u ∈ FABL.perpendicularSubspace E then ↑(Nat.card ↥E) else 0
Carlet Proposition 7: the raw transform of a subspace indicator is its cardinality on the perpendicular subspace and zero off it.
Normalized Poisson summation specialization. Let E\le V_n, let
\varphi:V_n\to\mathbb R, and let z\in V_n. Then
\frac{1}{|E|}\sum_{h\in E}\varphi(h+z)
=\sum_{u\in E^\perp}(-1)^{u\mathbin\cdot z}\widetilde\varphi(u).
Here \widetilde\varphi(u)=2^{-n}\widehat\varphi(u).
Lean code for Corollary1.8.5●1 theorem
Associated Lean declarations
-
FABL.poissonSummationFormula[complete]
-
FABL.poissonSummationFormula[complete]
-
theoremdefined in FABL/Chapter03/Restrictions.leancomplete
theorem FABL.poissonSummationFormula {n : ℕ} (f : FABL.F₂Cube n → ℝ) (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (z : FABL.F₂Cube n) : (Finset.univ.expect fun h => f (↑h + z)) = ∑ γ, (FABL.vectorWalshCharacter ↑γ) z * FABL.vectorFourierCoeff f ↑γ
theorem FABL.poissonSummationFormula {n : ℕ} (f : FABL.F₂Cube n → ℝ) (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (z : FABL.F₂Cube n) : (Finset.univ.expect fun h => f (↑h + z)) = ∑ γ, (FABL.vectorWalshCharacter ↑γ) z * FABL.vectorFourierCoeff f ↑γ
O'Donnell's Poisson Summation Formula on the binary cube.
This normalized coset-average identity is the specialization a=0 of the full Poisson formula
below.
Corollary 1 (Poisson summation; Carlet, Relation (17), p. 25). For every
\varphi:V_n\to\mathbb R, every subspace E\le V_n, and all a,b\in V_n,
\sum_{u\in a+E}(-1)^{b\mathbin\cdot u}\widehat\varphi(u)
=|E|(-1)^{a\mathbin\cdot b}
\sum_{x\in b+E^\perp}(-1)^{a\mathbin\cdot x}\varphi(x).
Lean code for Corollary1.8.6●1 theorem
Associated Lean declarations
-
CryptBoolean.rawPoissonSummationFormula[complete]
-
CryptBoolean.rawPoissonSummationFormula[complete]
-
theoremdefined in CryptBoolean/Carlet/Chapter02/Subspaces.leancomplete
theorem CryptBoolean.rawPoissonSummationFormula {n : ℕ} (φ : FABL.F₂Cube n → ℝ) (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a b : FABL.F₂Cube n) : ∑ u, (FABL.vectorWalshCharacter b) (a + ↑u) * CryptBoolean.rawFourierTransform φ (a + ↑u) = ↑(Nat.card ↥E) * (FABL.vectorWalshCharacter b) a * ∑ x, (FABL.vectorWalshCharacter a) (b + ↑x) * φ (b + ↑x)
theorem CryptBoolean.rawPoissonSummationFormula {n : ℕ} (φ : FABL.F₂Cube n → ℝ) (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a b : FABL.F₂Cube n) : ∑ u, (FABL.vectorWalshCharacter b) (a + ↑u) * CryptBoolean.rawFourierTransform φ (a + ↑u) = ↑(Nat.card ↥E) * (FABL.vectorWalshCharacter b) a * ∑ x, (FABL.vectorWalshCharacter a) (b + ↑x) * φ (b + ↑x)
Carlet Corollary 1, Relation (17): the full raw Poisson summation formula on affine cosets, with both modulation parameters explicit.
-
CryptBoolean.rawConvolution[complete] -
CryptBoolean.rawConvolution_eq_two_pow_mul_convolution[complete]
Convolution (Carlet, p. 26). For \varphi,\psi:V_n\to\mathbb R, define
their unnormalized convolution by
(\varphi\otimes\psi)(x)
=\sum_{y\in V_n}\varphi(y)\psi(x+y)
\qquad(x\in V_n).
Lean code for Definition1.8.7●2 declarations
Associated Lean declarations
-
CryptBoolean.rawConvolution[complete]
-
CryptBoolean.rawConvolution_eq_two_pow_mul_convolution[complete]
-
CryptBoolean.rawConvolution[complete] -
CryptBoolean.rawConvolution_eq_two_pow_mul_convolution[complete]
-
defdefined in CryptBoolean/Carlet/Chapter02/FourierOperations.leancomplete
def CryptBoolean.rawConvolution {n : ℕ} (φ ψ : FABL.F₂Cube n → ℝ) (x : FABL.F₂Cube n) : ℝ
def CryptBoolean.rawConvolution {n : ℕ} (φ ψ : FABL.F₂Cube n → ℝ) (x : FABL.F₂Cube n) : ℝ
Carlet's unnormalized convolution on the additive binary cube.
-
theoremdefined in CryptBoolean/Carlet/Chapter02/FourierOperations.leancomplete
theorem CryptBoolean.rawConvolution_eq_two_pow_mul_convolution {n : ℕ} (φ ψ : FABL.F₂Cube n → ℝ) (x : FABL.F₂Cube n) : CryptBoolean.rawConvolution φ ψ x = 2 ^ n * FABL.convolution φ ψ x
theorem CryptBoolean.rawConvolution_eq_two_pow_mul_convolution {n : ℕ} (φ ψ : FABL.F₂Cube n → ℝ) (x : FABL.F₂Cube n) : CryptBoolean.rawConvolution φ ψ x = 2 ^ n * FABL.convolution φ ψ x
Raw convolution is the cardinality-scaled normalized FABL convolution.
Proposition 8 (Carlet, Relation (20), p. 26). For all
\varphi,\psi:V_n\to\mathbb R and u\in V_n,
\widehat{\varphi\otimes\psi}(u)
=\widehat\varphi(u)\widehat\psi(u).
Lean code for Proposition1.8.8●1 theorem
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter02/FourierOperations.leancomplete
theorem CryptBoolean.rawFourierTransform_rawConvolution {n : ℕ} (φ ψ : FABL.F₂Cube n → ℝ) (a : FABL.F₂Cube n) : CryptBoolean.rawFourierTransform (CryptBoolean.rawConvolution φ ψ) a = CryptBoolean.rawFourierTransform φ a * CryptBoolean.rawFourierTransform ψ a
theorem CryptBoolean.rawFourierTransform_rawConvolution {n : ℕ} (φ ψ : FABL.F₂Cube n → ℝ) (a : FABL.F₂Cube n) : CryptBoolean.rawFourierTransform (CryptBoolean.rawConvolution φ ψ) a = CryptBoolean.rawFourierTransform φ a * CryptBoolean.rawFourierTransform ψ a
Carlet Proposition 8: the raw Fourier transform sends raw convolution to pointwise product.
Relation (22) and Parseval's relation (Carlet, p. 27). For all
\varphi,\psi:V_n\to\mathbb R,
\sum_{u\in V_n}\widehat\varphi(u)\widehat\psi(u)
=2^n\sum_{x\in V_n}\varphi(x)\psi(x).
In particular, taking \psi=\varphi gives Corollary 3:
\sum_{u\in V_n}\widehat\varphi(u)^2
=2^n\sum_{x\in V_n}\varphi(x)^2.
Lean code for Theorem1.8.9●1 theorem
Associated Lean declarations
-
CryptBoolean.sum_rawFourierTransform_mul[complete]
-
CryptBoolean.sum_rawFourierTransform_mul[complete]
-
theoremdefined in CryptBoolean/Carlet/Chapter02/FourierOperations.leancomplete
theorem CryptBoolean.sum_rawFourierTransform_mul {n : ℕ} (φ ψ : FABL.F₂Cube n → ℝ) : ∑ a, CryptBoolean.rawFourierTransform φ a * CryptBoolean.rawFourierTransform ψ a = 2 ^ n * ∑ x, φ x * ψ x
theorem CryptBoolean.sum_rawFourierTransform_mul {n : ℕ} (φ ψ : FABL.F₂Cube n → ℝ) : ∑ a, CryptBoolean.rawFourierTransform φ a * CryptBoolean.rawFourierTransform ψ a = 2 ^ n * ∑ x, φ x * ψ x
Carlet Corollary 3: Plancherel for the unnormalized transform.