Gaussian Comparison Constants and Named Results

This file defines the explicit constants (t0, A, B, a, p0, z, c0) and the two named results:

• gaussianDomination_c0: convex domination at the sharp scale
• gaussianSharpness_below_c0: failure below the sharp scale

@[reducible, inline]

abbrev ConvexSubgaussian.t0 : ℝ

The tail-cap transition point sqrt (2 log 2).

Equations

• ConvexSubgaussian.t0 = OneDimConvexDom.t0

@[reducible, inline]

abbrev ConvexSubgaussian.A : ℝ

The total sub-Gaussian tail-envelope mass.

Equations

• ConvexSubgaussian.A = OneDimConvexDom.A

@[reducible, inline]

abbrev ConvexSubgaussian.B : ℝ

The half-mass constant A / 2.

Equations

• ConvexSubgaussian.B = OneDimConvexDom.B

@[reducible, inline]

abbrev ConvexSubgaussian.a : ℝ

The unique threshold solving H(a) = B.

Equations

• ConvexSubgaussian.a = OneDimConvexDom.a

@[reducible, inline]

abbrev ConvexSubgaussian.p0 : ℝ

The plateau height p₀ = 2 exp (-a² / 2).

Equations

• ConvexSubgaussian.p0 = OneDimConvexDom.p0

@[reducible, inline]

abbrev ConvexSubgaussian.z : ℝ

The Gaussian tail quantile satisfying PhiBar z = p₀.

Equations

• ConvexSubgaussian.z = OneDimConvexDom.z

@[reducible, inline]

abbrev ConvexSubgaussian.c0 : ℝ

The optimal Gaussian comparison scale.

Equations

• ConvexSubgaussian.c0 = OneDimConvexDom.c0

@[reducible, inline]

abbrev ConvexSubgaussian.gaussianScale (c : ℝ) : MeasureTheory.Measure ℝ

The centered Gaussian law with standard deviation c.

Equations

• ConvexSubgaussian.gaussianScale c = OneDimConvexDom.gaussianScale c

theorem ConvexSubgaussian.gaussianDomination_c0 {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (X : Ω → ℝ) (hX : IsOneSubgaussian P X) {f : ℝ → ℝ} (hf : ConvexOn ℝ Set.univ f) (hPX : MeasureTheory.Integrable (fun (ω : Ω) => f (X ω)) P) (hG : MeasureTheory.Integrable f (gaussianScale c0)) : ∫ (ω : Ω), f (X ω) ∂P ≤ ∫ (x : ℝ), f x ∂gaussianScale c0

Convex domination at the sharp Gaussian scale c₀.

theorem ConvexSubgaussian.gaussianSharpness_below_c0 {c : ℝ} (hc : 0 < c) (hc_lt : 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

Sharpness below c₀: the canonical extremal witness beats the Gaussian.