The one-variable p-biased inequality from a pointwise bound

DefinitionMean of a p-biased two-valued function#✓fully proved

The mean (1-p) + p z of the p-biased two-valued function with values 1 and z.

def pih_m (p z : ℝ) : ℝ := (1 - p) + p * z

Used by 3

Used byPointwise bound implies the one-variable p-biased inequality · Pointwise bound behind the p-biased inequality · Pointwise bound for the p-biased inequality holds

DefinitionVariance term in the p-biased inequality#✓fully proved

The variance term 4(q-1) p²(1-p)²(z - 1)².

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

Used by 3

Used byPointwise bound implies the one-variable p-biased inequality · Pointwise bound behind the p-biased inequality · Pointwise bound for the p-biased inequality holds

DefinitionPointwise bound behind the p-biased inequality#✓fully proved

The pointwise bound (q/2) m^(q-2) V ≤ (1-p) + p z^q - m^q for all z ≥ 0, with m = pih_m p z, V = pih_V p q z.

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

Uses 2 · Used by 3

Statement usesVariance term in the p-biased inequality · Mean of a p-biased two-valued function

Used byPointwise bound implies the one-variable p-biased inequality · p-biased two-point inequality from the pointwise bound · Pointwise bound for the p-biased inequality holds

TheoremPointwise bound implies the one-variable p-biased inequality#✓fully proved

The pointwise bound pih_KEY p q implies the one-variable inequality pbt_OneVarCore p q.

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

Uses 5 · Used by 2

Statement usesStatement of the one-variable p-biased inequality · Pointwise bound behind the p-biased inequality

Proof usesLeft side of the one-variable p-biased inequality · Variance term in the p-biased inequality · Mean of a p-biased two-valued function

Used byp-biased two-point inequality from the pointwise bound · One-variable p-biased inequality

Theoremp-biased two-point inequality from the pointwise bound#✓fully proved

The p-biased two-point inequality from pih_KEY p q and pih_KEY (1 - p) q.

theorem pih_two_point_value_of_KEY {p q : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (hq1 : 1 ≤ q) (hq2 : q ≤ 2)
    (HKEY : pih_KEY p q) (HKEY' : pih_KEY (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 4 · Used by 1

Statement usesPointwise bound behind the p-biased inequality

Proof usesStatement of the one-variable p-biased inequality · Reduction of the p-biased two-point inequality to one variable · Pointwise bound implies the one-variable p-biased inequality

Used byp-biased two-point inequality

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.