The signed Boolean formulation

The final paragraph of Section 5 of arXiv:2609.19123 changes conventions from {0,1}-valued functions to {-1,1}-valued functions by h = 2g - 1. This file verifies that conversion, the positive-part and Fourier identities, and the resulting signed version of the weighted star inequality.

def Chvatal.IsSignedBoolean {ι : Type u_1} (h : Finset ι → ℝ) : Prop

A signed Boolean function, with values in {-1,1}, as in Section 5's comparison with Friedgut–Kahn–Kalai–Keller.

Equations

• Chvatal.IsSignedBoolean h = ∀ (x : Finset ι), h x = -1 ∨ h x = 1

def Chvatal.signLift {ι : Type u_1} (g : Finset ι → ℝ) (x : Finset ι) : ℝ

The convention change h = 2g - 1 in the final paragraph of Section 5.

Equations

• Chvatal.signLift g x = 2 * g x - 1

noncomputable def Chvatal.booleanPart {ι : Type u_1} (h : Finset ι → ℝ) (x : Finset ι) : ℝ

The inverse convention change g = (h + 1) / 2 in Section 5.

Equations

• Chvatal.booleanPart h x = (h x + 1) / 2

@[simp]

theorem Chvatal.booleanPart_signLift {ι : Type u_1} (g : Finset ι → ℝ) : booleanPart (signLift g) = g

The signed lift followed by the Boolean conversion is the identity.

@[simp]

theorem Chvatal.signLift_booleanPart {ι : Type u_1} (h : Finset ι → ℝ) : signLift (booleanPart h) = h

The Boolean conversion followed by the signed lift is the identity.

theorem Chvatal.IsBoolean.signLift {ι : Type u_1} {g : Finset ι → ℝ} (hg : IsBoolean g) : IsSignedBoolean (Chvatal.signLift g)

Section 5: a Boolean function becomes a {-1,1}-valued function.

theorem Chvatal.IsSignedBoolean.booleanPart {ι : Type u_1} {h : Finset ι → ℝ} (hh : IsSignedBoolean h) : IsBoolean (Chvatal.booleanPart h)

Conversely every signed Boolean function gives an ordinary Boolean function, so the closing signed formulation has the same scope as the Boolean one.

theorem Chvatal.monotone_signLift {ι : Type u_1} {g : Finset ι → ℝ} (hg : Monotone g) : Monotone (signLift g)

The convention change in Section 5 preserves increasing functions.

theorem Chvatal.monotone_booleanPart {ι : Type u_1} {h : Finset ι → ℝ} (hh : Monotone h) : Monotone (booleanPart h)

The inverse convention change also preserves increasing functions.

theorem Chvatal.signLift_compl {ι : Type u_1} [Fintype ι] [DecidableEq ι] {g : Finset ι → ℝ} (hg : dual g = g) (x : Finset ι) : signLift g xᶜ = -signLift g x

Section 5: a self-dual Boolean function lifts to an odd function under antipodal complementation, h(xᶜ) = -h(x).

theorem Chvatal.dual_booleanPart {ι : Type u_1} [Fintype ι] [DecidableEq ι] {h : Finset ι → ℝ} (hh : ∀ (x : Finset ι), h xᶜ = -h x) : dual (booleanPart h) = booleanPart h

The inverse of the preceding antipodality conversion.

theorem Chvatal.signLift_positivePart_sq {ι : Type u_1} {g : Finset ι → ℝ} (hg : IsBoolean g) (x : Finset ι) : max (signLift g x) 0 ^ 2 = g x

The identity h_+² = g explicitly stated in the final paragraph of Section 5.

theorem Chvatal.IsSignedBoolean.positivePart_sq {ι : Type u_1} {h : Finset ι → ℝ} (hh : IsSignedBoolean h) (x : Finset ι) : max (h x) 0 ^ 2 = Chvatal.booleanPart h x

The positive-part identity for an arbitrary signed Boolean function.

theorem Chvatal.fourier_signLift {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Finset ι → ℝ) (S : Finset ι) : fourier (signLift g) S = 2 * fourier g S - if S = ∅ then 1 else 0

Fourier coefficients under the affine convention change of Section 5, including the exceptional constant coefficient.

theorem Chvatal.fourier_signLift_of_nonempty {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Finset ι → ℝ) {S : Finset ι} (hS : S.Nonempty) : fourier (signLift g) S = 2 * fourier g S

Section 5's formula ĥ(S) = 2ĝ(S) for every nonempty Fourier index.

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

The coefficients in the final displayed equation of Section 5, in the signed Boolean convention. Choosing orderedSelector gives the paper's order.

Equations

• Chvatal.signedSpectralWeights h select i = ∑ S ∈ Finset.univ.erase ∅, if select S = i then Chvatal.fourier h S ^ 2 else 0

theorem Chvatal.spectralWeights_eq_signed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Finset ι → ℝ) (select : Finset ι → ι) (i : ι) : spectralWeights g select i = signedSpectralWeights (signLift g) select i

Section 5: the signed Fourier formula gives exactly the same coefficients λ_i as Proposition 5.3, with its factor of four absorbed by the convention change.

theorem Chvatal.signedSpectralWeights_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (h : Finset ι → ℝ) (select : Finset ι → ι) (i : ι) : 0 ≤ signedSpectralWeights h select i

Nonnegativity of the signed coefficients in the closing Section 5 formulation.

theorem Chvatal.sum_signedSpectralWeights {ι : Type u_1} [Fintype ι] [DecidableEq ι] {h : Finset ι → ℝ} (hh : IsSignedBoolean h) (hanti : ∀ (x : Finset ι), h xᶜ = -h x) (select : Finset ι → ι) : ∑ i : ι, signedSpectralWeights h select i = 1

The signed coefficients sum to one for every antipodal signed Boolean function.

theorem Chvatal.signed_weighted_star_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {h : Finset ι → ℝ} (hh : IsSignedBoolean h) (hm : Monotone h) (hanti : ∀ (x : Finset ι), h xᶜ = -h x) (select : Finset ι → ι) (hselect : ∀ (S : Finset ι), S.Nonempty → select S ∈ S) (ω : Finset ι → ℝ) (hω : ∀ (x : Finset ι), 0 ≤ ω x) (hωanti : Antitone ω) : ∑ x : Finset ι, max (h x) 0 ^ 2 * ω x ≤ ∑ i : ι, signedSpectralWeights h select i * ∑ x ∈ Family.star Finset.univ i, ω x

The weighted star inequality in the signed Boolean convention of Section 5's closing paragraph. Its left side uses exactly the stated positive-part square, and its coefficients use the stated squared signed Fourier coefficients.