Convex comparison under sub-Gaussian tails

StructureRandom variables with a 1-sub-Gaussian tail#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\). A function \(X : \Omega \to \mathbb{R}\) has a 1-sub-Gaussian tail when it is measurable and integrable, has mean \(\int X \, d\mu = 0\), and satisfies \(\mu\{\omega : |X(\omega)| > t\} \le 2 e^{-t^2/2}\) for every real \(t \ge 0\).

structure IsOneSubGaussianTail {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ) : Prop where
  measurable : Measurable X
  integrable : Integrable X μ
  mean_zero : ∫ ω, X ω ∂μ = 0
  tail_le : ∀ t : ℝ, 0 ≤ t →
    μ {ω | |X ω| > t} ≤ ENNReal.ofReal (2 * Real.exp (-t ^ 2 / 2))

Used by 4

Used byDavis–Power extremal variable · Admissible constants compare variables on every sample space · Admissible convex sub-Gaussian comparison constants · Admissible comparison constants are at least one

DefinitionConvex domination#✓fully proved

Let \(\mu_X\) and \(\mu_Y\) be measures on measurable spaces \(\Omega_X\) and \(\Omega_Y\), and let \(X : \Omega_X \to \mathbb{R}\) and \(Y : \Omega_Y \to \mathbb{R}\). Then \(X\) (under \(\mu_X\)) is convexly dominated by \(Y\) (under \(\mu_Y\)) when every convex function \(f : \mathbb{R} \to \mathbb{R}\) for which \(f \circ X\) is \(\mu_X\)-integrable and \(f \circ Y\) is \(\mu_Y\)-integrable satisfies \(\int f(X) \, d\mu_X \le \int f(Y) \, d\mu_Y\).

def ConvexDominated {ΩX ΩY : Type*}
    [MeasurableSpace ΩX] [MeasurableSpace ΩY]
    (μX : Measure ΩX) (X : ΩX → ℝ) (μY : Measure ΩY) (Y : ΩY → ℝ) : Prop :=
  ∀ f : ℝ → ℝ, ConvexOn ℝ univ f →
    Integrable (fun ω => f (X ω)) μX →
    Integrable (fun ω => f (Y ω)) μY →
    (∫ ω, f (X ω) ∂μX) ≤ ∫ ω, f (Y ω) ∂μY

Used by 4

Used byDavis–Power extremal variable · Admissible constants compare variables on every sample space · Admissible convex sub-Gaussian comparison constants · Admissible comparison constants are at least one

DefinitionAdmissible convex sub-Gaussian comparison constants#✓fully proved

An extended nonnegative real \(C \in [0, \infty]\) is an admissible comparison constant when \(0 < C < \infty\) and, for every probability measure \(\mu\) on a measurable space \(\Omega\) and every function \(X : \Omega \to \mathbb{R}\) with a 1-sub-Gaussian tail under \(\mu\), \(X\) under \(\mu\) is convexly dominated by the function \(g \mapsto \sqrt{C}\, g\) under the standard Gaussian measure \(\mathcal{N}(0, 1)\) on \(\mathbb{R}\).

def IsAdmissibleConstant (C : ENNReal) : Prop :=
  C ≠ ⊤ ∧ 0 < C ∧
    ∀ (Ω : Type) [MeasurableSpace Ω]
      (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ),
      IsOneSubGaussianTail μ X →
        ConvexDominated μ X (gaussianReal 0 1) (fun g : ℝ => Real.sqrt C.toReal * g)

Uses 2 · Used by 6

Statement usesConvex domination · Random variables with a 1-sub-Gaussian tail

Used byThe convex sub-Gaussian comparison constant · Davis–Power lower bound for admissible variance factors · Davis–Power upper bound: \(c_0^2\) is an admissible variance factor · Admissible constants compare variables on every sample space · The comparison constant is at least one · Admissible comparison constants are at least one

DefinitionThe convex sub-Gaussian comparison constant#✓fully proved

The comparison constant is the infimum, in \([0, \infty]\), of the set of admissible comparison constants \(C\); it equals \(\infty\) when no admissible constant exists.

noncomputable def comparisonConstant : ENNReal :=
  sInf {C : ENNReal | IsAdmissibleConstant C}

Uses 1 · Used by 3

Statement usesAdmissible convex sub-Gaussian comparison constants

Used byDavis–Power value of the convex sub-Gaussian comparison constant · Finiteness of the convex sub-Gaussian comparison constant · The comparison constant is at least one

DefinitionThe capped Gaussian tail envelope#✓fully proved

For a real number \(t\), the capped Gaussian tail envelope at \(t\) is \(\min\{1, 2 e^{-t^2/2}\}\).

noncomputable def gaussianTailEnvelope (t : ℝ) : ℝ :=
  min 1 (2 * Real.exp (-t ^ 2 / 2))

Used by 2

Used byThe envelope integral \(A\) · Saturating the Gaussian tail envelope

TheoremAdmissible comparison constants are at least one#✓fully proved

Every admissible comparison constant \(C\) satisfies \(C \ge 1\).

The proof applies the comparison to a standard Gaussian variable and the convex test function \(x \mapsto x^2\).

theorem one_le_of_isAdmissibleConstant {C : ENNReal} (hC : IsAdmissibleConstant C) :
    1 ≤ C

Uses 3 · Used by 1

Statement usesAdmissible convex sub-Gaussian comparison constants

Proof usesConvex domination · Random variables with a 1-sub-Gaussian tail

Used byThe comparison constant is at least one

TheoremThe comparison constant is at least one#✓fully proved

The convex sub-Gaussian comparison constant is at least \(1\). This holds also when no admissible comparison constant exists, in which case the constant is \(\infty\).

theorem one_le_comparisonConstant : (1 : ENNReal) ≤ comparisonConstant

Uses 3

Statement usesThe convex sub-Gaussian comparison constant

Proof usesAdmissible convex sub-Gaussian comparison constants · Admissible comparison constants are at least one

TheoremAdmissible constants compare variables on every sample space#✓fully proved

Let \(C\) be an admissible comparison constant, let \(\mu\) be a probability measure on a measurable space \(\Omega\), and let \(X : \Omega \to \mathbb{R}\) have a 1-sub-Gaussian tail. Then \(X\) is convexly dominated by \(\sqrt{C}\,G\), where \(G\) is a standard Gaussian random variable (the identity on \(\mathbb{R}\) under the standard normal law \(N(0, 1)\)).

The definition of admissibility quantifies only over sample spaces in the lowest universe; this form allows \(\Omega\) in any universe, by pushing the law of \(X\) forward to a probability measure on \(\mathbb{R}\).

theorem IsAdmissibleConstant.elim {C : ENNReal} (hC : IsAdmissibleConstant C)
    {Ω : Type u} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (X : Ω → ℝ) (hX : IsOneSubGaussianTail μ X) :
    ConvexDominated μ X (gaussianReal 0 1) (fun g : ℝ => Real.sqrt C.toReal * g)

Uses 3

Statement usesConvex domination · Admissible convex sub-Gaussian comparison constants · Random variables with a 1-sub-Gaussian tail

DefinitionSaturating the Gaussian tail envelope#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\Omega\). A function \(X : \Omega \to \mathbb{R}\) saturates the Gaussian tail when \(\mu\{\omega : |X(\omega)| > t\} = \min\{1, 2 e^{-t^2/2}\}\) for every real \(t \ge 0\), that is, its strict tails equal the capped Gaussian tail envelope.

def SaturatesGaussianTail {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) (X : Ω → ℝ) : Prop :=
  ∀ t : ℝ, 0 ≤ t →
    μ {ω | |X ω| > t} = ENNReal.ofReal (gaussianTailEnvelope t)

Uses 1 · Used by 1

Statement usesThe capped Gaussian tail envelope

Used byDavis–Power extremal variable

DefinitionStandard Gaussian upper tail#✓fully proved

For a real number \(x\), the standard Gaussian upper tail at \(x\) is \(Q(x) = \int_x^\infty \varphi(t)\,dt\), where \(\varphi(t) = e^{-t^2/2}/\sqrt{2\pi}\) is the standard Gaussian density.

noncomputable def standardNormalTail (x : ℝ) : ℝ :=
  ∫ t in Ici x, gaussianPDFReal 0 1 t

Used by 1

Used byValid solutions of the Davis–Power system

DefinitionThe Davis–Power transition threshold#✓fully proved

The transition threshold is the real number \(t_0 = \sqrt{2\log 2}\), where \(\log\) is the natural logarithm.

noncomputable def davisPowerT0 : ℝ :=
  Real.sqrt (2 * Real.log 2)

Used by 1

Used byValid solutions of the Davis–Power system

DefinitionThe envelope integral \(A\)#✓fully proved

Let \(A = \int_0^\infty \min(1, 2e^{-t^2/2})\,dt\), the integral over \([0, \infty)\) of the capped Gaussian tail envelope \(t \mapsto \min(1, 2e^{-t^2/2})\).

This integral appears in equation (3) of Davis–Power (2026).

noncomputable def davisPowerA : ℝ :=
  ∫ t in Ici (0 : ℝ), gaussianTailEnvelope t

Uses 1 · Used by 1

Statement usesThe capped Gaussian tail envelope

Used byHalf the envelope integral, \(B\)

DefinitionHalf the envelope integral, \(B\)#✓fully proved

Let \(B = A/2\), where \(A = \int_0^\infty \min(1, 2e^{-t^2/2})\,dt\) is the integral over \([0, \infty)\) of the capped Gaussian tail envelope.

This constant appears in equation (3) of Davis–Power (2026).

noncomputable def davisPowerB : ℝ :=
  davisPowerA / 2

Uses 1 · Used by 1

Statement usesThe envelope integral \(A\)

Used byValid solutions of the Davis–Power system

DefinitionThe function \(h\) of Davis–Power#✓fully proved

For real \(x\), let \(h(x) = 2x e^{-x^2/2} + 2\int_x^\infty e^{-t^2/2}\,dt\).

This is equation (4) of Davis–Power (2026); the Davis–Power equation system uses \(h\) only at points above the transition threshold \(\sqrt{2 \log 2}\).

noncomputable def davisPowerH (x : ℝ) : ℝ :=
  2 * x * Real.exp (-x ^ 2 / 2) + 2 * ∫ t in Ici x, Real.exp (-t ^ 2 / 2)

Used by 1

Used byValid solutions of the Davis–Power system

StructureParameter quadruples of the Davis–Power system#✓fully proved

A parameter quadruple is a quadruple \((a, p_0, z, c_0)\) of real numbers, the unknowns of the Davis–Power equation system. Being a solution of the system is a separate condition.

@[ext] structure DavisPowerSolution where
  a : ℝ
  p0 : ℝ
  z : ℝ
  c0 : ℝ

Used by 3

Used byValues of \(c_0\) solving the Davis–Power system · Existence and uniqueness for the Davis–Power system · Valid solutions of the Davis–Power system

DefinitionValid solutions of the Davis–Power system#✓fully proved

Let \(\varphi(t) = e^{-t^2/2}/\sqrt{2\pi}\) be the standard Gaussian density, \(Q(x) = \int_x^\infty \varphi(t)\,dt\) its upper tail, \(t_0 = \sqrt{2\log 2}\) with \(\log\) the natural logarithm, \(B = \frac{1}{2}\int_0^\infty \min(1, 2e^{-t^2/2})\,dt\) and \(h(x) = 2x e^{-x^2/2} + 2\int_x^\infty e^{-t^2/2}\,dt\). A quadruple \((a, p_0, z, c_0)\) of real numbers is a valid solution of the Davis–Power system when \(a > t_0\), \(h(a) = B\), \(p_0 = 2e^{-a^2/2}\), \(0 < p_0 < 1\), \(Q(z) = p_0\) and \(c_0 = B/\varphi(z)\).

These are equations (3)–(6) of Davis–Power (2026), with the domain conditions that select the solution.

noncomputable def DavisPowerSolution.IsValid (q : DavisPowerSolution) : Prop :=
  davisPowerT0 < q.a ∧
    davisPowerH q.a = davisPowerB ∧
    q.p0 = 2 * Real.exp (-q.a ^ 2 / 2) ∧
    0 < q.p0 ∧ q.p0 < 1 ∧
    standardNormalTail q.z = q.p0 ∧
    q.c0 = davisPowerB / gaussianPDFReal 0 1 q.z

Uses 5 · Used by 2

Statement usesParameter quadruples of the Davis–Power system · Half the envelope integral, \(B\) · The function \(h\) of Davis–Power · The Davis–Power transition threshold · Standard Gaussian upper tail

Used byValues of \(c_0\) solving the Davis–Power system · Existence and uniqueness for the Davis–Power system

DefinitionValues of \(c_0\) solving the Davis–Power system#✓fully proved

Let \(\varphi(t) = e^{-t^2/2}/\sqrt{2\pi}\) be the standard Gaussian density, \(B = \frac12 \int_0^\infty \min(1, 2e^{-t^2/2})\,dt\) and \(h(x) = 2x e^{-x^2/2} + 2\int_x^\infty e^{-t^2/2}\,dt\). This is the set of reals \(c_0\) for which there are reals \(a\), \(p_0\), \(z\) with \(a > \sqrt{2 \log 2}\), \(h(a) = B\), \(p_0 = 2e^{-a^2/2}\), \(0 < p_0 < 1\), \(\int_z^\infty \varphi(t)\,dt = p_0\) and \(c_0 = B / \varphi(z)\).

noncomputable def davisPowerC0Values : Set ℝ :=
  {c | ∃ q : DavisPowerSolution, q.IsValid ∧ q.c0 = c}

Uses 2 · Used by 1

Statement usesParameter quadruples of the Davis–Power system · Valid solutions of the Davis–Power system

Used byThe Davis–Power constant \(c_0\)

DefinitionThe Davis–Power constant \(c_0\)#✓fully proved

Let \(\varphi(t) = e^{-t^2/2}/\sqrt{2\pi}\) be the standard Gaussian density, \(B = \frac12 \int_0^\infty \min(1, 2e^{-t^2/2})\,dt\) and \(h(x) = 2x e^{-x^2/2} + 2\int_x^\infty e^{-t^2/2}\,dt\). The constant \(c_0\) is the infimum of the set of reals \(c\) for which there are reals \(a\), \(p_0\), \(z\) with \(a > \sqrt{2 \log 2}\), \(h(a) = B\), \(p_0 = 2e^{-a^2/2}\), \(0 < p_0 < 1\), \(\int_z^\infty \varphi(t)\,dt = p_0\) and \(c = B / \varphi(z)\). The infimum of a set of reals that is empty or unbounded below is taken to be \(0\).

If the system has exactly one solution \((a, p_0, z, c)\), then \(c_0 = c\). The constant is defined from the equation system, not from numerical data.

noncomputable def davisPowerC0 : ℝ :=
  sInf davisPowerC0Values

Uses 1 · Used by 4

Statement usesValues of \(c_0\) solving the Davis–Power system

Used byDavis–Power value of the convex sub-Gaussian comparison constant · Davis–Power extremal variable · Davis–Power lower bound for admissible variance factors · Davis–Power upper bound: \(c_0^2\) is an admissible variance factor

TheoremExistence and uniqueness for the Davis–Power system#●ready to prove

There is exactly one quadruple \((a, p_0, z, c_0)\) of real numbers that is a valid solution of the Davis–Power system.

theorem_wanted davisPowerSystem_existsUnique :
    ∃! q : DavisPowerSolution, q.IsValid

Sources

• Davis–Power (2026), equations (3)–(6), existence and uniqueness.

Uses 2

Statement usesParameter quadruples of the Davis–Power system · Valid solutions of the Davis–Power system

TheoremFiniteness of the convex sub-Gaussian comparison constant#●ready to prove

The comparison constant is finite. Here the comparison constant is the infimum, in \([0, \infty]\), of the variance factors \(C \in (0, \infty)\) such that every real random variable \(X\) on a probability space that is integrable, has mean zero and satisfies \(P(|X| > t) \le 2e^{-t^2/2}\) for all \(t \ge 0\) satisfies \(E f(X) \le E f(\sqrt{C}\,G)\) for every convex \(f : \mathbb{R} \to \mathbb{R}\) for which both expectations are finite, where \(G\) is a standard Gaussian. Equivalently, such a factor \(C\) exists.

theorem_wanted historicalFinitenessUpperBound :
    comparisonConstant ≠ ⊤

Sources

• van Handel (2025), historical one-dimensional finiteness consequence.

Uses 1

Statement usesThe convex sub-Gaussian comparison constant

TheoremDavis–Power upper bound: \(c_0^2\) is an admissible variance factor#●ready to prove

Let \(c_0\) be the Davis–Power constant and \(G\) a standard Gaussian. Then \(c_0^2 > 0\), and every real random variable \(X\) on a probability space that is measurable and integrable, has mean \(0\) and satisfies \(\mathbb{P}(|X| > t) \le 2e^{-t^2/2}\) for all \(t \ge 0\) is dominated by \(|c_0|\,G\) in the convex order. Here a real random variable \(X\) is dominated by \(Y\) in the convex order when \(\mathbb{E} f(X) \le \mathbb{E} f(Y)\) for every convex \(f : \mathbb{R} \to \mathbb{R}\) such that \(f(X)\) and \(f(Y)\) are integrable.

theorem_wanted davisPowerSharpUpper :
    IsAdmissibleConstant (ENNReal.ofReal (davisPowerC0 ^ 2))

Sources

• Davis–Power (2026), Theorem 1, the exact c0^2 comparator upper bound.

Uses 2

Statement usesAdmissible convex sub-Gaussian comparison constants · The Davis–Power constant \(c_0\)

TheoremDavis–Power lower bound for admissible variance factors#●ready to prove

Every admissible variance factor \(C \in [0, \infty]\) satisfies \(c_0^2 \le C\), where \(c_0\) is the Davis–Power constant. Here \(C\) is admissible when \(0 < C < \infty\) and every real random variable \(X\) on a probability space that is measurable and integrable, has mean \(0\) and satisfies \(\mathbb{P}(|X| > t) \le 2e^{-t^2/2}\) for all \(t \ge 0\) is dominated by \(\sqrt{C}\,G\) in the convex order, with \(G\) a standard Gaussian; a real random variable \(X\) on a probability space is dominated by \(Y\) in the convex order when \(\mathbb{E} f(X) \le \mathbb{E} f(Y)\) for every convex \(f : \mathbb{R} \to \mathbb{R}\) such that \(f(X)\) and \(f(Y)\) are integrable.

theorem_wanted davisPowerSharpLower (C : ENNReal) (hC : IsAdmissibleConstant C) :
    ENNReal.ofReal (davisPowerC0 ^ 2) ≤ C

Sources

• Davis–Power (2026), Theorem 1, sharpness for every admissible variance factor.

Uses 2

Statement usesAdmissible convex sub-Gaussian comparison constants · The Davis–Power constant \(c_0\)

TheoremDavis–Power value of the convex sub-Gaussian comparison constant#●ready to prove

The convex sub-Gaussian comparison constant, the infimum in \([0, \infty]\) of all admissible variance factors, equals \(c_0^2\), where \(c_0\) is the Davis–Power constant.

theorem_wanted comparisonConstant_eq_davisPowerC0_sq :
    comparisonConstant = ENNReal.ofReal (davisPowerC0 ^ 2)

Sources

• Davis–Power (2026), the exact solved one-dimensional catalogue constant.

Uses 2

Statement usesThe convex sub-Gaussian comparison constant · The Davis–Power constant \(c_0\)

TheoremDavis–Power extremal variable#●ready to prove

Let \(c_0\) be the Davis–Power constant and \(G\) a standard Gaussian, and say that a real random variable \(X\) is dominated by \(Y\) in the convex order when \(\mathbb{E} f(X) \le \mathbb{E} f(Y)\) for every convex \(f : \mathbb{R} \to \mathbb{R}\) such that \(f(X)\) and \(f(Y)\) are integrable. There is a real random variable \(X\) on a probability space that is measurable and integrable, has mean \(0\) and satisfies \(\mathbb{P}(|X| > t) \le 2e^{-t^2/2}\) for all \(t \ge 0\), whose tail saturates the capped envelope, \(\mathbb{P}(|X| > t) = \min(1, 2e^{-t^2/2})\) for every \(t \ge 0\), and such that for every real \(c\) with \(0 < c < c_0\), \(X\) is not dominated by \(cG\) in the convex order.

theorem_wanted davisPowerExtremalAttainment :
    ∃ (Ω : Type) (m : MeasurableSpace Ω)
      (μ : @Measure Ω m) (hμ : @IsProbabilityMeasure Ω m μ) (X : Ω → ℝ),
      @IsOneSubGaussianTail Ω m μ hμ X ∧ SaturatesGaussianTail μ X ∧
        ∀ c : ℝ, 0 < c → c < davisPowerC0 →
          ¬ConvexDominated μ X (gaussianReal 0 1) (fun g : ℝ => c * g)

Sources

• Davis–Power (2026), the tail-saturating extremizer and smaller-factor sharpness.

Uses 4

Statement usesConvex domination · Random variables with a 1-sub-Gaussian tail · Saturating the Gaussian tail envelope · The Davis–Power constant \(c_0\)

18 fully proved6 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.