Chvátal's conjecture and the sharp correlation inequality

The main results of Chang–Liu–Liu, arXiv:2609.19123v1:

• sharp_correlation: Theorem 1.2, the sharp harmonic-mean bound.
• antipodal_correlation: Corollary 1.3, the minimum-influence bound.
• chvatal: Theorem 1.1, the star bound for hereditary families.

Theorem 1.4 is two_spectral_le_quadratic_covariance in Chvatal.Correlation. The analytic statements allow an empty coordinate type. Statements involving a minimum coordinate or a star center explicitly require a nonempty coordinate type.

theorem Chvatal.covariance_nonneg {ι : Type u_1} [Fintype ι] {f g : Finset ι → ℝ} (hf : IsBoolean f) (hmf : Monotone f) (hg : IsBoolean g) (hmg : Monotone g) : 0 ≤ covariance f g

Nonnegativity of covariance for increasing Boolean functions, recalled after Theorem 1.2. Here it follows directly by setting t = 1 in Theorem 1.4.

theorem Chvatal.sharp_correlation {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f g : Finset ι → ℝ} (hf : IsBoolean f) (hmf : Monotone f) (hg : IsBoolean g) (hmg : Monotone g) : spectralWeight f g ≤ 2 * covariance f g * covariance f (dual g) / (covariance f g + covariance f (dual g))

Theorem 1.2, equation (1): the sharp correlation inequality. The denominator-zero convention in the paper agrees with Lean's real division.

theorem Chvatal.antipodal_spectral_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f g : Finset ι → ℝ} (hf : IsBoolean f) (hmf : Monotone f) (hg : IsBoolean g) (hmg : Monotone g) (hdual : dual g = g) : spectralWeight f g ≤ covariance f g

The antipodal specialization of Theorem 1.2 used in Corollary 1.3 and Proposition 5.3.

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

The minimum coordinate influence appearing in Corollary 1.3. A nonempty coordinate type is required to choose a minimum.

Equations

• Chvatal.minInfluence f = Finset.univ.inf' ⋯ (Chvatal.influence f)

theorem Chvatal.minInfluence_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (f : Finset ι → ℝ) (i : ι) : minInfluence f ≤ influence f i

The minimum influence is no larger than any coordinate influence.

theorem Chvatal.antipodal_correlation {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {f g : Finset ι → ℝ} (hf : IsBoolean f) (hmf : Monotone f) (hg : IsBoolean g) (hmg : Monotone g) (hdual : dual g = g) : minInfluence f / 4 ≤ covariance f g

Corollary 1.3, equation (2): the Friedgut–Kahn–Kalai–Keller correlation bound.

theorem Chvatal.antipodal_correlation_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] : AntipodalCorrelationBound ι

Corollary 1.3 in the existential coordinate form used by the Section 4 counting reduction.

theorem Chvatal.chvatal {ι : Type u_1} [DecidableEq ι] [Finite ι] [Nonempty ι] {D A : Family ι} (hD : D.IsHereditary) (hAD : A ⊆ D) (hA : A.IsIntersecting) : ∃ (i : ι), Finset.card A ≤ Finset.card (D.star i)

Theorem 1.1: every intersecting subfamily of a hereditary family is bounded in cardinality by a star of that hereditary family.

theorem Chvatal.exists_largest_intersecting_star {ι : Type u_1} [DecidableEq ι] [Finite ι] [Nonempty ι] {D : Family ι} (hD : D.IsHereditary) : ∃ (i : ι), (D.star i).IsIntersecting ∧ ∀ A ⊆ D, A.IsIntersecting → Finset.card A ≤ Finset.card (D.star i)

The abstract's formulation of Theorem 1.1: a single star is a largest intersecting subfamily of the given hereditary family.