Auxiliary monomials

The Boolean monomials in Section 3.1 of the paper are represented as indicators of principal upper sets. This file proves their exact Fourier expansion (9), all four assertions of Lemma 3.1, and the orthonormal auxiliary families of Corollary 3.2. The independence proof uses subset induction and needs no arbitrary ordering of the monomials.

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

The Boolean monomial M_S of Section 3.1, equal to 1 exactly on supersets of S.

Equations

• Chvatal.monomial S x = if S ⊆ x then 1 else 0

@[simp]

theorem Chvatal.monomial_ne_zero_iff {ι : Type u_1} [DecidableEq ι] (S x : Finset ι) : monomial S x ≠ 0 ↔ S ⊆ x

The physical support calculation immediately preceding Lemma 3.1.

@[simp]

theorem Chvatal.monomial_self {ι : Type u_1} [DecidableEq ι] (S : Finset ι) : monomial S S = 1

Each monomial is one at its own index, the diagonal entry in the triangular independence argument of Lemma 3.1(iii).

theorem Chvatal.monomial_coefficients_eq_zero {ι : Type u_1} [DecidableEq ι] [Fintype ι] (c : Finset ι → ℝ) (h : ∑ S : Finset ι, c S • monomial S = 0) (S : Finset ι) : c S = 0

Evaluating a zero linear combination at successive subsets forces every coefficient to vanish. This is the triangular argument in Lemma 3.1(iii).

theorem Chvatal.linearIndependent_monomial {ι : Type u_1} [DecidableEq ι] [Finite ι] : LinearIndependent ℝ monomial

Lemma 3.1(iii): the entire Boolean monomial family is linearly independent. Consequently every family obtained by restricting the index set is independent.

theorem Chvatal.linearIndependent_monomial_subfamily {ι : Type u_1} [DecidableEq ι] [Finite ι] (A : Set (Finset ι)) : LinearIndependent ℝ fun (S : ↑A) => monomial ↑S

Lemma 3.1(iii) for any specified subfamily of monomials.

theorem Chvatal.monomial_toggle {ι : Type u_1} [DecidableEq ι] {S : Finset ι} {i : ι} (hi : i ∉ S) (x : Finset ι) : monomial S (symmDiff x {i}) = monomial S x

A monomial is unchanged when a coordinate outside its index is toggled. This gives its Fourier support in the discussion preceding Lemma 3.1.

theorem Chvatal.fourier_monomial_eq_zero {ι : Type u_1} [DecidableEq ι] [Fintype ι] {S T : Finset ι} (hTS : ¬T ⊆ S) : fourier (monomial S) T = 0

The Fourier support inclusion for monomials preceding Lemma 3.1: only subsets of the monomial's index can have a nonzero coefficient.

noncomputable def Chvatal.fullWalshMultiplier {ι : Type u_1} [DecidableEq ι] [Fintype ι] : (Finset ι → ℝ) ≃ₗ[ℝ] Finset ι → ℝ

Multiplication by the full Walsh character, used to construct the second auxiliary family in Lemma 3.1. It is a linear involution.

Equations

• One or more equations did not get rendered due to their size.

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

The functions χ_[n] M_S in the second auxiliary family of Lemma 3.1.

Equations

• Chvatal.twistedMonomial S = Chvatal.fullWalshMultiplier (Chvatal.monomial S)

@[simp]

theorem Chvatal.twistedMonomial_apply {ι : Type u_1} [DecidableEq ι] [Fintype ι] (S x : Finset ι) : twistedMonomial S x = monomial S x * walsh Finset.univ x

Coordinate description of the twisted monomials of Lemma 3.1.

theorem Chvatal.linearIndependent_twistedMonomial {ι : Type u_1} [DecidableEq ι] [Fintype ι] : LinearIndependent ℝ twistedMonomial

Lemma 3.1(iii) for the second family: the full character is an invertible multiplier, so independence of the monomials is preserved.

theorem Chvatal.fourier_twistedMonomial_eq_zero {ι : Type u_1} [DecidableEq ι] [Fintype ι] {S T : Finset ι} (hST : ¬Sᶜ ⊆ T) : fourier (twistedMonomial S) T = 0

Fourier support of the second family in Lemma 3.1: a nonzero coefficient must contain the complement of the monomial's index.

theorem Chvatal.monomial_eq_zero_of_not_mem {ι : Type u_1} [DecidableEq ι] {F : Family ι} (hF : F.IsIncreasing) {S : Finset ι} (hS : S ∈ F) {x : Finset ι} (hx : x ∉ F) : monomial S x = 0

Lemma 3.1(i), physical support: increasing families contain the entire support of every monomial indexed by one of their members.

theorem Chvatal.fourier_monomial_eq_zero_of_mem {ι : Type u_1} [DecidableEq ι] [Fintype ι] {G : Family ι} (hG : G.IsIncreasing) {S T : Finset ι} (hS : S ∉ G) (hT : T ∈ G) : fourier (monomial S) T = 0

Lemma 3.1(i), Fourier support: a monomial whose index lies outside an increasing family has zero Fourier coefficients on that family.

theorem Chvatal.twistedMonomial_eq_zero_of_not_mem {ι : Type u_1} [DecidableEq ι] [Fintype ι] {F : Family ι} (hF : F.IsIncreasing) {S : Finset ι} (hS : S ∈ F) {x : Finset ι} (hx : x ∉ F) : twistedMonomial S x = 0

Lemma 3.1(ii), physical support of the twisted monomials.

theorem Chvatal.fourier_twistedMonomial_eq_zero_of_not_mem {ι : Type u_1} [DecidableEq ι] [Fintype ι] {G : Family ι} (hG : G.IsIncreasing) {S T : Finset ι} (hS : Sᶜ ∈ G) (hT : T ∉ G) : fourier (twistedMonomial S) T = 0

Lemma 3.1(ii), Fourier support of the twisted monomials: when the complement of the index belongs to an increasing family, all coefficients outside it vanish.

theorem Chvatal.monomial_insert {ι : Type u_1} [DecidableEq ι] (i : ι) (S x : Finset ι) : monomial (insert i S) x = if i ∈ x then monomial S x else 0

The multiplicative recursion for the Boolean monomials in Section 3.1.

theorem Chvatal.monomial_expansion_scaled {ι : Type u_1} [DecidableEq ι] (S x : Finset ι) : ∑ T ∈ S.powerset, (-1) ^ T.card * walsh T x = 2 ^ S.card * monomial S x

Equation (9), multiplied by 2^|S|: the finite Walsh expansion of a Boolean monomial. This proof follows the coordinate product expansion.

theorem Chvatal.monomial_expansion {ι : Type u_1} [DecidableEq ι] (S x : Finset ι) : monomial S x = (2 ^ S.card)⁻¹ * ∑ T ∈ S.powerset, (-1) ^ T.card * walsh T x

Equation (9): the normalized Fourier–Walsh expansion of M_S.

theorem Chvatal.fourier_smul_function {ι : Type u_1} [DecidableEq ι] [Fintype ι] (c : ℝ) (f : Finset ι → ℝ) (S : Finset ι) : fourier (c • f) S = c * fourier f S

Scalar linearity of the Fourier transform, used when preserving support under the Gram–Schmidt process in Corollary 3.2.

def Chvatal.supportSubspace {ι : Type u_1} [DecidableEq ι] [Fintype ι] (F K : Family ι) : Submodule ℝ (Finset ι → ℝ)

The functions satisfying both support restrictions of Corollary 3.2 form a linear subspace: physical support lies in F, and Fourier support lies in K.

Equations

• Chvatal.supportSubspace F K = { carrier := {f : Finset ι → ℝ | (∀ x ∉ F, f x = 0) ∧ ∀ S ∉ K, Chvatal.fourier f S = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Chvatal.mem_supportSubspace {ι : Type u_1} [DecidableEq ι] [Fintype ι] (F K : Family ι) (f : Finset ι → ℝ) : f ∈ supportSubspace F K ↔ (∀ x ∉ F, f x = 0) ∧ ∀ S ∉ K, fourier f S = 0

Expanded membership criterion for the support-preserving subspace used in Corollary 3.2.

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

The probability inner product of Theorem 2.1 is the cube expectation used in all Fourier identities in Section 2.

theorem Chvatal.uniformInner_eq_zero_of_fourier_support {ι : Type u_1} [DecidableEq ι] [Fintype ι] (G : Family ι) {f g : Finset ι → ℝ} (hf : ∀ S ∈ G, fourier f S = 0) (hg : ∀ S ∉ G, fourier g S = 0) : uniformInner f g = 0

Lemma 3.1(iv): disjoint Fourier supports imply orthogonality by Parseval.

theorem Chvatal.uniformInner_comm {ι : Type u_1} [Fintype ι] (f g : Finset ι → ℝ) : uniformInner f g = uniformInner g f

Symmetry of the real probability inner product, used for the two mixed orders in the combined orthonormal family of Corollary 3.2.

theorem Chvatal.monomial_twistedMonomial_orthogonal {ι : Type u_1} [DecidableEq ι] [Fintype ι] {G : Family ι} (hG : G.IsIncreasing) {S T : Finset ι} (hS : S ∉ G) (hT : Tᶜ ∈ G) : uniformInner (monomial S) (twistedMonomial T) = 0

Lemma 3.1(iv) for the particular two monomial families in the paper.

theorem Chvatal.auxiliary_orthonormal_system {ι : Type u_1} [DecidableEq ι] [Fintype ι] (F G : Family ι) (hF : F.IsIncreasing) (hG : G.IsIncreasing) : ∃ (u : ↥(F \ G) → Finset ι → ℝ) (v : ↥(F \ G.dual) → Finset ι → ℝ), UniformOrthonormal (Sum.elim u v) ∧ (∀ (i : ↥(F \ G)), u i ∈ supportSubspace F Gᶜ) ∧ ∀ (i : ↥(F \ G.dual)), v i ∈ supportSubspace F G

Corollary 3.2: orthonormal auxiliary families with the paper's exact index sets and both required support conditions. The sum type joins the two families into a single orthonormal system, including when either index set is empty.

theorem Chvatal.fourier_monomial {ι : Type u_1} [DecidableEq ι] [Fintype ι] (S T : Finset ι) : fourier (monomial S) T = if T ⊆ S then (2 ^ S.card)⁻¹ * (-1) ^ T.card else 0

The exact coefficient formula from equation (9). In particular, every subset of S occurs with a nonzero Fourier coefficient.

theorem Chvatal.fourier_monomial_ne_zero_iff {ι : Type u_1} [DecidableEq ι] [Fintype ι] (S T : Finset ι) : fourier (monomial S) T ≠ 0 ↔ T ⊆ S

The exact Fourier support calculation for the first family preceding Lemma 3.1.

theorem Chvatal.fourier_twistedMonomial {ι : Type u_1} [DecidableEq ι] [Fintype ι] (S T : Finset ι) : fourier (twistedMonomial S) T = if Sᶜ ⊆ T then (2 ^ S.card)⁻¹ * (-1) ^ Tᶜ.card else 0

The exact coefficients of the second auxiliary family, obtained by complementing Fourier indices as in the discussion preceding Lemma 3.1.

theorem Chvatal.fourier_twistedMonomial_ne_zero_iff {ι : Type u_1} [DecidableEq ι] [Fintype ι] (S T : Finset ι) : fourier (twistedMonomial S) T ≠ 0 ↔ Sᶜ ⊆ T

The exact Fourier support calculation for the second family preceding Lemma 3.1: its support is the upper interval above the complementary index.

theorem Chvatal.support_monomial {ι : Type u_1} [DecidableEq ι] (S : Finset ι) : Function.support (monomial S) = {x : Finset ι | S ⊆ x}

The physical support equality for monomials stated before Lemma 3.1.

theorem Chvatal.support_fourier_monomial {ι : Type u_1} [DecidableEq ι] [Fintype ι] (S : Finset ι) : Function.support (fourier (monomial S)) = {T : Finset ι | T ⊆ S}

The Fourier support equality for monomials stated before Lemma 3.1.

theorem Chvatal.support_twistedMonomial {ι : Type u_1} [DecidableEq ι] [Fintype ι] (S : Finset ι) : Function.support (twistedMonomial S) = {x : Finset ι | S ⊆ x}

Multiplication by the full character does not change physical support, as stated before Lemma 3.1.

theorem Chvatal.support_fourier_twistedMonomial {ι : Type u_1} [DecidableEq ι] [Fintype ι] (S : Finset ι) : Function.support (fourier (twistedMonomial S)) = {T : Finset ι | Sᶜ ⊆ T}

The Fourier support equality for twisted monomials stated before Lemma 3.1.