Ordered influence weights in the sharp correlation inequality

This file defines the left-hand side 𝒲(f,g) of Theorem 1.2 and proves the comparison (16) from Lemma 3.3. It also records the variance argument in Corollary 1.3. The parameter optimization is in Chvatal.Optimization.

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

The largest influence over a Fourier index, as in Theorem 1.2. The empty index is assigned zero so that sums can run over the entire cube.

Equations

• Chvatal.maxInfluence f S = if h : S.Nonempty then S.sup' h (Chvatal.influence f) else 0

@[simp]

theorem Chvatal.maxInfluence_empty {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) : maxInfluence f ∅ = 0

The empty Fourier index makes no contribution to Theorem 1.2.

theorem Chvatal.maxInfluence_of_nonempty {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) {S : Finset ι} (hS : S.Nonempty) : maxInfluence f S = S.sup' hS (influence f)

On a nonempty index, the influence weight is the ordinary finite maximum.

theorem Chvatal.influence_le_maxInfluence {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) {S : Finset ι} {i : ι} (hi : i ∈ S) : influence f i ≤ maxInfluence f S

Every coordinate in an index is bounded by its maximum influence.

theorem Chvatal.maxInfluence_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Finset ι → ℝ) (S : Finset ι) : 0 ≤ maxInfluence f S

The spectral weights in Theorem 1.2 are nonnegative.

theorem Chvatal.maxInfluence_le_flip_energy {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Finset ι → ℝ} (hf : IsBoolean f) (hm : Monotone f) (T : Finset ι) : maxInfluence f T ≤ cubeMean fun (x : Finset ι) => (f x - f (symmDiff x T)) ^ 2

Lemma 3.3 in its stated maximum-over-coordinates form.

theorem Chvatal.maxInfluence_le_odd_spectral {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Finset ι → ℝ} (hf : IsBoolean f) (hm : Monotone f) (T : Finset ι) : maxInfluence f T ≤ 4 * ∑ S : Finset ι with Odd (S ∩ T).card, fourier f S ^ 2

Lemma 3.3, equation (15): maximum influence is bounded by the odd-intersection Fourier energy. The formula also holds for the empty index under our zero convention.

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

The spectral expression 𝒲(f,g) in Theorem 1.2 and Section 5. Its empty-index term vanishes by maxInfluence_empty.

Equations

• Chvatal.spectralWeight f g = ∑ S : Finset ι, Chvatal.fourier g S ^ 2 * Chvatal.maxInfluence f S

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

The expression spectralWeight agrees with the paper's sum over nonempty indices.

theorem Chvatal.spectralWeight_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : Finset ι → ℝ) : 0 ≤ spectralWeight f g

Nonnegativity of the left side of Theorem 1.2, used when a covariance vanishes.

theorem Chvatal.spectralWeight_le_four_spectral {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Finset ι → ℝ} (hf : IsBoolean f) (hm : Monotone f) (g : Finset ι → ℝ) : spectralWeight f g ≤ 4 * ∑ T : Finset ι, ∑ S : Finset ι with Odd (S ∩ T).card, fourier f S ^ 2 * fourier g T ^ 2

Equation (16): multiply Lemma 3.3 by the squared Fourier coefficient and sum.

theorem Chvatal.fourier_mass_of_antipodal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {g : Finset ι → ℝ} (hb : IsBoolean g) (hg : dual g = g) : ∑ S ∈ Finset.univ.erase ∅, fourier g S ^ 2 = 1 / 4

The Parseval computation in Corollary 1.3: nonconstant Fourier coefficients of an antipodal Boolean function have total squared mass one quarter.

theorem Chvatal.quarter_le_spectralWeight {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f g : Finset ι → ℝ} {m : ℝ} (hb : IsBoolean g) (hg : dual g = g) (hm : ∀ (i : ι), m ≤ influence f i) : m / 4 ≤ spectralWeight f g

The lower bound on 𝒲(f,g) used in Corollary 1.3. Any common lower bound on the coordinate influences is weighted by the variance 1/4.