theorem BooleanFourier.lpNorm_noiseOperator_le_of_twoPoint {n : ℕ} (f : BoolFn n) {p q ρ : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) (hρ_nonneg : 0 ≤ ρ) (hρ_bound : ρ ≤ √((p - 1) / (q - 1))) (_h_twopoint : ∀ (g : Bool → ℝ), twoPointLpNorm q (twoPointNoiseOp ρ g) ≤ twoPointLpNorm p g) : lpNorm q (noiseOperator ρ f) ≤ lpNorm p f

theorem BooleanFourier.hypercontractivity {n : ℕ} (f : BoolFn n) {p q ρ : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) (hρ_nonneg : 0 ≤ ρ) (hρ_bound : ρ ≤ √((p - 1) / (q - 1))) : lpNorm q (noiseOperator ρ f) ≤ lpNorm p f