The quadratic correlation inequality

This file follows Section 3.2 of arXiv:2609.19123: spectral flip energy is written as a boundary sum, a constant is subtracted from the second function, and the auxiliary orthonormal system bounds the resulting interior sum.

theorem Chvatal.sum_indicator_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Family ι) (h : Finset ι → ℝ) : ∑ x : Finset ι, F.indicator x * h x = ∑ x ∈ F, h x

Summing against a family indicator restricts a sum to that family, as in (11).

theorem Chvatal.indicator_boundary_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Family ι) (k : Finset ι → Finset ι → ℝ) (hk : ∀ (x y : Finset ι), k x y = k y x) : ∑ x : Finset ι, ∑ y : Finset ι, (F.indicator x - F.indicator y) ^ 2 * k x y = 2 * ∑ x ∈ F, ∑ y ∈ Fᶜ, k x y

Summing a symmetric kernel against the squared change of an indicator counts each boundary pair twice. This is the Boolean step in equation (11).

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

Equation (11), its first equality: the odd-intersection spectral sum is one half of the Fourier-weighted flip energy.

theorem Chvatal.two_spectral_eq_boundary {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Family ι) (g : Finset ι → ℝ) : 2 * ∑ T : Finset ι, ∑ S : Finset ι with Odd (S ∩ T).card, fourier F.indicator S ^ 2 * fourier g T ^ 2 = (∑ x ∈ F, ∑ y ∈ Fᶜ, fourier g (symmDiff x y) ^ 2) / ↑(Fintype.card (Finset ι))

Equation (11), the boundary formula for a family indicator.

theorem Chvatal.boundary_sub_const {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Family ι) (g : Finset ι → ℝ) (t : ℝ) : ∑ x ∈ F, ∑ y ∈ Fᶜ, fourier g (symmDiff x y) ^ 2 = ∑ x ∈ F, ∑ y ∈ Fᶜ, fourier (fun (z : Finset ι) => g z - t) (symmDiff x y) ^ 2

Equation (12): the Fourier kernel across a family boundary is unchanged when a constant is subtracted from the function.

theorem Chvatal.sum_fourier_kernel_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Finset ι → ℝ) (x : Finset ι) : ∑ y : Finset ι, fourier g (symmDiff x y) ^ 2 = cubeMean fun (z : Finset ι) => g z ^ 2

Reindexing the squared Fourier kernel gives the Parseval norm, the first step in equation (13).

theorem Chvatal.boundary_eq_total_sub_interior {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Family ι) (g : Finset ι → ℝ) : ∑ x ∈ F, ∑ y ∈ Fᶜ, fourier g (symmDiff x y) ^ 2 = (↑(Finset.card F) * cubeMean fun (z : Finset ι) => g z ^ 2) - ∑ x ∈ F, ∑ y ∈ F, fourier g (symmDiff x y) ^ 2

Equation (13): boundary energy equals total energy minus interior energy.

theorem Chvatal.boolean_sub_const_norm {ι : Type u_1} [Fintype ι] {g : Finset ι → ℝ} (hg : IsBoolean g) (t : ℝ) : (cubeMean fun (z : Finset ι) => (g z - t) ^ 2) = (1 - t) ^ 2 * cubeMean g + t ^ 2 * (1 - cubeMean g)

A shifted Boolean function's squared norm, used after equation (14).

theorem Chvatal.card_sdiff_div_cube {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F G : Family ι) : ↑(Finset.card (F \ G)) / ↑(Fintype.card (Finset ι)) = cubeMean F.indicator - cubeMean fun (x : Finset ι) => F.indicator x * G.indicator x

The density of a family difference is the difference of the corresponding indicator means, used to convert equation (14) into covariance.

theorem Chvatal.shifted_dimension_covariance {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F G : Family ι) (t : ℝ) : ((↑(Finset.card F) * cubeMean fun (z : Finset ι) => (G.indicator z - t) ^ 2) - (t ^ 2 * ↑(Finset.card (F \ G)) + (1 - t) ^ 2 * ↑(Finset.card (F \ G.dual)))) / ↑(Fintype.card (Finset ι)) = t ^ 2 * covariance F.indicator G.indicator + (1 - t) ^ 2 * covariance F.indicator (dual G.indicator)

The final algebra in Section 3.2: the total shifted norm minus the two auxiliary-family dimensions equals a quadratic combination of covariances.

theorem Chvatal.two_spectral_le_of_interior_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F G : Family ι) (t : ℝ) (hinterior : t ^ 2 * ↑(Finset.card (F \ G)) + (1 - t) ^ 2 * ↑(Finset.card (F \ G.dual)) ≤ ∑ x ∈ F, ∑ y ∈ F, fourier (fun (z : Finset ι) => G.indicator z - t) (symmDiff x y) ^ 2) : 2 * ∑ T : Finset ι, ∑ S : Finset ι with Odd (S ∩ T).card, fourier F.indicator S ^ 2 * fourier G.indicator T ^ 2 ≤ t ^ 2 * covariance F.indicator G.indicator + (1 - t) ^ 2 * covariance F.indicator (dual G.indicator)

The last step of Section 3.2, isolating how the interior-kernel estimate (14) combines with the boundary identities (11)–(13).

theorem Chvatal.two_spectral_le_quadratic_covariance {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f g : Finset ι → ℝ} (hf : IsBoolean f) (hmf : Monotone f) (hg : IsBoolean g) (hmg : Monotone g) (t : ℝ) : 2 * ∑ T : Finset ι, ∑ S : Finset ι with Odd (S ∩ T).card, fourier f S ^ 2 * fourier g T ^ 2 ≤ t ^ 2 * covariance f g + (1 - t) ^ 2 * covariance f (dual g)

Theorem 1.4, equation (3): for every real t, twice the odd-intersection Fourier energy is bounded by the indicated quadratic combination of covariances. The proof includes empty supports and an empty coordinate type.