Fourier–Walsh analysis on the finite Boolean cube

This file develops the normalized Fourier–Walsh conventions used in Section 2 of arXiv:2609.19123. A point of the cube is its set of coordinates equal to one.

noncomputable def Chvatal.cubeMean {ι : Type u_1} [Fintype ι] (f : Finset ι → ℝ) : ℝ

Uniform expectation on the Boolean cube, as in the preliminaries of the paper.

Equations

• Chvatal.cubeMean f = (∑ x : Finset ι, f x) / ↑(Fintype.card (Finset ι))

def Chvatal.walsh {ι : Type u_1} [DecidableEq ι] (S x : Finset ι) : ℝ

The Walsh character indexed by S, denoted χ_S in the paper.

Equations

• Chvatal.walsh S x = (-1) ^ (S ∩ x).card

noncomputable def Chvatal.fourier {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) (S : Finset ι) : ℝ

The normalized Fourier coefficient f̂(S) of Section 2.

Equations

• Chvatal.fourier f S = Chvatal.cubeMean fun (x : Finset ι) => f x * Chvatal.walsh S x

noncomputable def Chvatal.covariance {ι : Type u_1} [Fintype ι] (f g : Finset ι → ℝ) : ℝ

Covariance with respect to uniform measure, as used in the main theorem.

Equations

• Chvatal.covariance f g = (Chvatal.cubeMean fun (x : Finset ι) => f x * g x) - Chvatal.cubeMean f * Chvatal.cubeMean g

def Chvatal.dual {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) (x : Finset ι) : ℝ

The dual Boolean function f*(x) = 1 - f(1-x) in the paper.

Equations

• Chvatal.dual f x = 1 - f xᶜ

theorem Chvatal.cube_card_pos {ι : Type u_1} [Fintype ι] : 0 < ↑(Fintype.card (Finset ι))

The cube has positive cardinality, including when its coordinate set is empty.

@[simp]

theorem Chvatal.cubeMean_const {ι : Type u_1} [Fintype ι] (c : ℝ) : (cubeMean fun (x : Finset ι) => c) = c

Uniform expectation preserves constants; this fixes the normalization in Section 2.

theorem Chvatal.cubeMean_add {ι : Type u_1} [Fintype ι] (f g : Finset ι → ℝ) : (cubeMean fun (x : Finset ι) => f x + g x) = cubeMean f + cubeMean g

Additivity of the expectation used throughout the Fourier calculations.

theorem Chvatal.cubeMean_sub {ι : Type u_1} [Fintype ι] (f g : Finset ι → ℝ) : (cubeMean fun (x : Finset ι) => f x - g x) = cubeMean f - cubeMean g

Subtractivity of the expectation used throughout the Fourier calculations.

theorem Chvatal.cubeMean_mul_left {ι : Type u_1} [Fintype ι] (c : ℝ) (f : Finset ι → ℝ) : (cubeMean fun (x : Finset ι) => c * f x) = c * cubeMean f

Scalar linearity of expectation, used for the Fourier identities in Section 2.

theorem Chvatal.cubeMean_mul_right {ι : Type u_1} [Fintype ι] (f : Finset ι → ℝ) (c : ℝ) : (cubeMean fun (x : Finset ι) => f x * c) = cubeMean f * c

Right scalar linearity of expectation, a companion to cubeMean_mul_left.

@[simp]

theorem Chvatal.cubeMean_neg {ι : Type u_1} [Fintype ι] (f : Finset ι → ℝ) : (cubeMean fun (x : Finset ι) => -f x) = -cubeMean f

Negation commutes with expectation, as used in Fourier coefficient calculations.

theorem Chvatal.cubeMean_sum {ι : Type u_1} [Fintype ι] {κ : Type u_2} (s : Finset κ) (f : κ → Finset ι → ℝ) : (cubeMean fun (x : Finset ι) => ∑ k ∈ s, f k x) = ∑ k ∈ s, cubeMean (f k)

Expectation commutes with finite sums; this is used in Fourier inversion.

theorem Chvatal.cubeMean_symmDiff {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) (S : Finset ι) : (cubeMean fun (x : Finset ι) => f (symmDiff x S)) = cubeMean f

The uniform cube distribution is invariant under translation by symmetric difference.

theorem Chvatal.cubeMean_compl {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) : (cubeMean fun (x : Finset ι) => f xᶜ) = cubeMean f

Complementation preserves uniform expectation; used in the duality identities.

@[simp]

theorem Chvatal.cubeMean_dual {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) : cubeMean (dual f) = 1 - cubeMean f

The mean of the dual function, recorded in the paper's preliminaries.

@[simp]

theorem Chvatal.walsh_empty {ι : Type u_1} [DecidableEq ι] (x : Finset ι) : walsh ∅ x = 1

The empty Walsh character is the constant one function (Section 2).

@[simp]

theorem Chvatal.walsh_apply_empty {ι : Type u_1} [DecidableEq ι] (S : Finset ι) : walsh S ∅ = 1

Evaluating a character at the origin gives one (Section 2).

theorem Chvatal.walsh_comm {ι : Type u_1} [DecidableEq ι] (S x : Finset ι) : walsh S x = walsh x S

The symmetry of the Walsh kernel allows inversion to use the same transform.

@[simp]

theorem Chvatal.fourier_empty {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) : fourier f ∅ = cubeMean f

The empty Fourier coefficient is the uniform mean, in the convention of Section 2.

theorem Chvatal.walsh_insert {ι : Type u_1} [DecidableEq ι] {i : ι} {S : Finset ι} (hi : i ∉ S) (x : Finset ι) : walsh (insert i S) x = (if i ∈ x then -1 else 1) * walsh S x

Inserting a coordinate multiplies a Walsh character by that coordinate's sign.

theorem Chvatal.walsh_symmDiff_right {ι : Type u_1} [DecidableEq ι] (S x y : Finset ι) : walsh S (symmDiff x y) = walsh S x * walsh S y

The character multiplication law in the cube variable, used in Section 2.

theorem Chvatal.walsh_symmDiff_left {ι : Type u_1} [DecidableEq ι] (S T x : Finset ι) : walsh (symmDiff S T) x = walsh S x * walsh T x

The product of characters is indexed by symmetric difference, as in Section 2.

@[simp]

theorem Chvatal.walsh_sq {ι : Type u_1} [DecidableEq ι] (S x : Finset ι) : walsh S x ^ 2 = 1

Every Walsh character has square one, as needed for Parseval's identity.

theorem Chvatal.walsh_singleton {ι : Type u_1} [DecidableEq ι] (i : ι) (x : Finset ι) : walsh {i} x = if i ∈ x then -1 else 1

A singleton character is the sign of its single cube coordinate.

theorem Chvatal.walsh_toggle {ι : Type u_1} [DecidableEq ι] {S : Finset ι} {i : ι} (hi : i ∈ S) (x : Finset ι) : walsh S (symmDiff x {i}) = -walsh S x

Toggling a coordinate in a character's support reverses its sign.

theorem Chvatal.cubeMean_walsh_of_nonempty {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Finset ι} (hS : S.Nonempty) : cubeMean (walsh S) = 0

Every nonconstant Walsh character has mean zero, the orthogonality input of Section 2.

theorem Chvatal.cubeMean_walsh {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) : cubeMean (walsh S) = if S = ∅ then 1 else 0

The uniform mean of a Walsh character is the Kronecker delta at the empty set.

theorem Chvatal.walsh_orthogonality {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S T : Finset ι) : (cubeMean fun (x : Finset ι) => walsh S x * walsh T x) = if S = T then 1 else 0

Orthogonality of the Walsh basis, stated in the paper's normalized inner product.

theorem Chvatal.fourier_mul_walsh {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) (S T : Finset ι) : fourier (fun (x : Finset ι) => f x * walsh T x) S = fourier f (symmDiff S T)

Multiplying by a character shifts the Fourier index, as used in Lemma 2.2.

theorem Chvatal.fourier_eq_zero_of_invariant {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) {S : Finset ι} {i : ι} (hi : i ∈ S) (hf : ∀ (x : Finset ι), f (symmDiff x {i}) = f x) : fourier f S = 0

A function independent of coordinate i has no Fourier coefficient containing i. This is the support argument for the monomials in Lemma 2.2.

theorem Chvatal.sum_walsh_kernel {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x y : Finset ι) : ∑ S : Finset ι, walsh S x * walsh S y = if x = y then ↑(Fintype.card (Finset ι)) else 0

Summing the Walsh kernel gives a scaled Kronecker delta, the inversion kernel.

theorem Chvatal.fourier_inversion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) (x : Finset ι) : ∑ S : Finset ι, fourier f S * walsh S x = f x

Fourier inversion on the Boolean cube, the expansion used throughout Section 2.

theorem Chvatal.parseval_inner {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : Finset ι → ℝ) : (cubeMean fun (x : Finset ι) => f x * g x) = ∑ S : Finset ι, fourier f S * fourier g S

Parseval's identity for two real cube functions, as recalled in Section 2.

theorem Chvatal.parseval {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) : (cubeMean fun (x : Finset ι) => f x ^ 2) = ∑ S : Finset ι, fourier f S ^ 2

The sum-of-squares form of Parseval's identity in Section 2.

theorem Chvatal.fourier_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : Finset ι → ℝ) (S : Finset ι) : fourier (fun (x : Finset ι) => f x + g x) S = fourier f S + fourier g S

The transform preserves addition, used in the constant-coefficient adjustment.

theorem Chvatal.fourier_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : Finset ι → ℝ) (S : Finset ι) : fourier (fun (x : Finset ι) => f x - g x) S = fourier f S - fourier g S

The transform preserves subtraction, used in the constant-coefficient adjustment.

theorem Chvatal.fourier_const {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c : ℝ) (S : Finset ι) : fourier (fun (x : Finset ι) => c) S = if S = ∅ then c else 0

A constant has only its empty Fourier coefficient, as in the Section 2 convention.

theorem Chvatal.fourier_sub_mean {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) (S : Finset ι) : fourier (fun (x : Finset ι) => f x - cubeMean f) S = if S = ∅ then 0 else fourier f S

Subtracting the mean removes exactly the constant Fourier coefficient.

theorem Chvatal.fourier_injective {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Function.Injective fourier

The Fourier transform is injective, a direct consequence of the inversion formula.

theorem Chvatal.walsh_compl {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S x : Finset ι) : walsh S xᶜ = (-1) ^ S.card * walsh S x

Complementation multiplies a Walsh character by the parity of its index.

theorem Chvatal.fourier_compl {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) (S : Finset ι) : fourier (fun (x : Finset ι) => f xᶜ) S = (-1) ^ S.card * fourier f S

Complementing the argument multiplies Fourier coefficients by index parity.

theorem Chvatal.fourier_dual_of_nonempty {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) {S : Finset ι} (hS : S.Nonempty) : fourier (dual f) S = -((-1) ^ S.card * fourier f S)

The nonconstant Fourier coefficients of the dual, recalled in Section 2.

theorem Chvatal.covariance_fourier {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : Finset ι → ℝ) : covariance f g = ∑ S ∈ Finset.univ.erase ∅, fourier f S * fourier g S

Covariance is the sum of the products of the nonconstant Fourier coefficients.

theorem Chvatal.covariance_dual_fourier {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) : covariance f (dual f) = ∑ S ∈ Finset.univ.erase ∅, -(-1) ^ S.card * fourier f S ^ 2

The alternating Fourier expression for covariance with the dual, used in Theorem 1.2.

theorem Chvatal.cubeMean_nonneg {ι : Type u_1} [Fintype ι] {f : Finset ι → ℝ} (hf : ∀ (x : Finset ι), 0 ≤ f x) : 0 ≤ cubeMean f

Pointwise nonnegativity implies nonnegative uniform expectation.

theorem Chvatal.cubeMean_mono {ι : Type u_1} [Fintype ι] {f g : Finset ι → ℝ} (h : ∀ (x : Finset ι), f x ≤ g x) : cubeMean f ≤ cubeMean g

Pointwise comparison implies comparison of uniform expectations.

theorem Chvatal.fourier_symmDiff {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) (S T : Finset ι) : fourier (fun (x : Finset ι) => f (symmDiff x T)) S = walsh S T * fourier f S

Translating a cube function multiplies each Fourier coefficient by the character of the translation vector; this is the spectral step in equation (10).

theorem Chvatal.flip_energy_fourier {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) (T : Finset ι) : (cubeMean fun (x : Finset ι) => (f x - f (symmDiff x T)) ^ 2) = ∑ S : Finset ι, (1 - walsh S T) ^ 2 * fourier f S ^ 2

Equation (10), first equality: the energy of a simultaneous coordinate flip is the Fourier energy weighted by the squared character difference.

theorem Chvatal.walsh_flip_factor {ι : Type u_1} [DecidableEq ι] (S T : Finset ι) : (1 - walsh S T) ^ 2 = if Odd (S ∩ T).card then 4 else 0

The elementary parity computation behind equation (10).

theorem Chvatal.flip_energy_odd {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) (T : Finset ι) : (cubeMean fun (x : Finset ι) => (f x - f (symmDiff x T)) ^ 2) = 4 * ∑ S : Finset ι with Odd (S ∩ T).card, fourier f S ^ 2

Equation (10), second equality: only Fourier sets meeting the flipped set in an odd number of coordinates contribute to the flip energy.

theorem Chvatal.weighted_flip_energy {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : Finset ι → ℝ) : (1 / 2 * ∑ T : Finset ι, fourier g T ^ 2 * cubeMean fun (x : Finset ι) => (f x - f (symmDiff x T)) ^ 2) = 1 / 2 * cubeMean fun (x : Finset ι) => ∑ y : Finset ι, (f x - f y) ^ 2 * fourier g (symmDiff x y) ^ 2

The change of variables y = x ∆ T in equation (11), before specializing f to an indicator. Both sides retain the paper's factor of one half.