The two-point Bonami inequality

TheoremTaylor lower bound for \((1+t)^q + (1-t)^q\)#✓fully proved

For 1 ≤ q ≤ 2 and |t| ≤ 1, 2 + q(q-1) t² ≤ (1 + t)^q + (1 - t)^q.

theorem bts_taylor_lower {q t : ℝ} (hq1 : 1 ≤ q) (hq2 : q ≤ 2) (ht : |t| ≤ 1) :
    2 + q * (q - 1) * t ^ 2 ≤ (1 + t) ^ q + (1 - t) ^ q

Used by 1

Used byTwo-point Bonami inequality

TheoremTwo-point Bonami inequality#✓fully proved

The two-point Bonami inequality (Bonami 1970; Beckner 1975): for 0 ≤ ρ ≤ 1 and real a, b, with q = 1 + ρ², a² + ρ² b² ≤ ((|a + b|^q + |a - b|^q) / 2)^(2/q), i.e. ‖a + ρ b x‖₂ ≤ ‖a + b x‖_q for a uniform random sign x.

theorem bts_twoPointScalar {ρ : ℝ} (h0 : 0 ≤ ρ) (h1 : ρ ≤ 1) (a b : ℝ) :
    a ^ 2 + ρ ^ 2 * b ^ 2
      ≤ ((|a + b| ^ (1 + ρ ^ 2) + |a - b| ^ (1 + ρ ^ 2)) / 2) ^ (2 / (1 + ρ ^ 2))

Uses 1 · Used by 1

Proof usesTaylor lower bound for \((1+t)^q + (1-t)^q\)

Used byVector two-point inequality for nonnegative noise

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.