The p-biased two-point inequality, reduced to one variable

DefinitionLeft side of the one-variable p-biased inequality#✓fully proved

((1-p) + p z)² + 4(q-1) p²(1-p)²(z - 1)²: the left side of the p-biased two-point inequality at u = 1, v = z.

def pbt_g (p q z : ℝ) : ℝ :=
  ((1 - p) + p * z) ^ 2 + (q - 1) * 4 * p ^ 2 * (1 - p) ^ 2 * (z - 1) ^ 2

Used by 3

Used byPointwise bound implies the one-variable p-biased inequality · Statement of the one-variable p-biased inequality · Reduction of the p-biased two-point inequality to one variable

DefinitionStatement of the one-variable p-biased inequality#✓fully proved

The one-variable p-biased inequality: pbt_g p q z ≤ ((1-p) + p z^q)^(2/q) for z ≥ 0.

def pbt_OneVarCore (p q : ℝ) : Prop :=
  ∀ z : ℝ, 0 ≤ z → pbt_g p q z ≤ ((1 - p) + p * z ^ q) ^ (2 / q)

Uses 1 · Used by 4

Statement usesLeft side of the one-variable p-biased inequality

Used byPointwise bound implies the one-variable p-biased inequality · p-biased two-point inequality from the pointwise bound · Reduction of the p-biased two-point inequality to one variable · One-variable p-biased inequality

DefinitionLeft side of the p-biased two-point inequality#✓fully proved

The left side ((1-p) u + p v)² + 4(q-1) p²(1-p)²(u - v)² of the p-biased two-point inequality.

def pbt_lhs (p q u v : ℝ) : ℝ :=
  ((1 - p) * u + p * v) ^ 2 + (q - 1) * 4 * p ^ 2 * (1 - p) ^ 2 * (u - v) ^ 2

Used by 1

Used byReduction of the p-biased two-point inequality to one variable

TheoremReduction of the p-biased two-point inequality to one variable#✓fully proved

The p-biased two-point inequality, assuming the one-variable inequality for p and 1 - p.

theorem pbt_two_point_value_of_core {p q : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
    (hq1 : 1 ≤ q) (hq2 : q ≤ 2)
    (Hcore : pbt_OneVarCore p q) (Hcore' : pbt_OneVarCore (1 - p) q) (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 3 · Used by 1

Statement usesStatement of the one-variable p-biased inequality

Proof usesLeft side of the one-variable p-biased inequality · Left side of the p-biased two-point inequality

Used byp-biased two-point inequality from the pointwise bound

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.