Walsh–Fourier analysis on the uniform cube and the KKL reduction

Definition\(\pm 1\) value of a bit#✓fully proved

The ±1 value of a bit: false ↦ 1, true ↦ -1.

def khc_sign (b : Bool) : ℝ := if b then -1 else 1

Used by 6

Used byBonami–Beckner applied to a discrete derivative · \(p\)-biased character at \(p = 1/2\) is the Walsh character up to sign · Normalized bit at \(p = 1/2\) is \(-(-1)^b\) · Walsh character on the Boolean cube · Walsh character agrees with the canonical cube character up to sign · Reindexing a Walsh character reindexes its coordinate set

DefinitionWalsh character on the Boolean cube#✓fully proved

The Walsh character χ_S(x) = ∏_{i ∈ S} (-1)^{x i} on {0, 1}^ι.

This legacy sign convention is retained for KKL consumers; its proofs use BooleanCube.cubeChi through khc_walshChar_eq_cubeChi.

noncomputable def khc_walshChar (S : Finset ι) (x : ι → Bool) : ℝ :=
  ∏ i ∈ S, khc_sign (x i)

Uses 1 · Used by 12

Statement uses\(\pm 1\) value of a bit

Used byBonami–Beckner applied to a discrete derivative · Bonami–Beckner bound for indicator functions · Bound on \(m - m^{2/(1+\rho^2)}\) by total influence · Squared \(p\)-biased and Walsh coefficients agree at \(p = 1/2\) · \(p\)-biased character at \(p = 1/2\) is the Walsh character up to sign · Fourier–Walsh coefficient under the uniform measure · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier coefficients are invariant under reindexing · Fourier inversion on the Boolean cube · Noise operator is diagonal in the Walsh basis · Walsh character agrees with the canonical cube character up to sign · Reindexing a Walsh character reindexes its coordinate set

DefinitionFourier–Walsh coefficient under the uniform measure#✓fully proved

The Fourier–Walsh coefficient f̂(S) = 𝔼[f χ_S] under the uniform measure.

This retains the legacy signs; khc_fourierCoeff_eq_boolFourierCoeff transports the canonical Fourier identities used below.

noncomputable def khc_fourierCoeff (f : (ι → Bool) → ℝ) (S : Finset ι) : ℝ :=
  bnt_uexp (fun x => f x * khc_walshChar S x)

Uses 2 · Used by 33

Statement usesUniform expectation on the Boolean cube · Walsh character on the Boolean cube

Used bySum of influence powers capped by the maximal influence · Capped per-coordinate hypercontractive estimate · Capped-estimate form of KKL implies the indicator-bound form · Bonami–Beckner applied to a discrete derivative · Fourier-form KKL at \(p = 1/2\) conditional on the capped estimate · Conditional Fourier-form KKL holds trivially with constant zero · Summed per-coordinate Bonami–Beckner bound · Bonami–Beckner bound for indicator functions · Fourier-form KKL inequality given the indicator Bonami–Beckner bound · Indicator-bound form of KKL implies the hypercontractive form · Indicator-bound form of KKL with constant 0 holds trivially · Poincaré inequality in Fourier form · Fourier-form KKL inequality given the measure–influence bound · Measure–influence form of KKL with constant 0 holds trivially · Edge-isoperimetric inequality · Measure–influence form of KKL implies the indicator-bound form · Bound on \(m - m^{2/(1+\rho^2)}\) by total influence · Squared \(p\)-biased and Walsh coefficients agree at \(p = 1/2\) · Total influence at \(p = 1/2\) via \(p\)-biased Fourier coefficients · Capped estimate rewritten in the variable \(u = 1 - \rho^2\) · KKL inequality · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier coefficients are invariant under reindexing · Fourier inversion on the Boolean cube · Influence of a coordinate as Fourier weight · Hypercontractive form of KKL implies the KKL inequality at \(p = 1/2\) · Fourier-form KKL inequality given the hypercontractive bound · Hypercontractive form of KKL with constant 0 holds trivially · Hypercontractivity in Fourier form · Noise operator is diagonal in the Walsh basis · Parseval's identity on the Boolean cube · Total influence as Fourier weight · Variance as Fourier weight off the empty set

DefinitionReindexing a cube function along an index bijection#✓fully proved

The function f on {0, 1}^ι transported to {0, 1}^κ along the bijection e : κ ≃ ι.

noncomputable def khc_reindex {κ : Type*} (e : κ ≃ ι) (f : (ι → Bool) → ℝ) :
    (κ → Bool) → ℝ :=
  fun y => f (fun i => y (e.symm i))

Used by 14

Used byBonami–Beckner applied to a discrete derivative · Fourier coefficients are invariant under reindexing · Fourier inversion on the Boolean cube · Bonami–Beckner hypercontractive inequality · Event influence is four times the canonical influence · Influence of a coordinate as Fourier weight · Hypercontractivity in Fourier form · Noise operator is diagonal in the Walsh basis · Parseval's identity on the Boolean cube · Reindexing preserves values at corresponding cube points · Total influence as Fourier weight · Variance as Fourier weight off the empty set · Reindexing a Walsh character reindexes its coordinate set · Fourier form of \(p\)-biased hypercontractivity on finite index types

DefinitionCube bijection induced by an index bijection#✓fully proved

The bijection {0, 1}^ι ≃ {0, 1}^κ induced by e : κ ≃ ι.

def khc_cubeEquiv {κ : Type*} (e : κ ≃ ι) : (ι → Bool) ≃ (κ → Bool) :=
  Equiv.arrowCongr e.symm (Equiv.refl Bool)

Used by 11

Used byBonami–Beckner applied to a discrete derivative · Fourier coefficients are invariant under reindexing · Fourier inversion on the Boolean cube · Bonami–Beckner hypercontractive inequality · Event influence is four times the canonical influence · Hypercontractivity in Fourier form · Noise operator is diagonal in the Walsh basis · Parseval's identity on the Boolean cube · Reindexing preserves values at corresponding cube points · Variance as Fourier weight off the empty set · Fourier form of \(p\)-biased hypercontractivity on finite index types

TheoremWalsh character agrees with the canonical cube character up to sign#✓fully proved

On Fin n, the Walsh character is BooleanCube.cubeChi up to the sign (-1)^{|S|}: BooleanCube.cubeVal sends true to 1, while khc_sign sends it to -1.

theorem khc_walshChar_eq_cubeChi {n : ℕ} (S : Finset (Fin n)) (x : Fin n → Bool) :
    khc_walshChar S x = (-1) ^ S.card * BooleanCube.cubeChi n S x

Uses 4 · Used by 4

Statement usesFourier character on the Boolean cube · Walsh character on the Boolean cube

Proof usesSign of a Boolean coordinate · \(\pm 1\) value of a bit

Used byBonami–Beckner applied to a discrete derivative · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier inversion on the Boolean cube · Noise operator is diagonal in the Walsh basis

TheoremWalsh coefficient is the canonical Fourier coefficient up to sign#✓fully proved

On Fin n, the Fourier coefficient is BooleanCube.boolFourierCoeff up to the sign (-1)^{|S|}.

theorem khc_fourierCoeff_eq_boolFourierCoeff {n : ℕ} (f : (Fin n → Bool) → ℝ)
    (S : Finset (Fin n)) :
    khc_fourierCoeff f S = (-1) ^ S.card * BooleanCube.boolFourierCoeff n f S

Uses 8 · Used by 7

Statement usesFourier coefficient on the Boolean cube · Fourier–Walsh coefficient under the uniform measure

Proof usesBoolean cube · Number of points of the Boolean cube · Fourier character on the Boolean cube · Uniform expectation on the Boolean cube · Walsh character on the Boolean cube · Walsh character agrees with the canonical cube character up to sign

Used byFourier inversion on the Boolean cube · Influence of a coordinate as Fourier weight · Hypercontractivity in Fourier form · Noise operator is diagonal in the Walsh basis · Parseval's identity on the Boolean cube · Total influence as Fourier weight · Variance as Fourier weight off the empty set

TheoremReindexing a Walsh character reindexes its coordinate set#✓fully proved

Reindexing a Walsh character reindexes its finite set of coordinates.

theorem khc_walshChar_reindex {κ : Type*} (e : ι ≃ κ) (S : Finset ι) :
    khc_reindex e.symm (khc_walshChar S) = khc_walshChar (e.finsetCongr S)

Uses 3 · Used by 4

Statement usesReindexing a cube function along an index bijection · Walsh character on the Boolean cube

Proof uses\(\pm 1\) value of a bit

Used byBonami–Beckner applied to a discrete derivative · Fourier coefficients are invariant under reindexing · Fourier inversion on the Boolean cube · Noise operator is diagonal in the Walsh basis

TheoremReindexing preserves values at corresponding cube points#✓fully proved

Reindexing back at the corresponding cube point recovers the original value.

theorem khc_reindex_cubeEquiv {κ : Type*} (e : κ ≃ ι) (f : (ι → Bool) → ℝ)
    (x : ι → Bool) : khc_reindex e f (khc_cubeEquiv e x) = f x

Uses 2 · Used by 3

Statement usesCube bijection induced by an index bijection · Reindexing a cube function along an index bijection

Used byBonami–Beckner applied to a discrete derivative · Fourier inversion on the Boolean cube · Noise operator is diagonal in the Walsh basis

TheoremFourier coefficients are invariant under reindexing#✓fully proved

Fourier coefficients are unchanged when both the function and its index are reindexed.

theorem khc_fourierCoeff_reindex {κ : Type*} [Fintype κ] [DecidableEq κ]
    (e : ι ≃ κ) (f : (ι → Bool) → ℝ) (S : Finset ι) :
    khc_fourierCoeff (khc_reindex e.symm f) (e.finsetCongr S) = khc_fourierCoeff f S

Uses 6 · Used by 7

Statement usesFourier–Walsh coefficient under the uniform measure · Reindexing a cube function along an index bijection

Proof usesUniform expectation on the Boolean cube · Cube bijection induced by an index bijection · Walsh character on the Boolean cube · Reindexing a Walsh character reindexes its coordinate set

Used byFourier inversion on the Boolean cube · Influence of a coordinate as Fourier weight · Hypercontractivity in Fourier form · Noise operator is diagonal in the Walsh basis · Parseval's identity on the Boolean cube · Total influence as Fourier weight · Variance as Fourier weight off the empty set

TheoremFourier inversion on the Boolean cube#✓fully proved

Fourier inversion: f = ∑_S f̂(S) χ_S.

theorem khc_fourier_expansion (f : (ι → Bool) → ℝ) (x : ι → Bool) :
    (∑ S : Finset ι, khc_fourierCoeff f S * khc_walshChar S x) = f x

Uses 12 · Used by 1

Statement usesFourier–Walsh coefficient under the uniform measure · Walsh character on the Boolean cube

Proof usesFourier coefficient on the Boolean cube · Fourier character on the Boolean cube · Fourier inversion on the Boolean cube · Cube bijection induced by an index bijection · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier coefficients are invariant under reindexing · Reindexing a cube function along an index bijection · Reindexing preserves values at corresponding cube points · Walsh character agrees with the canonical cube character up to sign · Reindexing a Walsh character reindexes its coordinate set

Used byBonami–Beckner applied to a discrete derivative

TheoremParseval's identity on the Boolean cube#✓fully proved

Parseval's identity: 𝔼[f g] = ∑_S f̂(S) ĝ(S).

Transported from BooleanCube.expect_mul_eq_sum_boolFourierCoeff_mul.

theorem khc_parseval (f g : (ι → Bool) → ℝ) :
    bnt_uexp (fun x => f x * g x)
      = ∑ S : Finset ι, khc_fourierCoeff f S * khc_fourierCoeff g S

Uses 10 · Used by 1

Statement usesUniform expectation on the Boolean cube · Fourier–Walsh coefficient under the uniform measure

Proof usesBoolean cube · Fourier coefficient on the Boolean cube · Plancherel's identity on the Boolean cube · Uniform expectation on the cube equals the finite average · Cube bijection induced by an index bijection · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier coefficients are invariant under reindexing · Reindexing a cube function along an index bijection

Used byBound on \(m - m^{2/(1+\rho^2)}\) by total influence

TheoremNoise operator is diagonal in the Walsh basis#✓fully proved

The noise operator acts diagonally on the Walsh basis: T_ρ f = ∑_S ρ^{|S|} f̂(S) χ_S.

Transported from BooleanCube.boolNoiseOp_eq_sum, for every real ρ.

theorem khc_noiseOp_fourier (ρ : ℝ) (f : (ι → Bool) → ℝ) :
    bnt_noiseOp ρ f
      = fun x => ∑ S : Finset ι, (ρ ^ S.card * khc_fourierCoeff f S) * khc_walshChar S x

Uses 16

Statement usesNoise operator on the Boolean cube · Fourier–Walsh coefficient under the uniform measure · Walsh character on the Boolean cube

Proof usesFourier coefficient on the Boolean cube · Noise operator on the Boolean cube · Fourier expansion of the noise operator · Fourier character on the Boolean cube · Noise kernel on the Boolean cube · Agreement of the two noise operators on the Boolean cube · Cube bijection induced by an index bijection · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier coefficients are invariant under reindexing · Reindexing a cube function along an index bijection · Reindexing preserves values at corresponding cube points · Walsh character agrees with the canonical cube character up to sign · Reindexing a Walsh character reindexes its coordinate set

TheoremBonami–Beckner hypercontractive inequality#✓fully proved

Bonami–Beckner hypercontractive inequality (A. Bonami, Étude des coefficients de Fourier des fonctions de Lᵖ(G), Ann. Inst. Fourier 1970; W. Beckner, Inequalities in Fourier analysis, Ann. of Math. 1975): ‖T_ρ g‖₂ ≤ ‖g‖_{1+ρ²} on {0, 1}^ι for 0 ≤ ρ ≤ 1.

theorem khc_hypercontractivity_general {ρ : ℝ} (h0 : 0 ≤ ρ) (h1 : ρ ≤ 1)
    (g : (ι → Bool) → ℝ) :
    bnt_qnorm 2 (bnt_noiseOp ρ g) ≤ bnt_qnorm (1 + ρ ^ 2) g

Uses 9 · Used by 2

Statement usesNoise operator on the Boolean cube · \(L^q\) norm under the uniform measure on the cube

Proof usesHypercontractivity from the vector two-point inequality · Noise kernel on the Boolean cube · q-th moment under the uniform measure on the cube · Uniform expectation on the Boolean cube · Cube bijection induced by an index bijection · Reindexing a cube function along an index bijection · Vector two-point inequality for nonnegative noise

Used byBonami–Beckner applied to a discrete derivative · Hypercontractivity in Fourier form

TheoremHypercontractivity in Fourier form#✓fully proved

Hypercontractivity in Fourier form: ∑_S ρ^{2|S|} f̂(S)² ≤ ‖f‖²_{1+ρ²}.

theorem khc_lowDegreeWeight_le {ρ : ℝ} (h0 : 0 ≤ ρ) (h1 : ρ ≤ 1)
    (f : (ι → Bool) → ℝ) :
    (∑ S : Finset ι, (ρ ^ S.card) ^ 2 * (khc_fourierCoeff f S) ^ 2)
      ≤ (bnt_qnorm (1 + ρ ^ 2) f) ^ 2

Uses 18 · Used by 2

Statement uses\(L^q\) norm under the uniform measure on the cube · Fourier–Walsh coefficient under the uniform measure

Proof usesBoolean cube · Fourier coefficient on the Boolean cube · Fourier coefficients of the noise operator · Noise operator on the Boolean cube · Parseval's identity on the Boolean cube · Noise kernel on the Boolean cube · Noise operator on the Boolean cube · Agreement of the two noise operators on the Boolean cube · q-th moment under the uniform measure on the cube · Uniform expectation on the Boolean cube · Uniform expectation on the cube equals the finite average · Cube bijection induced by an index bijection · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier coefficients are invariant under reindexing · Bonami–Beckner hypercontractive inequality · Reindexing a cube function along an index bijection

Used byBonami–Beckner bound for indicator functions · Hypercontractive form of KKL implies the KKL inequality at \(p = 1/2\)

TheoremVariance as Fourier weight off the empty set#✓fully proved

Variance under the uniform measure is the Fourier weight off the empty set.

theorem khc_var_eq_fourierWeight (g : ConfigSpace ι → ℝ) :
    OSSS.var (OSSS.bernoulliWeight (1 / 2 : ℝ)) g
      = ∑ S ∈ (univ.erase (∅ : Finset ι)), (khc_fourierCoeff g S) ^ 2

Uses 18 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Variance under a product weight · Fourier–Walsh coefficient under the uniform measure

Proof usesBoolean cube · Fourier coefficient on the Boolean cube · Variance on the Boolean cube · Variance as mean square minus squared mean · Variance in terms of Fourier coefficients · Covariance under a product weight · Expectation under a product weight · Probability of a configuration under a product weight · Uniform expectation on the Boolean cube · Uniform expectation on the cube equals the finite average · Cube bijection induced by an index bijection · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier coefficients are invariant under reindexing · Reindexing a cube function along an index bijection

Used byHypercontractive form of KKL implies the KKL inequality at \(p = 1/2\)

TheoremEvent influence is four times the canonical influence#✓fully proved

Event influence is four times canonical quarter-square influence after reindexing.

theorem khc_infl_eq_four_boolInfluence {n : ℕ} (e : ι ≃ Fin n)
    (φ : ConfigSpace ι → Bool) (i : ι) :
    OSSS.infl (OSSS.bernoulliWeight (1 / 2 : ℝ))
        (fun x => if φ x then (1 : ℝ) else 0) i =
      4 * BooleanCube.boolInfluence
        (khc_reindex e.symm (fun x => if φ x then (1 : ℝ) else 0)) (e i)

Uses 14 · Used by 2

Statement usesInfluence of a coordinate · Configuration space of a statistical-mechanics model · Bernoulli product weight · Influence of a coordinate · Reindexing a cube function along an index bijection

Proof usesBoolean cube · Coordinate flip on the Boolean cube · Expectation under a product weight · Probability of a configuration under a product weight · Uniform expectation on the Boolean cube · Uniform expectation on the cube equals the finite average · Cube bijection induced by an index bijection · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byInfluence of a coordinate as Fourier weight · Total influence as Fourier weight

TheoremInfluence of a coordinate as Fourier weight#✓fully proved

The influence of e on a Boolean function is ∑_{S ∋ e} 4 f̂(S)².

theorem khc_infl_eq_fourierWeight (φ : ConfigSpace ι → Bool) (e : ι) :
    OSSS.infl (OSSS.bernoulliWeight (1 / 2 : ℝ)) (fun ω => if φ ω then (1 : ℝ) else 0) e
      = ∑ S ∈ univ.filter (fun S : Finset ι => e ∈ S),
          4 * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2

Uses 11

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Influence of a coordinate · Fourier–Walsh coefficient under the uniform measure

Proof usesFourier coefficient on the Boolean cube · Influence of a coordinate · Fourier formula for influence · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier coefficients are invariant under reindexing · Event influence is four times the canonical influence · Reindexing a cube function along an index bijection

TheoremTotal influence as Fourier weight#✓fully proved

The total influence of a Boolean function is ∑_S 4 |S| f̂(S)².

theorem khc_totalInfl_eq_fourierWeight (φ : ConfigSpace ι → Bool) :
    totalInfl (OSSS.bernoulliWeight (1 / 2 : ℝ)) (fun ω => if φ ω then (1 : ℝ) else 0)
      = ∑ S : Finset ι, 4 * (S.card : ℝ)
          * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2

Uses 14 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Fourier–Walsh coefficient under the uniform measure · Total influence under a product weight

Proof usesBoolean cube · Fourier coefficient on the Boolean cube · Influence of a coordinate · Total influence on the Boolean cube · Total influence in Fourier form · Influence of a coordinate · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier coefficients are invariant under reindexing · Event influence is four times the canonical influence · Reindexing a cube function along an index bijection

Used bySum of influence powers capped by the maximal influence · Total influence at \(p = 1/2\) via \(p\)-biased Fourier coefficients · Hypercontractive form of KKL implies the KKL inequality at \(p = 1/2\) · Hypercontractive form of KKL with constant 0 holds trivially

DefinitionFourier-form KKL inequality given the hypercontractive bound#✓fully proved

The KKL inequality at p = 1/2 in Fourier form, with the hypercontractive bound as a hypothesis: for every Boolean φ, if ∑_S ρ^{2|S|} f̂(S)² ≤ ‖f‖²_{1+ρ²} for all ρ ∈ [0, 1], then c · ∑_{S ≠ ∅} f̂(S)² · log (1 / maxₑ Infₑ(f)) ≤ ∑_S 4 |S| f̂(S)², where f = 1_φ. The hypothesis always holds (khc_lowDegreeWeight_le).

def khc_LogSobolevStep (c : ℝ) : Prop :=
  ∀ {E : Type} [Fintype E] [DecidableEq E] [Nonempty E] (φ : ConfigSpace E → Bool),
    (∀ ρ : ℝ, 0 ≤ ρ → ρ ≤ 1 →
        (∑ S : Finset E, (ρ ^ S.card) ^ 2
            * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
          ≤ (bnt_qnorm (1 + ρ ^ 2) (fun ω => if φ ω then (1 : ℝ) else 0)) ^ 2) →
      c * (∑ S ∈ (univ.erase (∅ : Finset E)),
            (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
          * Real.log (1 / maxInfl (OSSS.bernoulliWeight (1 / 2 : ℝ))
              (fun ω => if φ ω then (1 : ℝ) else 0))
        ≤ ∑ S : Finset E, 4 * (S.card : ℝ)
            * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2

Uses 5 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · \(L^q\) norm under the uniform measure on the cube · Fourier–Walsh coefficient under the uniform measure · Maximal influence under a product weight

Used byIndicator-bound form of KKL implies the hypercontractive form · Hypercontractive form of KKL implies the KKL inequality at \(p = 1/2\) · Hypercontractive form of KKL with constant 0 holds trivially

TheoremHypercontractive form of KKL with constant 0 holds trivially#✓fully proved

khc_LogSobolevStep 0 holds trivially.

theorem khc_logSobolevStep_zero : khc_LogSobolevStep 0

Uses 14

Statement usesFourier-form KKL inequality given the hypercontractive bound

Proof usesConfiguration space of a statistical-mechanics model · Product probability weight · Bernoulli product weight · Expectation under a product weight · Influence of a coordinate · Probability of a configuration under a product weight · \(L^q\) norm under the uniform measure on the cube · Fourier–Walsh coefficient under the uniform measure · Total influence as Fourier weight · Maximal influence under a product weight · Total influence under a product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

TheoremHypercontractive form of KKL implies the KKL inequality at \(p = 1/2\)#✓fully proved

The Fourier form khc_LogSobolevStep c implies the KKL inequality KKLHypercontractive (1/2) c.

theorem khc_KKL {c : ℝ} (H : khc_LogSobolevStep c) :
    KKLHypercontractive (1 / 2 : ℝ) c

Uses 11 · Used by 1

Statement usesKKL inequality with constant \(c\) for the \(p\)-biased measure · Fourier-form KKL inequality given the hypercontractive bound

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Variance under a product weight · Fourier–Walsh coefficient under the uniform measure · Hypercontractivity in Fourier form · Total influence as Fourier weight · Variance as Fourier weight off the empty set · Maximal influence under a product weight · Total influence under a product weight

Used byIndicator-bound form of KKL implies the KKL inequality at \(p = 1/2\)

TheoremUniform variance agrees with the canonical Boolean variance#✓fully proved

On Fin n, the variance under the uniform product weight is BooleanCube.boolVariance.

theorem khc_var_half_eq_boolVariance {n : ℕ} (f : (Fin n → Bool) → ℝ) :
    OSSS.var (OSSS.bernoulliWeight (1 / 2 : ℝ)) f = BooleanCube.boolVariance f

Uses 11

Statement usesVariance on the Boolean cube · Bernoulli product weight · Variance under a product weight

Proof usesBoolean cube · Variance as mean square minus squared mean · Uniform average over the Boolean cube as a sum · Configuration space of a statistical-mechanics model · Covariance under a product weight · Expectation under a product weight · Probability of a configuration under a product weight · Uniform expectation on the Boolean cube

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.