theorem BooleanFourier.noiseOp_snoc_eq_twoPointNoiseOp {m : ℕ} (ρ : ℝ) (f : BoolFn (m + 1)) (x' : Fin m → Bool) (b : Bool) : noiseOp ρ f (Fin.snoc x' b) = twoPointNoiseOp ρ (fun (c : Bool) => noiseOp ρ (restrictLast f c) x') b

theorem BooleanFourier.lpNorm_convex_combination {m : ℕ} (g₁ g₂ : BoolFn m) (α β : ℝ) (hα : 0 ≤ α) (hβ : 0 ≤ β) {q : ℝ} (hq : 1 ≤ q) : (lpNorm q fun (x : Fin m → Bool) => α * g₁ x + β * g₂ x) ≤ α * lpNorm q g₁ + β * lpNorm q g₂

theorem BooleanFourier.bonami_beckner_succ {m : ℕ} (f : BoolFn (m + 1)) {p q ρ : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) (hρ0 : 0 ≤ ρ) (hρ : ρ ≤ √((p - 1) / (q - 1))) (ih : ∀ (g : BoolFn m), lpNorm q (noiseOp ρ g) ≤ lpNorm p g) : lpNorm q (noiseOp ρ f) ≤ lpNorm p f

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

theorem BooleanFourier.lpNorm_degree1_hypercontractive {n : ℕ} (f : BoolFn n) (hd : degree f ≤ 1) {q : ℝ} (hq : 2 ≤ q) : lpNorm q f ≤ √(q - 1) * lpNorm 2 f