noncomputable def BooleanFourier.twoPointLpNorm (p : ℝ) (g : Bool → ℝ) : ℝ

noncomputable def BooleanFourier.twoPointNoiseOp (ρ : ℝ) (g : Bool → ℝ) : Bool → ℝ

theorem BooleanFourier.two_point_core_inequality {p q ρ : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) (hρ0 : 0 ≤ ρ) (hρ : ρ ≤ √((p - 1) / (q - 1))) (a b : ℝ) : (|(1 + ρ) / 2 * a + (1 - ρ) / 2 * b| ^ q + |(1 - ρ) / 2 * a + (1 + ρ) / 2 * b| ^ q) / 2 ≤ ((|a| ^ p + |b| ^ p) / 2) ^ (q / p)

theorem BooleanFourier.two_point_inequality {p q ρ : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) (hρ0 : 0 ≤ ρ) (hρ : ρ ≤ √((p - 1) / (q - 1))) (g : Bool → ℝ) : twoPointLpNorm q (twoPointNoiseOp ρ g) ≤ twoPointLpNorm p g

noncomputable def BooleanFourier.twoPointPathFn (p a b t : ℝ) : ℝ

noncomputable def BooleanFourier.twoPointExponent (p t : ℝ) : ℝ

theorem BooleanFourier.twoPointPathFn_c_pos {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : 0 < a + b) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : 0 < (1 + t) / 2 * a + (1 - t) / 2 * b

theorem BooleanFourier.twoPointPathFn_d_pos {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : 0 < a + b) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : 0 < (1 - t) / 2 * a + (1 + t) / 2 * b

theorem BooleanFourier.twoPointPathFn_base_pos {p a b : ℝ} (_hp : 1 < p) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : 0 < a + b) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : 0 < (((1 + t) / 2 * a + (1 - t) / 2 * b) ^ (1 + (p - 1) / t ^ 2) + ((1 - t) / 2 * a + (1 + t) / 2 * b) ^ (1 + (p - 1) / t ^ 2)) / 2

noncomputable def BooleanFourier.twoPointPathFn_derivValue (p a b t : ℝ) : ℝ