Documentation

Complexity.Foundations.BooleanAnalysis.Hypercontractivity.Tensorization

Tensorization of two-function hypercontractivity #

For a correlation ρ, the expectation 𝔼_x f x · T_ρ g x of f against the noise operator applied to g is the expectation of f x g y over a ρ-correlated pair (x, y). A two-function hypercontractive inequality bounds it by ‖f‖_p ‖g‖_q. Such an inequality tensorizes: if it holds on a single bit, it holds on every cube (the Two-Function Hypercontractivity Induction Theorem, BitString.expect_mul_noiseOp_le_of_unit) O'Donnell, Section 9.4.

The proof is induction by restrictions. On the cube over ι ⊕ κ the noise operator acts on the two blocks of coordinates independently (BitString.noiseOp_sumElim), since a random mask on ι ⊕ κ is a pair of independent masks (BitString.bernoulliAverage_sumElim). Fixing the bits in ι, the inequality on κ bounds the inner expectation by the product of the norms of the restrictions; these norms are functions of the bits in ι, to which the inequality on ι applies, and their norms are the norms of f and g (BitString.lpNorm_sumElim). The noise operator also commutes with renaming the coordinates (BitString.noiseOp_comp_arrowCongr), so induction over Fin n reaches every finite coordinate type.

Main results #

References #

The noise operator on split coordinates #

theorem Cslib.BitString.noiseOp_sumElim {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (ρ : ℝ) (g : (ι ⊕ κ → Bool) → ℝ) (x₁ : ι → Bool) (x₂ : κ → Bool) :
noiseOp ρ g (Sum.elim x₁ x₂) = noiseOp ρ (fun (y₁ : ι → Bool) => noiseOp ρ (fun (y₂ : κ → Bool) => g (Sum.elim y₁ y₂)) x₂) x₁

The noise operator on a disjoint union of coordinates applies the noise operator on the bits in κ and then the noise operator on the bits in ι.

Tensorization #

theorem Cslib.BitString.expect_mul_noiseOp_le_of_unit {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p q ρ : ℝ} (hp : p ≠ 0) (hq : q ≠ 0) (hρ : 0 ≤ ρ) (hρ' : ρ ≤ 1) (h : ∀ (f g : (Unit → Bool) → ℝ), (Finset.univ.expect fun (x : Unit → Bool) => f x * noiseOp ρ g x) ≤ lpNorm p f * lpNorm q g) (f g : (ι → Bool) → ℝ) :
(Finset.univ.expect fun (x : ι → Bool) => f x * noiseOp ρ g x) ≤ lpNorm p f * lpNorm q g

The Two-Function Hypercontractivity Induction Theorem: if the two-function inequality 𝔼_x f x · T_ρ g x ≤ ‖f‖_p ‖g‖_q holds for all functions of a single bit, then it holds for all functions on every cube. Here 𝔼_x f x · T_ρ g x is the expectation of f x g y over a ρ-correlated pair (x, y) O'Donnell, Section 9.4.