Boolean functions and coordinate influences

This file formalizes the influence convention in Section 2, equation (6), and the influence comparison of Lemma 3.3 of Chang–Liu–Liu, arXiv:2609.19123v1. Boolean functions are real-valued functions with an explicit IsBoolean hypothesis; this makes their Fourier transforms ordinary real-valued transforms. Increasing functions use mathlib's Monotone predicate on finite subsets ordered by inclusion.

def Chvatal.IsBoolean {ι : Type u_1} (f : Finset ι → ℝ) : Prop

Section 2: a real-valued cube function is Boolean when every value is zero or one.

Equations

• Chvatal.IsBoolean f = ∀ (x : Finset ι), f x = 0 ∨ f x = 1

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

The sign 2xᵢ - 1 used in the influence identity (6).

Equations

• Chvatal.coordinateSign i x = if i ∈ x then 1 else -1

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

Section 2: influence, written as mean squared change under a single-coordinate flip. For Boolean functions this is the probability that the value changes; see influence_eq_mean_indicator.

Equations

• Chvatal.influence f i = Chvatal.cubeMean fun (x : Finset ι) => (f x - f (symmDiff x {i})) ^ 2

theorem Chvatal.IsBoolean.dual {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Finset ι → ℝ} (hf : IsBoolean f) : IsBoolean (Chvatal.dual f)

The Boolean duality operation of Section 2 preserves Boolean values.

theorem Chvatal.monotone_dual {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Finset ι → ℝ} (hf : Monotone f) : Monotone (dual f)

The duality operation of Section 2 preserves monotonicity.

theorem Chvatal.IsBoolean.nonneg {ι : Type u_1} {f : Finset ι → ℝ} (hf : IsBoolean f) (x : Finset ι) : 0 ≤ f x

Boolean values lie in the unit interval; used in the pointwise estimates of Section 3.

theorem Chvatal.IsBoolean.sq {ι : Type u_1} {f : Finset ι → ℝ} (hf : IsBoolean f) (x : Finset ι) : f x ^ 2 = f x

Squaring a Boolean value leaves it unchanged, as used in Parseval's variance formula.

theorem Chvatal.influence_eq_mean_indicator {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Finset ι → ℝ} (hf : IsBoolean f) (i : ι) : influence f i = cubeMean fun (x : Finset ι) => if f x ≠ f (symmDiff x {i}) then 1 else 0

For Boolean functions the squared-change definition equals the probability definition of influence in Section 2.

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

Influences are nonnegative, including in the degenerate cases of Theorem 1.2.

theorem Chvatal.coordinateSign_symmDiff {ι : Type u_1} [DecidableEq ι] {T : Finset ι} {i : ι} (hi : i ∈ T) (x : Finset ι) : coordinateSign i (symmDiff x T) = -coordinateSign i x

Flipping a set containing i reverses 2xᵢ - 1, as in the proof of Lemma 3.3.

theorem Chvatal.signed_mean_flip {ι : Type u_1} [Fintype ι] [DecidableEq ι] {T : Finset ι} {i : ι} (hi : i ∈ T) (f : Finset ι → ℝ) : (cubeMean fun (x : Finset ι) => coordinateSign i x * f (symmDiff x T)) = -cubeMean fun (x : Finset ι) => coordinateSign i x * f x

The change of variables in the proof of Lemma 3.3 negates the signed mean.

theorem Chvatal.signed_mean_difference {ι : Type u_1} [Fintype ι] [DecidableEq ι] {T : Finset ι} {i : ι} (hi : i ∈ T) (f : Finset ι → ℝ) : (cubeMean fun (x : Finset ι) => coordinateSign i x * (f x - f (symmDiff x T))) = 2 * cubeMean fun (x : Finset ι) => coordinateSign i x * f x

The signed difference formula in the proof of Lemma 3.3, before using Boolean values.

theorem Chvatal.flip_sq_eq_signed_difference {ι : Type u_1} [DecidableEq ι] {f : Finset ι → ℝ} (hf : IsBoolean f) (hm : Monotone f) (i : ι) (x : Finset ι) : (f x - f (symmDiff x {i})) ^ 2 = coordinateSign i x * (f x - f (symmDiff x {i}))

Equation (6), pointwise form: monotonicity fixes the sign of a single-coordinate change.

theorem Chvatal.influence_eq_signed_mean {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Finset ι → ℝ} (hf : IsBoolean f) (hm : Monotone f) (i : ι) : influence f i = 2 * cubeMean fun (x : Finset ι) => coordinateSign i x * f x

Equation (6): influence of an increasing Boolean function equals twice its signed mean.

theorem Chvatal.signed_difference_le_sq {ι : Type u_1} [DecidableEq ι] {f : Finset ι → ℝ} (hf : IsBoolean f) (i : ι) (x y : Finset ι) : coordinateSign i x * (f x - f y) ≤ (f x - f y) ^ 2

The pointwise Boolean estimate in Lemma 3.3: a signed change is at most its square.

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

Lemma 3.3, inequality in (15), for each coordinate in the flipped set. Taking the maximum over these coordinates gives exactly the paper's formulation.

theorem Chvatal.mean_eq_half_of_antipodal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {g : Finset ι → ℝ} (hg : dual g = g) : cubeMean g = 1 / 2

Corollary 1.3: an antipodal Boolean function has mean one half.

theorem Chvatal.variance_eq_quarter_of_antipodal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {g : Finset ι → ℝ} (hb : IsBoolean g) (hg : dual g = g) : covariance g g = 1 / 4

Corollary 1.3: an antipodal Boolean function has variance one quarter.