The p-biased two-point inequality

DefinitionConvex auxiliary function for the p-biased inequality#✓fully proved

(1-p)(1 - p t)^q + p(1 + (1-p) t)^q - 1 - 2q(q-1) p²(1-p)² t², convex and nonnegative on [-1/(1-p), 1/p] for 1 ≤ q ≤ 2.

noncomputable def pcx_g (p q t : ℝ) : ℝ :=
  (1 - p) * (1 - p * t) ^ q + p * (1 + (1 - p) * t) ^ q - 1
    - 2 * q * (q - 1) * p ^ 2 * (1 - p) ^ 2 * t ^ 2

Used by 1

Used byPointwise bound for the p-biased inequality holds

TheoremPointwise bound for the p-biased inequality holds#✓fully proved

The pointwise bound pih_KEY p q for 0 < p < 1 and 1 ≤ q ≤ 2.

theorem pcx_KEY_pos {p q : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (hq1 : 1 ≤ q) (hq2 : q ≤ 2) :
    pih_KEY p q

Uses 4 · Used by 2

Statement usesPointwise bound behind the p-biased inequality

Proof usesConvex auxiliary function for the p-biased inequality · Variance term in the p-biased inequality · Mean of a p-biased two-valued function

Used byOne-variable p-biased inequality · p-biased two-point inequality

TheoremOne-variable p-biased inequality#✓fully proved

The one-variable p-biased inequality for 0 < p < 1 and 1 ≤ q ≤ 2.

theorem pcx_OneVarCore {p q : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (hq1 : 1 ≤ q) (hq2 : q ≤ 2) :
    pbt_OneVarCore p q

Uses 3

Statement usesStatement of the one-variable p-biased inequality

Proof usesPointwise bound for the p-biased inequality holds · Pointwise bound implies the one-variable p-biased inequality

Theoremp-biased two-point inequality#✓fully proved

The p-biased two-point inequality: for 0 < p < 1, 1 ≤ q ≤ 2 and real u, v, ((1-p) u + p v)² + 4(q-1) p²(1-p)²(u - v)² ≤ ((1-p)|u|^q + p|v|^q)^(2/q).

theorem pcx_two_point_value {p q : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (hq1 : 1 ≤ q) (hq2 : q ≤ 2)
    (u v : ℝ) :
    ((1 - p) * u + p * v) ^ 2 + (q - 1) * 4 * p ^ 2 * (1 - p) ^ 2 * (u - v) ^ 2
      ≤ ((1 - p) * |u| ^ q + p * |v| ^ q) ^ (2 / q)

Uses 2 · Used by 1

Proof usesPointwise bound for the p-biased inequality holds · p-biased two-point inequality from the pointwise bound

Used byTensorization step for \(p\)-biased hypercontractivity

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.