Tensorization of two-point hypercontractivity on the uniform cube

DefinitionUniform expectation on the Boolean cube#✓fully proved

The expectation of f under the uniform measure on ι → Bool. This is 𝔼 ω, f ω (Finset.expect).

noncomputable def bnt_uexp (f : (ι → Bool) → ℝ) : ℝ :=
  (∑ ω : ι → Bool, f ω) / (2 ^ (Fintype.card ι))

Used by 26

Used byCapped-estimate form of KKL implies the indicator-bound form · Bonami–Beckner applied to a discrete derivative · Bonami–Beckner bound for indicator functions · Fourier-form KKL inequality given the indicator Bonami–Beckner bound · Indicator-bound form of KKL with constant 0 holds trivially · 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\) · Fourier–Walsh coefficient under the uniform measure · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier coefficients are invariant under reindexing · Bonami–Beckner hypercontractive inequality · Event influence is four times the canonical influence · Hypercontractivity in Fourier form · Parseval's identity on the Boolean cube · Variance as Fourier weight off the empty set · Uniform variance agrees with the canonical Boolean variance · Vector two-point inequality for nonnegative noise · Hypercontractivity from the vector two-point inequality · Hypercontractivity from the tensorization step · q-th moment under the uniform measure on the cube · Vector two-point inequality implies the tensorization step · Uniform expectation on the cube equals the finite average

Definitionq-th moment under the uniform measure on the cube#✓fully proved

E|f|^q under the uniform measure.

noncomputable def bnt_qnormPow (q : ℝ) (f : (ι → Bool) → ℝ) : ℝ :=
  bnt_uexp (fun ω => |f ω| ^ q)

Uses 1 · Used by 10

Statement usesUniform expectation on the Boolean cube

Used byBonami–Beckner applied to a discrete derivative · Bonami–Beckner bound for indicator functions · Bonami–Beckner hypercontractive inequality · Hypercontractivity in Fourier form · Vector two-point inequality for nonnegative noise · Hypercontractivity from the vector two-point inequality · Hypercontractivity from the tensorization step · \(L^q\) norm under the uniform measure on the cube · Vector two-point inequality implies the tensorization step · Vector-valued two-point hypercontractive inequality

Definition\(L^q\) norm under the uniform measure on the cube#✓fully proved

The L^q norm (E|f|^q)^(1/q) under the uniform measure.

noncomputable def bnt_qnorm (q : ℝ) (f : (ι → Bool) → ℝ) : ℝ :=
  (bnt_qnormPow q f) ^ (1 / q)

Uses 1 · Used by 14

Statement usesq-th moment under the uniform measure on the cube

Used byBonami–Beckner applied to a discrete derivative · Bonami–Beckner bound for indicator functions · Indicator-bound form of KKL implies the hypercontractive form · Bonami–Beckner hypercontractive inequality · Fourier-form KKL inequality given the hypercontractive bound · Hypercontractive form of KKL with constant 0 holds trivially · Hypercontractivity in Fourier form · Bonami–Beckner hypercontractive inequality · Vector two-point inequality for nonnegative noise · Hypercontractivity from the vector two-point inequality · Hypercontractivity from the tensorization step · Induction step of hypercontractivity tensorization · Vector two-point inequality implies the tensorization step · Vector-valued two-point hypercontractive inequality

DefinitionNoise kernel on the Boolean cube#✓fully proved

The noise kernel: ∏ i, (1 + ρ)/2 or (1 - ρ)/2 according as x i = y i or not.

noncomputable def bnt_noiseKernel (ρ : ℝ) (x y : ι → Bool) : ℝ :=
  ∏ i : ι, (if x i = y i then (1 + ρ) / 2 else (1 - ρ) / 2)

Used by 9

Used byBonami–Beckner applied to a discrete derivative · Bonami–Beckner hypercontractive inequality · Hypercontractivity in Fourier form · Noise operator is diagonal in the Walsh basis · Hypercontractivity from the vector two-point inequality · Hypercontractivity from the tensorization step · Noise operator on the Boolean cube · Agreement of the two noise operators on the Boolean cube · Vector two-point inequality implies the tensorization step

DefinitionNoise operator on the Boolean cube#✓fully proved

The noise operator T_ρ f x = ∑ y, bnt_noiseKernel ρ x y * f y: for ρ ∈ [-1, 1], the expectation of f y where each coordinate of y equals that of x with probability (1 + ρ)/2.

noncomputable def bnt_noiseOp (ρ : ℝ) (f : (ι → Bool) → ℝ) : (ι → Bool) → ℝ :=
  fun x => ∑ y : ι → Bool, bnt_noiseKernel ρ x y * f y

Uses 1 · Used by 10

Statement usesNoise kernel on the Boolean cube

Used byBonami–Beckner applied to a discrete derivative · Bonami–Beckner hypercontractive inequality · Hypercontractivity in Fourier form · Noise operator is diagonal in the Walsh basis · Bonami–Beckner hypercontractive inequality · Hypercontractivity from the vector two-point inequality · Hypercontractivity from the tensorization step · Agreement of the two noise operators on the Boolean cube · Induction step of hypercontractivity tensorization · Vector two-point inequality implies the tensorization step

TheoremUniform expectation on the cube equals the finite average#✓fully proved

bnt_uexp is the uniform average Finset.expect.

theorem bnt_uexp_eq_expect (f : (ι → Bool) → ℝ) : bnt_uexp f = 𝔼 ω, f ω

Uses 1 · Used by 4

Statement usesUniform expectation on the Boolean cube

Used byEvent influence is four times the canonical influence · Hypercontractivity in Fourier form · Parseval's identity on the Boolean cube · Variance as Fourier weight off the empty set

TheoremAgreement of the two noise operators on the Boolean cube#✓fully proved

On Fin n → Bool, bnt_noiseOp is the noise operator BooleanCube.boolNoiseOp.

theorem bnt_noiseOp_eq_boolNoiseOp {n : ℕ} (ρ : ℝ) (f : (Fin n → Bool) → ℝ) :
    bnt_noiseOp ρ f = BooleanCube.boolNoiseOp ρ f

Uses 5 · Used by 3

Statement usesNoise operator on the Boolean cube · Noise operator on the Boolean cube

Proof usesBoolean cube · Sign of a Boolean coordinate · Noise kernel on the Boolean cube

Used byBonami–Beckner applied to a discrete derivative · Hypercontractivity in Fourier form · Noise operator is diagonal in the Walsh basis

DefinitionVector-valued two-point hypercontractive inequality#✓fully proved

The vector-valued two-point inequality at noise ρ, with q = 1 + ρ²: for all n and u v : (Fin n → Bool) → ℝ, the average of ‖((1+ρ)/2) u + ((1-ρ)/2) v‖₂² and ‖((1-ρ)/2) u + ((1+ρ)/2) v‖₂² is at most ((‖u‖_q^q + ‖v‖_q^q) / 2)^(2/q).

def bnt_VectorTwoPoint (ρ : ℝ) : Prop :=
  ∀ (n : ℕ) (u v : (Fin n → Bool) → ℝ),
    (bnt_qnormPow 2 (fun ω => (1 + ρ) / 2 * u ω + (1 - ρ) / 2 * v ω)
        + bnt_qnormPow 2 (fun ω => (1 - ρ) / 2 * u ω + (1 + ρ) / 2 * v ω)) / 2
      ≤ ((bnt_qnorm 2 u ^ (1 + ρ ^ 2) + bnt_qnorm 2 v ^ (1 + ρ ^ 2)) / 2) ^ (2 / (1 + ρ ^ 2))

Uses 2 · Used by 3

Statement uses\(L^q\) norm under the uniform measure on the cube · q-th moment under the uniform measure on the cube

Used byVector two-point inequality for nonnegative noise · Hypercontractivity from the vector two-point inequality · Vector two-point inequality implies the tensorization step

DefinitionInduction step of hypercontractivity tensorization#✓fully proved

The induction step of tensorization: ‖T_ρ g‖₂ ≤ ‖g‖_(1+ρ²) in dimension n implies the same in dimension n + 1.

def bnt_TensorStep (ρ : ℝ) : Prop :=
  ∀ n : ℕ,
    (∀ g : (Fin n → Bool) → ℝ, bnt_qnorm 2 (bnt_noiseOp ρ g) ≤ bnt_qnorm (1 + ρ ^ 2) g) →
    (∀ f : (Fin (n + 1) → Bool) → ℝ,
      bnt_qnorm 2 (bnt_noiseOp ρ f) ≤ bnt_qnorm (1 + ρ ^ 2) f)

Uses 2 · Used by 1

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

Used byHypercontractivity from the tensorization step

TheoremVector two-point inequality implies the tensorization step#✓fully proved

The vector two-point inequality gives the tensorization step.

theorem bnt_tensorStep_of_vec {ρ : ℝ} (Hvec : bnt_VectorTwoPoint ρ) (n : ℕ)
    (ih : ∀ g : (Fin n → Bool) → ℝ, bnt_qnorm 2 (bnt_noiseOp ρ g) ≤ bnt_qnorm (1 + ρ ^ 2) g)
    (f : (Fin (n + 1) → Bool) → ℝ) :
    bnt_qnorm 2 (bnt_noiseOp ρ f) ≤ bnt_qnorm (1 + ρ ^ 2) f

Uses 6 · Used by 1

Statement usesVector-valued two-point hypercontractive inequality · Noise operator on the Boolean cube · \(L^q\) norm under the uniform measure on the cube

Proof usesNoise kernel on the Boolean cube · q-th moment under the uniform measure on the cube · Uniform expectation on the Boolean cube

Used byHypercontractivity from the vector two-point inequality

TheoremHypercontractivity from the vector two-point inequality#✓fully proved

Hypercontractivity ‖T_ρ f‖₂ ≤ ‖f‖_(1+ρ²) on Fin n → Bool, from the vector two-point inequality.

theorem bnt_hypercontractivity {ρ : ℝ} (Hvec : bnt_VectorTwoPoint ρ) (n : ℕ)
    (f : (Fin n → Bool) → ℝ) :
    bnt_qnorm 2 (bnt_noiseOp ρ f) ≤ bnt_qnorm (1 + ρ ^ 2) f

Uses 7 · Used by 2

Statement usesVector-valued two-point hypercontractive inequality · Noise operator on the Boolean cube · \(L^q\) norm under the uniform measure on the cube

Proof usesNoise kernel on the Boolean cube · q-th moment under the uniform measure on the cube · Vector two-point inequality implies the tensorization step · Uniform expectation on the Boolean cube

Used byBonami–Beckner hypercontractive inequality · Bonami–Beckner hypercontractive inequality

TheoremHypercontractivity from the tensorization step#✓fully proved

Hypercontractivity ‖T_ρ f‖₂ ≤ ‖f‖_(1+ρ²) on Fin n → Bool, from the tensorization step.

theorem bnt_hypercontractivity_of_twoPoint {ρ : ℝ} (Hstep : bnt_TensorStep ρ)
    (n : ℕ) (f : (Fin n → Bool) → ℝ) :
    bnt_qnorm 2 (bnt_noiseOp ρ f) ≤ bnt_qnorm (1 + ρ ^ 2) f

Uses 6

Statement usesInduction step of hypercontractivity tensorization · Noise operator on the Boolean cube · \(L^q\) norm under the uniform measure on the cube

Proof usesNoise kernel on the Boolean cube · q-th moment under the uniform measure on the cube · Uniform expectation on the Boolean cube

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.