Sharpness and the two-coordinate counterexample

This file formalizes Proposition 5.1 and Remark 5.2 of arXiv:2609.19123. The AND function is the indicator of the top cube point; OR is its dual.

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

The function AND_n in Section 5: all coordinates must equal one.

Equations

• Chvatal.andFunction x = if x = Finset.univ then 1 else 0

def Chvatal.orFunction {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Finset ι → ℝ

The function OR_n in Section 5, defined as the dual of AND_n.

Equations

• Chvatal.orFunction = Chvatal.dual Chvatal.andFunction

theorem Chvatal.isBoolean_andFunction {ι : Type u_1} [Fintype ι] [DecidableEq ι] : IsBoolean andFunction

AND is Boolean, as required for the sharpness examples in Section 5.

theorem Chvatal.monotone_andFunction {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Monotone andFunction

AND is increasing, as required for Proposition 5.1.

theorem Chvatal.isBoolean_orFunction {ι : Type u_1} [Fintype ι] [DecidableEq ι] : IsBoolean orFunction

OR is Boolean, as required for Remark 5.2.

theorem Chvatal.monotone_orFunction {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Monotone orFunction

OR is increasing, as required for Remark 5.2.

theorem Chvatal.cubeMean_andFunction_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Finset ι → ℝ) : (cubeMean fun (x : Finset ι) => andFunction x * g x) = g Finset.univ / ↑(Fintype.card (Finset ι))

Integrating against AND evaluates at the top point, the counting calculation in Proposition 5.1.

theorem Chvatal.cubeMean_andFunction {ι : Type u_1} [Fintype ι] [DecidableEq ι] : cubeMean andFunction = 1 / ↑(Fintype.card (Finset ι))

The quantity a = 2^{-n} in Proposition 5.1 is the mean of AND.

theorem Chvatal.influence_andFunction {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) : influence andFunction i = 2 / ↑(Fintype.card (Finset ι))

Every coordinate of AND has influence 2a, as computed in Proposition 5.1.

theorem Chvatal.maxInfluence_andFunction {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Finset ι} (hS : S.Nonempty) : maxInfluence andFunction S = 2 / ↑(Fintype.card (Finset ι))

AND has the same maximum influence on every nonempty Fourier index.

theorem Chvatal.spectralWeight_andFunction {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Finset ι → ℝ) : spectralWeight andFunction g = 2 / ↑(Fintype.card (Finset ι)) * covariance g g

Proposition 5.1: the AND spectral weight is 2a times the variance of g.

theorem Chvatal.covariance_self_boolean {ι : Type u_1} [Fintype ι] {g : Finset ι → ℝ} (hg : IsBoolean g) : covariance g g = cubeMean g * (1 - cubeMean g)

The variance of a Boolean function is b(1-b), the Parseval calculation used in Proposition 5.1.

theorem Chvatal.covariance_andFunction {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Finset ι → ℝ) : covariance andFunction g = 1 / ↑(Fintype.card (Finset ι)) * (g Finset.univ - cubeMean g)

The covariance of AND with any function, prior to using the endpoint values in Proposition 5.1.

theorem Chvatal.covariance_andFunction_dual {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Finset ι → ℝ) : covariance andFunction (dual g) = 1 / ↑(Fintype.card (Finset ι)) * (cubeMean g - g ∅)

The covariance of AND with the dual, in the endpoint form used by Proposition 5.1.

theorem Chvatal.monotone_boolean_endpoints {ι : Type u_1} [Fintype ι] {g : Finset ι → ℝ} (hg : IsBoolean g) (hm : Monotone g) : (g = fun (x : Finset ι) => 0) ∨ (g = fun (x : Finset ι) => 1) ∨ g ∅ = 0 ∧ g Finset.univ = 1

An increasing Boolean function is constant or has the two endpoint values used in the nonconstant case of Proposition 5.1.

theorem Chvatal.andFunction_sharp {ι : Type u_1} [Fintype ι] [DecidableEq ι] {g : Finset ι → ℝ} (hg : IsBoolean g) (hm : Monotone g) : spectralWeight andFunction g = 2 * covariance andFunction g * covariance andFunction (dual g) / (covariance andFunction g + covariance andFunction (dual g))

Proposition 5.1: AND attains equality in the harmonic correlation bound for every increasing Boolean second function, including constant functions.

theorem Chvatal.cubeMean_orFunction {ι : Type u_1} [Fintype ι] [DecidableEq ι] : cubeMean orFunction = 1 - 1 / ↑(Fintype.card (Finset ι))

The mean of OR is 1 - 2^{-n}, used in Remark 5.2.

@[simp]

theorem Chvatal.orFunction_empty {ι : Type u_1} [Fintype ι] [DecidableEq ι] : orFunction ∅ = 0

OR vanishes at the bottom cube point, including in dimension zero.

@[simp]

theorem Chvatal.orFunction_univ {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] : orFunction Finset.univ = 1

OR is one at the top when there is at least one coordinate.

theorem Chvatal.and_or_two_example : covariance andFunction orFunction = 1 / 16 ∧ covariance andFunction (dual orFunction) = 3 / 16 ∧ spectralWeight andFunction orFunction = 3 / 32 ∧ covariance andFunction orFunction < spectralWeight andFunction orFunction

Remark 5.2: the exact two-coordinate AND/OR counterexample. The spectral weight exceeds covariance, so removing antipodality from the stronger bound fails.

theorem Chvatal.andFunction_one_antipodal : dual andFunction = andFunction

On a single coordinate AND is antipodal, providing the extremizer for the optimal constant asserted in Proposition 5.1.

theorem Chvatal.andFunction_one_values : covariance andFunction andFunction = 1 / 4 ∧ influence andFunction 0 = 1

The one-coordinate extremizer has covariance one quarter and influence one, so the coefficient in Corollary 1.3 cannot be increased.

theorem Chvatal.andFunction_antipodal_sharp {ι : Type u_1} [Fintype ι] [DecidableEq ι] {g : Finset ι → ℝ} (hg : IsBoolean g) (hm : Monotone g) (hdual : dual g = g) (i : ι) : covariance andFunction g = influence andFunction i / 4

Proposition 5.1, antipodal case: AND attains the factor one quarter for every coordinate and every increasing antipodal Boolean second function.

theorem Chvatal.quarter_coefficient_optimal (c : ℝ) (hc : ∀ (f g : Finset (Fin 1) → ℝ), IsBoolean f → Monotone f → IsBoolean g → Monotone g → dual g = g → c * Finset.univ.inf' ⋯ (influence f) ≤ covariance f g) : c ≤ 1 / 4

Proposition 5.1, optimality: a coefficient valid for all increasing Boolean pairs with an antipodal second function, even just on the one-coordinate cube, cannot exceed 1/4. The finite infimum is the minimum influence from (2).