B-Reasonability Bounds

def Hypercontractivity.IsBReasonable {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (P : MeasureTheory.Measure Ω) (B : ℝ) : Prop

Equations

• Hypercontractivity.IsBReasonable X P B = (ProbabilityTheory.moment X 4 P ≤ B * ProbabilityTheory.moment X 2 P ^ 2)

theorem Hypercontractivity.b_reasonable_tail_bound {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : Ω → ℝ} {B : ℝ} (hB : IsBReasonable X P B) (t : ℝ) (ht : 0 < t) (hX_pos : 0 < ProbabilityTheory.moment X 2 P) (hX_int : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 4) P) : (P {ω : Ω | X ω ^ 4 ≥ t ^ 4 * ProbabilityTheory.moment X 2 P ^ 2}).toReal ≤ B / t ^ 4

If X not equivalent to 0 is B-reasonable, Pr[|X| ≥ t ||X||₂] ≤ B/t⁴ for all t > 0

theorem Hypercontractivity.min_prob_b_reasonable {Ω : Type u_1} [MeasurableSpace Ω] [Fintype Ω] [DiscreteMeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : Ω → ℝ} {π : PMF Ω} (hP : P = π.toMeasure) {μ : ℝ} (hμ_pos : 0 < μ) (hμ_min : ∀ (ω : Ω), μ ≤ (π ω).toReal) : IsBReasonable X P (1 / μ)

theorem Hypercontractivity.paley_zygmund_ineq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Z : Ω → ℝ} (h_meas : Measurable Z) (h_nonneg : ∀ᵐ (ω : Ω) ∂μ, 0 ≤ Z ω) (h_int : MeasureTheory.Integrable Z μ) (h_int_sq : MeasureTheory.Integrable (fun (ω : Ω) => Z ω ^ 2) μ) {θ : ℝ} (hθ_pos : 0 ≤ θ) (hθ_le_one : θ ≤ 1) (hZ_pos : 0 < ProbabilityTheory.moment Z 1 μ) : (1 - θ) ^ 2 * ProbabilityTheory.moment Z 1 μ ^ 2 / ProbabilityTheory.moment Z 2 μ ≤ (μ {ω : Ω | θ * ProbabilityTheory.moment Z 1 μ < Z ω}).toReal

theorem Hypercontractivity.b_reasonable_anticon_zero {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : Ω → ℝ} {B : ℝ} (hB : IsBReasonable X P B) (hX_meas : Measurable X) (hX_int_sq : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) P) (hX_int_4 : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 4) P) (hX_pos_2 : 0 < ProbabilityTheory.moment X 2 P) {t : ℝ} (ht_nonneg : 0 ≤ t) (ht_le_one : t ≤ 1) : (1 - t ^ 2) ^ 2 / B ≤ (P {ω : Ω | t ^ 2 * ProbabilityTheory.moment X 2 P < X ω ^ 2}).toReal

Helper definitions and lemmas for the Bonami lemma

noncomputable def Hypercontractivity.restrictLast {n : ℕ} (f : BooleanAnalysis.BooleanFunc (n + 1)) (b : Bool) : BooleanAnalysis.BooleanFunc n

Restrict a Boolean function on n+1 variables by fixing the last coordinate.

Equations

• Hypercontractivity.restrictLast f b x = f (Fin.snoc x b)

noncomputable def Hypercontractivity.avgLast {n : ℕ} (f : BooleanAnalysis.BooleanFunc (n + 1)) : BooleanAnalysis.BooleanFunc n

The average of f over the last coordinate.

Equations

• Hypercontractivity.avgLast f x = (Hypercontractivity.restrictLast f false x + Hypercontractivity.restrictLast f true x) / 2

noncomputable def Hypercontractivity.diffLast {n : ℕ} (f : BooleanAnalysis.BooleanFunc (n + 1)) : BooleanAnalysis.BooleanFunc n

The half-difference of f over the last coordinate.

Equations

• Hypercontractivity.diffLast f x = (Hypercontractivity.restrictLast f false x - Hypercontractivity.restrictLast f true x) / 2

theorem Hypercontractivity.restrictLast_false_eq {n : ℕ} (f : BooleanAnalysis.BooleanFunc (n + 1)) (x : BooleanAnalysis.BoolCube n) : restrictLast f false x = avgLast f x + diffLast f x

restrictLast false = avgLast + diffLast

theorem Hypercontractivity.restrictLast_true_eq {n : ℕ} (f : BooleanAnalysis.BooleanFunc (n + 1)) (x : BooleanAnalysis.BoolCube n) : restrictLast f true x = avgLast f x - diffLast f x

restrictLast true = avgLast - diffLast

theorem Hypercontractivity.sum_boolCube_succ {n : ℕ} (φ : BooleanAnalysis.BoolCube (n + 1) → ℝ) : ∑ x : BooleanAnalysis.BoolCube (n + 1), φ x = ∑ x : BooleanAnalysis.BoolCube n, φ (Fin.snoc x false) + ∑ x : BooleanAnalysis.BoolCube n, φ (Fin.snoc x true)

theorem Hypercontractivity.uniformWeight_succ (n : ℕ) : BooleanAnalysis.uniformWeight (n + 1) = BooleanAnalysis.uniformWeight n / 2

uniformWeight (n+1) = uniformWeight n / 2

theorem Hypercontractivity.expect_succ_eq {n : ℕ} (φ : BooleanAnalysis.BooleanFunc (n + 1)) : BooleanAnalysis.expect φ = (BooleanAnalysis.expect (restrictLast φ false) + BooleanAnalysis.expect (restrictLast φ true)) / 2

theorem Hypercontractivity.fourth_pow_sum (a b : ℝ) : (a + b) ^ 4 + (a - b) ^ 4 = 2 * (a ^ 4 + 6 * a ^ 2 * b ^ 2 + b ^ 4)

The algebraic identity: (a+b)^4 + (a-b)^4 = 2*(a^4 + 6a^2b^2 + b^4)

theorem Hypercontractivity.second_pow_sum (a b : ℝ) : (a + b) ^ 2 + (a - b) ^ 2 = 2 * (a ^ 2 + b ^ 2)

The algebraic identity: (a+b)^2 + (a-b)^2 = 2*(a^2 + b^2)

theorem Hypercontractivity.fourth_moment_decomp {n : ℕ} (f : BooleanAnalysis.BooleanFunc (n + 1)) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube (n + 1)) => f x ^ 4) = ((BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => avgLast f x ^ 4) + 6 * BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => avgLast f x ^ 2 * diffLast f x ^ 2) + BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => diffLast f x ^ 4

theorem Hypercontractivity.second_moment_decomp {n : ℕ} (f : BooleanAnalysis.BooleanFunc (n + 1)) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube (n + 1)) => f x ^ 2) = (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => avgLast f x ^ 2) + BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => diffLast f x ^ 2

theorem Hypercontractivity.expect_cs_sq {n : ℕ} (g h : BooleanAnalysis.BooleanFunc n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => g x ^ 2 * h x ^ 2) ^ 2 ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => g x ^ 4) * BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => h x ^ 4

theorem Hypercontractivity.expect_sq_nonneg {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) : 0 ≤ BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 2

theorem Hypercontractivity.expect_sq_nonneg_prod {n : ℕ} (g h : BooleanAnalysis.BooleanFunc n) : 0 ≤ BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => g x ^ 2 * h x ^ 2

theorem Hypercontractivity.expect_fourth_nonneg {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) : 0 ≤ BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 4

theorem Hypercontractivity.degree_avgLast {n : ℕ} (f : BooleanAnalysis.BooleanFunc (n + 1)) (k : ℕ) (hf : BooleanAnalysis.has_degree_at_most f k) : BooleanAnalysis.has_degree_at_most (avgLast f) k

theorem Hypercontractivity.degree_diffLast {n : ℕ} (f : BooleanAnalysis.BooleanFunc (n + 1)) (k : ℕ) (hf : BooleanAnalysis.has_degree_at_most f k) : BooleanAnalysis.has_degree_at_most (diffLast f) (k - 1)

theorem Hypercontractivity.degree_zero_const {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) (hf : BooleanAnalysis.has_degree_at_most f 0) (x : BooleanAnalysis.BoolCube n) : f x = f default

theorem Hypercontractivity.degree_zero_fourth_moment {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) (hf : BooleanAnalysis.has_degree_at_most f 0) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 4) = (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 2) ^ 2

theorem Hypercontractivity.bonami_algebra {m : ℕ} {a b A B C : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hB : 0 ≤ B) (hC : 0 ≤ C) (hA_bound : A ≤ 9 ^ (m + 1) * a ^ 2) (hB_bound : B ≤ 9 ^ m * b ^ 2) (hC_bound : C ^ 2 ≤ A * B) : A + 6 * C + B ≤ 9 ^ (m + 1) * (a + b) ^ 2

theorem Hypercontractivity.bonami_expect {n : ℕ} (k : ℕ) (f : BooleanAnalysis.BooleanFunc n) (hf : BooleanAnalysis.has_degree_at_most f k) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 4) ≤ 9 ^ k * (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 2) ^ 2

theorem Hypercontractivity.moment_eq_expect {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) (p : ℕ) (P : MeasureTheory.Measure (BooleanAnalysis.BoolCube n)) [MeasureTheory.IsProbabilityMeasure P] (hP_unif : ∀ (x : BooleanAnalysis.BoolCube n), (P {x}).toReal = BooleanAnalysis.uniformWeight n) : ProbabilityTheory.moment f p P = BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ p

noncomputable def Hypercontractivity.uniformMeasure (n : ℕ) : MeasureTheory.Measure (BooleanAnalysis.BoolCube n)

The canonical uniform probability measure on the Boolean Hypercube.

Equations

• Hypercontractivity.uniformMeasure n = (PMF.uniformOfFintype (BooleanAnalysis.BoolCube n)).toMeasure

instance Hypercontractivity.instIsProbabilityMeasureBoolCubeUniformMeasure (n : ℕ) : MeasureTheory.IsProbabilityMeasure (uniformMeasure n)

theorem Hypercontractivity.uniformMeasure_apply {n : ℕ} (x : BooleanAnalysis.BoolCube n) : ((uniformMeasure n) {x}).toReal = BooleanAnalysis.uniformWeight n

Prove that our canonical measure matches the combinatorial uniformWeight.

theorem Hypercontractivity.bonami_lemma {n : ℕ} (k : ℕ) (f : BooleanAnalysis.BooleanFunc n) (hf : BooleanAnalysis.has_degree_at_most f k) : IsBReasonable f (uniformMeasure n) (9 ^ k)

The Bonami Lemma: A Boolean function of degree at most k is 9^k-reasonable under the uniform measure.

(2,4)-Hypercontractivity Theorem

theorem Hypercontractivity.fourierCoeff_avgLast {n : ℕ} (f : BooleanAnalysis.BooleanFunc (n + 1)) (S : Finset (Fin n)) : BooleanAnalysis.fourierCoeff (avgLast f) S = BooleanAnalysis.fourierCoeff f (Finset.image Fin.castSucc S)

theorem Hypercontractivity.fourierCoeff_diffLast {n : ℕ} (f : BooleanAnalysis.BooleanFunc (n + 1)) (S : Finset (Fin n)) : BooleanAnalysis.fourierCoeff (diffLast f) S = BooleanAnalysis.fourierCoeff f (Finset.image Fin.castSucc S ∪ {Fin.last n})

theorem Hypercontractivity.chiS_snoc_castSucc {n : ℕ} (S : Finset (Fin n)) (x : BooleanAnalysis.BoolCube n) (b : Bool) : BooleanAnalysis.chiS (Finset.image Fin.castSucc S) (Fin.snoc x b) = BooleanAnalysis.chiS S x

theorem Hypercontractivity.chiS_snoc_with_last {n : ℕ} (S : Finset (Fin n)) (x : BooleanAnalysis.BoolCube n) (b : Bool) : BooleanAnalysis.chiS (Finset.image Fin.castSucc S ∪ {Fin.last n}) (Fin.snoc x b) = BooleanAnalysis.boolToSign b * BooleanAnalysis.chiS S x

theorem Hypercontractivity.finset_fin_succ_sum_partition {n : ℕ} (φ : Finset (Fin (n + 1)) → ℝ) : ∑ S : Finset (Fin (n + 1)), φ S = ∑ T : Finset (Fin n), φ (Finset.image Fin.castSucc T) + ∑ T : Finset (Fin n), φ (Finset.image Fin.castSucc T ∪ {Fin.last n})

theorem Hypercontractivity.card_image_castSucc {n : ℕ} (S : Finset (Fin n)) : (Finset.image Fin.castSucc S).card = S.card

Cardinality of a lifted set: |S.image castSucc| = |S|.

theorem Hypercontractivity.card_image_castSucc_union_last {n : ℕ} (S : Finset (Fin n)) : (Finset.image Fin.castSucc S ∪ {Fin.last n}).card = S.card + 1

theorem Hypercontractivity.noiseOp_snoc {n : ℕ} (ρ : ℝ) (f : BooleanAnalysis.BooleanFunc (n + 1)) (x : BooleanAnalysis.BoolCube n) (b : Bool) : BooleanAnalysis.noiseOp ρ f (Fin.snoc x b) = BooleanAnalysis.noiseOp ρ (avgLast f) x + BooleanAnalysis.boolToSign b * ρ * BooleanAnalysis.noiseOp ρ (diffLast f) x

theorem Hypercontractivity.fourth_moment_noise_decomp {n : ℕ} (ρ : ℝ) (f : BooleanAnalysis.BooleanFunc (n + 1)) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube (n + 1)) => BooleanAnalysis.noiseOp ρ f x ^ 4) = ((BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ (avgLast f) x ^ 4) + 6 * ρ ^ 2 * BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ (avgLast f) x ^ 2 * BooleanAnalysis.noiseOp ρ (diffLast f) x ^ 2) + ρ ^ 4 * BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ (diffLast f) x ^ 4

theorem Hypercontractivity.sq_le_sq_mul_of_nonneg {C a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (h : C ^ 2 ≤ a ^ 2 * b ^ 2) : C ≤ a * b

theorem Hypercontractivity.hypercontractivity_algebra_simple {a b ρ : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hρ : ρ ^ 2 ≤ 1 / 3) : a ^ 2 + 6 * ρ ^ 2 * (a * b) + ρ ^ 4 * b ^ 2 ≤ (a + b) ^ 2

theorem Hypercontractivity.hypercontractivity_algebra' {a b A B C ρ : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hA_nn : 0 ≤ A) (hB_nn : 0 ≤ B) (hC : 0 ≤ C) (hA_bound : A ≤ a ^ 2) (hB_bound : B ≤ b ^ 2) (hC_bound : C ^ 2 ≤ A * B) (hρ : ρ ^ 2 ≤ 1 / 3) : A + 6 * ρ ^ 2 * C + ρ ^ 4 * B ≤ (a + b) ^ 2

Key algebraic inequality: under ρ² ≤ 1/3, the recurrence closes.

theorem Hypercontractivity.hypercontractivity_2_4 {n : ℕ} (ρ : ℝ) (hρ : ρ ^ 2 ≤ 1 / 3) (f : BooleanAnalysis.BooleanFunc n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ f x ^ 4) ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 2) ^ 2

The (2,4)-Hypercontractivity Theorem (Bonami–Beckner): For any Boolean function f : {0,1}ⁿ → ℝ and noise parameter ρ with ρ² ≤ 1/3 (i.e., |ρ| ≤ 1/√3), 𝔼[(T_ρ f)⁴] ≤ (𝔼[f²])², or equivalently ‖T_ρ f‖₄ ≤ ‖f‖₂.

theorem Hypercontractivity.innerProduct_le_L43_L4 {n : ℕ} (f g : BooleanAnalysis.BooleanFunc n) : BooleanAnalysis.innerProduct f g ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => |f x| ^ (4 / 3)) ^ (3 / 4) * (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => |g x| ^ 4) ^ (1 / 4)

Hölder's inequality for p = 4/3 and q = 4.

theorem Hypercontractivity.hypercontractivity_4_div_3_2 {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp (1 / √3) f x ^ 2) ^ (1 / 2) ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => |f x| ^ (4 / 3)) ^ (3 / 4)

Contractivity of the noise operator (q = 2 case)

theorem Hypercontractivity.noise_l2_fourier {n : ℕ} (ρ : ℝ) (f : BooleanAnalysis.BooleanFunc n) : BooleanAnalysis.innerProduct (BooleanAnalysis.noiseOp ρ f) (BooleanAnalysis.noiseOp ρ f) = ∑ S : Finset (Fin n), (ρ ^ S.card) ^ 2 * BooleanAnalysis.fourierCoeff f S ^ 2

The L² norm of T_ρ f in Fourier space: 𝔼[(T_ρ f)²] = ∑_S ρ^{2|S|} f̂(S)².

theorem Hypercontractivity.contractivity {n : ℕ} (ρ : ℝ) (hρ : ρ ^ 2 ≤ 1) (f : BooleanAnalysis.BooleanFunc n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ f x ^ 2) ≤ BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 2

Contractivity: 𝔼[(T_ρ f)²] ≤ 𝔼[f²] for ρ² ≤ 1. This is the q = 2 case of hypercontractivity.

Combinatorial inequality

theorem Hypercontractivity.binom_coeff_ineq (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (hj : j ≤ k) : (2 * k).choose (2 * j) ≤ k.choose j * (2 * k - 1) ^ j

Two-point inequality for even powers

theorem Hypercontractivity.two_point_ineq (k : ℕ) (hk : 1 ≤ k) (α β ρ : ℝ) (hρ : ρ ^ 2 ≤ 1 / (2 * ↑k - 1)) : (α + ρ * β) ^ (2 * k) + (α - ρ * β) ^ (2 * k) ≤ 2 * (α ^ 2 + β ^ 2) ^ k

theorem Hypercontractivity.two_point_ineq_avg (k : ℕ) (hk : 1 ≤ k) (α β ρ : ℝ) (hρ : ρ ^ 2 ≤ 1 / (2 * ↑k - 1)) : ((α + ρ * β) ^ (2 * k) + (α - ρ * β) ^ (2 * k)) / 2 ≤ (α ^ 2 + β ^ 2) ^ k

Two-point inequality, averaged form (dividing by 2).

Moment decomposition for even powers

theorem Hypercontractivity.qth_moment_decomp {n : ℕ} (q : ℕ) (f : BooleanAnalysis.BooleanFunc (n + 1)) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube (n + 1)) => f x ^ q) = BooleanAnalysis.expect fun (x' : BooleanAnalysis.BoolCube n) => ((avgLast f x' + diffLast f x') ^ q + (avgLast f x' - diffLast f x') ^ q) / 2

For even q, the q-th moment decomposes using avgLast and diffLast.

theorem Hypercontractivity.noise_qth_moment_decomp {n : ℕ} (q : ℕ) (ρ : ℝ) (f : BooleanAnalysis.BooleanFunc (n + 1)) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube (n + 1)) => BooleanAnalysis.noiseOp ρ f x ^ q) = BooleanAnalysis.expect fun (x' : BooleanAnalysis.BoolCube n) => ((BooleanAnalysis.noiseOp ρ (avgLast f) x' + ρ * BooleanAnalysis.noiseOp ρ (diffLast f) x') ^ q + (BooleanAnalysis.noiseOp ρ (avgLast f) x' - ρ * BooleanAnalysis.noiseOp ρ (diffLast f) x') ^ q) / 2

The noise operator decomposes on (n+1)-cubes for q-th moments.

The main (2, 2k)-Hypercontractivity Theorem

theorem Hypercontractivity.hypercontractivity_2_2k {n : ℕ} (k : ℕ) (hk : 1 ≤ k) (ρ : ℝ) (hρ : ρ ^ 2 ≤ 1 / (2 * ↑k - 1)) (f : BooleanAnalysis.BooleanFunc n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ f x ^ (2 * k)) ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 2) ^ k

Equivalent formulation with q

theorem Hypercontractivity.hypercontractivity_2_q {n : ℕ} (q : ℕ) (hq : 2 ≤ q) (hq_even : Even q) (ρ : ℝ) (hρ : ρ ^ 2 ≤ 1 / (↑q - 1)) (f : BooleanAnalysis.BooleanFunc n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ f x ^ q) ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 2) ^ (q / 2)

The (2, q)-Hypercontractivity restated with even q.

Corollaries and specific cases

theorem Hypercontractivity.hypercontractivity_2_2 {n : ℕ} (ρ : ℝ) (hρ : ρ ^ 2 ≤ 1) (f : BooleanAnalysis.BooleanFunc n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ f x ^ 2) ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 2) ^ 1

The (2, 2)-hypercontractivity is just contractivity.

theorem Hypercontractivity.hypercontractivity_2_4_inst {n : ℕ} (ρ : ℝ) (hρ : ρ ^ 2 ≤ 1 / 3) (f : BooleanAnalysis.BooleanFunc n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ f x ^ 4) ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 2) ^ 2

The (2, 4)-hypercontractivity instantiation.

theorem Hypercontractivity.hypercontractivity_2_6 {n : ℕ} (ρ : ℝ) (hρ : ρ ^ 2 ≤ 1 / 5) (f : BooleanAnalysis.BooleanFunc n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ f x ^ 6) ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 2) ^ 3

The (2, 6)-hypercontractivity.

Real-power formulation

theorem Hypercontractivity.hypercontractivity_2_2k_rpow {n : ℕ} (k : ℕ) (hk : 1 ≤ k) (ρ : ℝ) (hρ : ρ ^ 2 ≤ 1 / (2 * ↑k - 1)) (f : BooleanAnalysis.BooleanFunc n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ f x ^ (2 * k)) ^ (1 / (2 * ↑k)) ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 2) ^ (1 / 2)

(p, 2)-Hypercontractivity via Duality

theorem Hypercontractivity.innerProduct_eq_expect_sq {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) : BooleanAnalysis.innerProduct f f = BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x ^ 2

theorem Hypercontractivity.expect_sq_noiseOp_nonneg {n : ℕ} (ρ : ℝ) (f : BooleanAnalysis.BooleanFunc n) : 0 ≤ BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ f x ^ 2

theorem Hypercontractivity.expect_rpow_abs_nonneg {n : ℕ} (p : ℝ) (f : BooleanAnalysis.BooleanFunc n) : 0 ≤ BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => |f x| ^ p

theorem Hypercontractivity.noiseOp_compose {n : ℕ} (ρ σ : ℝ) (f : BooleanAnalysis.BooleanFunc n) : BooleanAnalysis.noiseOp ρ (BooleanAnalysis.noiseOp σ f) = BooleanAnalysis.noiseOp (ρ * σ) f

theorem Hypercontractivity.hypercontractivity_p_2_general {n : ℕ} {ρ p q : ℝ} (hp : 1 < p) (hq : 2 ≤ q) (hpq : 1 / p + 1 / q = 1) (f : BooleanAnalysis.BooleanFunc n) (holder : ∀ (u v : BooleanAnalysis.BooleanFunc n), BooleanAnalysis.innerProduct u v ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => |u x| ^ p) ^ (1 / p) * (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => |v x| ^ q) ^ (1 / q)) (hyp_2_q : ∀ (g : BooleanAnalysis.BooleanFunc n), (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => |BooleanAnalysis.noiseOp ρ g x| ^ q) ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => g x ^ 2) ^ (q / 2)) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp ρ f x ^ 2) ^ (1 / 2) ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => |f x| ^ p) ^ (1 / p)

The (p, 2)-Hypercontractivity Theorem (general duality framework):

Given a (2, q)-hypercontractivity bound and Hölder's inequality for (p, q), we conclude (𝔼[(T_ρ f)²])^{1/2} ≤ (𝔼[|f|^p])^{1/p}.

The proof:

1. ‖T_ρ f‖₂² = ⟨T_ρ f, T_ρ f⟩ = ⟨f, T_ρ(T_ρ f)⟩ by self-adjointness
2. ⟨f, T_ρ(T_ρ f)⟩ ≤ ‖f‖_p · ‖T_ρ(T_ρ f)‖_q by Hölder
3. ‖T_ρ(T_ρ f)‖_q ≤ ‖T_ρ f‖₂ by (2,q)-hypercontractivity
4. Divide both sides by ‖T_ρ f‖₂.

theorem Hypercontractivity.hypercontractivity_p_2_at_4_div_3 {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => BooleanAnalysis.noiseOp (1 / √3) f x ^ 2) ^ (1 / 2) ≤ (BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => |f x| ^ (4 / 3)) ^ (3 / 4)

(4/3, 2)-hypercontractivity via the existing theorem.