Sharp Gaussian Comparison Theorem

This file contains the main theorem: the sharp one-dimensional convex sub-Gaussian comparison constant is c0, and no smaller Gaussian scale suffices.

def ConvexSubgaussian.AdmissibleScale (c : ℝ) : Prop

AdmissibleScale c is the statement

0 < c ∧
  ∀ {Ω : Type} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P]
    (X : Ω → Real), IsOneSubgaussian P X →
    ∀ {f : Real → Real}, ConvexOn Real Set.univ f →
      Integrable (fun ω => f (X ω)) P →
      Integrable f (gaussianScale c) →
      (∫ ω, f (X ω) ∂P) <= (∫ x, f x ∂(gaussianScale c))

In words: c is admissible iff c > 0 and every tail-sense one-sub-Gaussian real random variable is convex-dominated by the centered Gaussian law of scale c, for every convex test function whose two expectations are finite.

Equations

• One or more equations did not get rendered due to their size.

def ConvexSubgaussian.cStar : ℝ

The sharp one-dimensional Gaussian convex-comparison constant, defined as the infimum of admissible Gaussian scales.

Equations

• ConvexSubgaussian.cStar = sInf {c : ℝ | ConvexSubgaussian.AdmissibleScale c}

theorem ConvexSubgaussian.sharp_convexSubgaussianComparison : cStar = c0 ∧ (∀ {Ω : Type} [inst : MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (X : Ω → ℝ), IsOneSubgaussian P X → ∀ {f : ℝ → ℝ}, ConvexOn ℝ Set.univ f → MeasureTheory.Integrable (fun (ω : Ω) => f (X ω)) P → MeasureTheory.Integrable f (gaussianScale c0) → ∫ (ω : Ω), f (X ω) ∂P ≤ ∫ (x : ℝ), f x ∂gaussianScale c0) ∧ ∀ (c : ℝ), 0 < c → c < c0 → MeasureTheory.IsProbabilityMeasure OneDimConvexDom.muStar ∧ (IsOneSubgaussian OneDimConvexDom.muStar fun (x : ℝ) => x) ∧ ∃ (u : ℝ), 0 ≤ u ∧ ∫ (x : ℝ), psi u x ∂OneDimConvexDom.muStar > ∫ (x : ℝ), psi u x ∂gaussianScale c

Sharp one-dimensional convex sub-Gaussian comparison.

• cStar = c0
• c0 is admissible
• every smaller positive scale fails, witnessed by an explicit hinge test against the canonical extremal law