Internal Gaussian Proof

This internal module contains the main body of the existing formal proof.

Reader-facing API wrappers live in:

• ConvexSubgaussian.GaussianAsymptotics
• ConvexSubgaussian.GaussianMain

theorem OneDimConvexDom.stopLossDom_integral_convex {mu nu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] [MeasureTheory.IsProbabilityMeasure nu] (hDom : StopLossDom mu nu) {f : ℝ → ℝ} (hf : IsSimpleConvex f) (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) (hIntNuId : MeasureTheory.Integrable (fun (x : ℝ) => x) nu) (_hmu : MeasureTheory.Integrable f mu) (_hnu : MeasureTheory.Integrable f nu) : ∫ (x : ℝ), f x ∂mu ≤ ∫ (x : ℝ), f x ∂nu

2. Tail cap and envelope constants

def OneDimConvexDom.s (t : ℝ) : ℝ

Equations

• OneDimConvexDom.s t = min 1 (2 * Real.exp (-t ^ 2 / 2))

def OneDimConvexDom.t0 : ℝ

Equations

• OneDimConvexDom.t0 = √(2 * Real.log 2)

def OneDimConvexDom.A : ℝ

Equations

• OneDimConvexDom.A = ∫ (t : ℝ) in Set.Ioi 0, OneDimConvexDom.s t

def OneDimConvexDom.B : ℝ

Equations

• OneDimConvexDom.B = OneDimConvexDom.A / 2

def OneDimConvexDom.H (x : ℝ) : ℝ

Equations

• OneDimConvexDom.H x = x * OneDimConvexDom.s x + ∫ (t : ℝ) in Set.Ioi x, OneDimConvexDom.s t

theorem OneDimConvexDom.H_strictAntiOn : StrictAntiOn H (Set.Ioi t0)

theorem OneDimConvexDom.H_at_t0 : H t0 = A

theorem OneDimConvexDom.H_tendsto_zero : Filter.Tendsto H Filter.atTop (nhds 0)

theorem OneDimConvexDom.exists_unique_a : ∃! a : ℝ, a > t0 ∧ H a = B

noncomputable def OneDimConvexDom.a : ℝ

Equations

• OneDimConvexDom.a = Classical.choose OneDimConvexDom.exists_unique_a

theorem OneDimConvexDom.a_spec : a > t0 ∧ H a = B

def OneDimConvexDom.p0 : ℝ

Equations

• OneDimConvexDom.p0 = OneDimConvexDom.s OneDimConvexDom.a

def OneDimConvexDom.J (u : ℝ) : ℝ

Equations

• OneDimConvexDom.J u = if u ≤ OneDimConvexDom.a then OneDimConvexDom.B - OneDimConvexDom.p0 * u else ∫ (t : ℝ) in Set.Ioi u, OneDimConvexDom.s t

theorem OneDimConvexDom.J_of_le_a {u : ℝ} (hu : u ≤ a) : J u = B - p0 * u

theorem OneDimConvexDom.J_of_gt_a {u : ℝ} (hu : a < u) : J u = ∫ (t : ℝ) in Set.Ioi u, s t

theorem OneDimConvexDom.t0_pos : 0 < t0

theorem OneDimConvexDom.s_eq_gauss_tail_of_gt_t0 {x : ℝ} (hx : x > t0) : s x = 2 * Real.exp (-x ^ 2 / 2)

theorem OneDimConvexDom.s_integrableOn_Ioi_zero : MeasureTheory.IntegrableOn (fun (t : ℝ) => s t) (Set.Ioi 0) MeasureTheory.volume

theorem OneDimConvexDom.s_le_p0_of_ge_a {x : ℝ} (hx : a ≤ x) : s x ≤ p0

def OneDimConvexDom.t1 : ℝ

Equations

• OneDimConvexDom.t1 = √(2 * Real.log 4)

theorem OneDimConvexDom.t1_pos : 0 < t1

theorem OneDimConvexDom.t0_lt_t1 : t0 < t1

theorem OneDimConvexDom.two_exp_neg_t1_sq_div_two_eq_half : 2 * Real.exp (-t1 ^ 2 / 2) = 1 / 2

theorem OneDimConvexDom.s_t1_eq_half : s t1 = 1 / 2

theorem OneDimConvexDom.integral_s_Ioc_0_t1_lt_t1 : ∫ (t : ℝ) in Set.Ioc 0 t1, s t < t1

theorem OneDimConvexDom.H_t1_gt_B : H t1 > B

theorem OneDimConvexDom.a_gt_t1 : a > t1

theorem OneDimConvexDom.p0_lt_half : p0 < 1 / 2

3. Tail constraints and envelope

def OneDimConvexDom.prob (mu : MeasureTheory.Measure ℝ) (S : Set ℝ) : ℝ

Equations

• OneDimConvexDom.prob mu S = (mu S).toReal

def OneDimConvexDom.absTail (mu : MeasureTheory.Measure ℝ) (t : ℝ) : ℝ

Equations

• OneDimConvexDom.absTail mu t = OneDimConvexDom.prob mu {x : ℝ | |x| > t}

def OneDimConvexDom.subgaussianTail (mu : MeasureTheory.Measure ℝ) : Prop

Equations

• OneDimConvexDom.subgaussianTail mu = ∀ (t : ℝ), 0 ≤ t → OneDimConvexDom.absTail mu t ≤ 2 * Real.exp (-t ^ 2 / 2)

theorem OneDimConvexDom.J_eq_integral_Ioi_of_ge_a (x : ℝ) (hx : a ≤ x) : J x = ∫ (t : ℝ) in Set.Ioi x, s t

theorem OneDimConvexDom.layer_cake_hinge {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {Y : Ω → ℝ} (hY : MeasureTheory.Integrable Y P) (u : ℝ) : ∫ (ω : Ω), hinge u (Y ω) ∂P = ∫ (t : ℝ) in Set.Ioi u, (P {ω : Ω | Y ω > t}).toReal

theorem OneDimConvexDom.stopLoss_eq_integral_tail {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (u : ℝ) : stopLoss μ u = ∫ (t : ℝ) in Set.Ioi u, prob μ {x : ℝ | x > t}

theorem OneDimConvexDom.s_nonneg (t : ℝ) : 0 ≤ s t

theorem OneDimConvexDom.first_moment_bound {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) (htail : subgaussianTail mu) (hmean : mean mu = 0) : ∫ (x : ℝ), |x| ∂mu ≤ A ∧ stopLoss mu 0 ≤ B

theorem OneDimConvexDom.stopLoss_envelope_case_ge_a {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) (htail : subgaussianTail mu) (u : ℝ) (hu : a ≤ u) : stopLoss mu u ≤ J u

theorem OneDimConvexDom.hinge_convex_in_u (x : ℝ) : ConvexOn ℝ Set.univ fun (u : ℝ) => hinge u x

theorem OneDimConvexDom.stopLoss_convex {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) : ConvexOn ℝ Set.univ fun (u : ℝ) => stopLoss mu u

theorem OneDimConvexDom.stopLoss_envelope_case_le_a {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) (htail : subgaussianTail mu) (hmean : mean mu = 0) (u : ℝ) (hu0 : 0 ≤ u) (hua : u ≤ a) : stopLoss mu u ≤ J u

theorem OneDimConvexDom.stopLoss_envelope {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) (htail : subgaussianTail mu) (hmean : mean mu = 0) : (∀ (u : ℝ), 0 ≤ u → stopLoss mu u ≤ J u) ∧ ∀ (u : ℝ), 0 ≤ u → stopLoss (MeasureTheory.Measure.map (fun (x : ℝ) => -x) mu) u ≤ J u

theorem OneDimConvexDom.stopLoss_extend_all_u {mu nu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] [MeasureTheory.IsProbabilityMeasure nu] (hIntMu : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) (hIntNu : MeasureTheory.Integrable (fun (x : ℝ) => x) nu) (hmean : mean mu = mean nu) (hpos : ∀ (u : ℝ), 0 ≤ u → stopLoss mu u ≤ stopLoss nu u) (hneg : ∀ (u : ℝ), 0 ≤ u → stopLoss (MeasureTheory.Measure.map (fun (x : ℝ) => -x) mu) u ≤ stopLoss (MeasureTheory.Measure.map (fun (x : ℝ) => -x) nu) u) (u : ℝ) : stopLoss mu u ≤ stopLoss nu u

4. Gaussian objects and comparison

def OneDimConvexDom.phi (t : ℝ) : ℝ

Equations

• OneDimConvexDom.phi t = 1 / √(2 * Real.pi) * Real.exp (-t ^ 2 / 2)

def OneDimConvexDom.PhiBar (t : ℝ) : ℝ

Equations

• OneDimConvexDom.PhiBar t = ∫ (x : ℝ) in Set.Ioi t, OneDimConvexDom.phi x

def OneDimConvexDom.R (c u : ℝ) : ℝ

Equations

• OneDimConvexDom.R c u = OneDimConvexDom.PhiBar (u / c) / (2 * Real.exp (-u ^ 2 / 2))

theorem OneDimConvexDom.phi_pos (x : ℝ) : 0 < phi x

theorem OneDimConvexDom.phi_nonneg (x : ℝ) : 0 ≤ phi x

theorem OneDimConvexDom.phi_integrable : MeasureTheory.Integrable (fun (x : ℝ) => phi x) MeasureTheory.volume

theorem OneDimConvexDom.integral_phi_univ : ∫ (x : ℝ), phi x = 1

theorem OneDimConvexDom.phi_deriv (x : ℝ) : deriv phi x = -x * phi x

theorem OneDimConvexDom.integral_Ioi_mul_exp_neg_sq_half (a : ℝ) : ∫ (x : ℝ) in Set.Ioi a, x * Real.exp (-x ^ 2 / 2) = Real.exp (-a ^ 2 / 2)

theorem OneDimConvexDom.integral_Ioi_mul_phi (a : ℝ) : ∫ (x : ℝ) in Set.Ioi a, x * phi x = phi a

theorem OneDimConvexDom.PhiBar_strictAnti : StrictAnti PhiBar

theorem OneDimConvexDom.PhiBar_tendsto_atTop_zero : Filter.Tendsto PhiBar Filter.atTop (nhds 0)

theorem OneDimConvexDom.PhiBar_tendsto_atBot_one : Filter.Tendsto PhiBar Filter.atBot (nhds 1)

theorem OneDimConvexDom.PhiBar_continuous : Continuous PhiBar

theorem OneDimConvexDom.PhiBar_deriv (t : ℝ) : deriv PhiBar t = -phi t

def OneDimConvexDom.gaussianMeasure : MeasureTheory.Measure ℝ

Equations

• OneDimConvexDom.gaussianMeasure = ProbabilityTheory.gaussianReal 0 1

theorem OneDimConvexDom.gaussian_isProbability : MeasureTheory.IsProbabilityMeasure gaussianMeasure

instance OneDimConvexDom.instIsProbabilityMeasureRealGaussianMeasure : MeasureTheory.IsProbabilityMeasure gaussianMeasure

def OneDimConvexDom.gaussianScale (c : ℝ) : MeasureTheory.Measure ℝ

Equations

• OneDimConvexDom.gaussianScale c = MeasureTheory.Measure.map (fun (x : ℝ) => c * x) OneDimConvexDom.gaussianMeasure

theorem OneDimConvexDom.gaussianScale_isProbability (c : ℝ) : MeasureTheory.IsProbabilityMeasure (gaussianScale c)

def OneDimConvexDom.gClosed (c u : ℝ) : ℝ

Equations

• OneDimConvexDom.gClosed c u = c * OneDimConvexDom.phi (u / c) - u * OneDimConvexDom.PhiBar (u / c)

def OneDimConvexDom.gSL (c u : ℝ) : ℝ

Equations

• OneDimConvexDom.gSL c u = OneDimConvexDom.stopLoss (OneDimConvexDom.gaussianScale c) u

theorem OneDimConvexDom.gaussian_call_closed_form (c u : ℝ) (hc : 0 < c) : ∫ (x : ℝ), hinge u (c * x) * phi x = c * phi (u / c) - u * PhiBar (u / c)

theorem OneDimConvexDom.gSL_eq_gClosed (c u : ℝ) (hc : 0 < c) : gSL c u = gClosed c u

theorem OneDimConvexDom.gClosed_deriv (c : ℝ) (hc : 0 < c) : (deriv fun (u : ℝ) => gClosed c u) = fun (u : ℝ) => -PhiBar (u / c)

theorem OneDimConvexDom.gClosed_convex (c : ℝ) (hc : 0 < c) : ConvexOn ℝ Set.univ fun (u : ℝ) => gClosed c u

theorem OneDimConvexDom.exists_unique_z : ∃! z : ℝ, PhiBar z = p0

noncomputable def OneDimConvexDom.z : ℝ

Equations

• OneDimConvexDom.z = Classical.choose OneDimConvexDom.exists_unique_z

theorem OneDimConvexDom.z_spec : PhiBar z = p0

theorem OneDimConvexDom.PhiBar_zero_eq_half : PhiBar 0 = 1 / 2

theorem OneDimConvexDom.z_pos : 0 < z

noncomputable def OneDimConvexDom.c0 : ℝ

Equations

• OneDimConvexDom.c0 = OneDimConvexDom.B / OneDimConvexDom.phi OneDimConvexDom.z

noncomputable def OneDimConvexDom.uStar : ℝ

Equations

• OneDimConvexDom.uStar = OneDimConvexDom.c0 * OneDimConvexDom.z

theorem OneDimConvexDom.gaussian_tangent : deriv (fun (u : ℝ) => gClosed c0 u) uStar = -p0 ∧ gClosed c0 uStar = B - p0 * uStar

theorem OneDimConvexDom.gaussian_above_tangent_line (u : ℝ) : gClosed c0 u ≥ B - p0 * u

theorem OneDimConvexDom.lemma_gauss_ge_J_case1 (_h_cond1 : a * (1 - 1 / c0 ^ 2) > 1) (_h_cond2 : c0 > 1) (u : ℝ) (_hu : 0 ≤ u) (hua : u ≤ a) : J u ≤ gClosed c0 u

theorem OneDimConvexDom.D_nonneg_at_a (_h_cond2 : c0 > 1) : gClosed c0 a ≥ J a

theorem OneDimConvexDom.PhiBar_pos (t : ℝ) : 0 < PhiBar t

theorem OneDimConvexDom.integral_Ioc_0_t0_eq_t0_for_s : ∫ (t : ℝ) in Set.Ioc 0 t0, s t = t0

Numeric side condition kept as an explicit assumption.

theorem OneDimConvexDom.integral_Ioc_t0_t1_s_ge_half_len : (t1 - t0) / 2 ≤ ∫ (t : ℝ) in Set.Ioc t0 t1, s t

theorem OneDimConvexDom.A_ge_t0_plus_half_t1_sub_t0 : t0 + (t1 - t0) / 2 ≤ A

theorem OneDimConvexDom.B_ge_sum_t0_t1_div_four : (t0 + t1) / 4 ≤ B

theorem OneDimConvexDom.t0_gt_117_div_100 : 117 / 100 < t0

theorem OneDimConvexDom.t1_gt_166_div_100 : 166 / 100 < t1

theorem OneDimConvexDom.phi_upper_uniform (t : ℝ) : phi t ≤ 1 / √(2 * Real.pi)

theorem OneDimConvexDom.inv_sqrt_two_pi_lt_two_fifths : 1 / √(2 * Real.pi) < 2 / 5

theorem OneDimConvexDom.phi_le_two_fifths (t : ℝ) : phi t ≤ 2 / 5

theorem OneDimConvexDom.B_gt_283_div_400 : 283 / 400 < B

theorem OneDimConvexDom.c0_gt_seven_fourths : 7 / 4 < c0

theorem OneDimConvexDom.a_gt_three_halves : 3 / 2 < a

theorem OneDimConvexDom.numerics_c0 : c0 > 1 ∧ a * (1 - 1 / c0 ^ 2) > 1

theorem OneDimConvexDom.J_tendsto_zero : Filter.Tendsto J Filter.atTop (nhds 0)

G1 boundary for Gaussian-vs-envelope: tail limit of J.

theorem OneDimConvexDom.integrableOn_phi_div_sq (x : ℝ) (hx : 0 < x) : MeasureTheory.IntegrableOn (fun (t : ℝ) => phi t / t ^ 2) (Set.Ioi x) MeasureTheory.volume

Canonical Mills-ratio upper bound: phi / PhiBar ≤ x + 1/x for x>0.

theorem OneDimConvexDom.phi_tail_ibp_Ioi (x : ℝ) (hx : 0 < x) : PhiBar x = phi x / x - ∫ (t : ℝ) in Set.Ioi x, phi t / t ^ 2

theorem OneDimConvexDom.mills_bounds (x : ℝ) (hx : 0 < x) : x / (1 + x ^ 2) * phi x ≤ PhiBar x ∧ PhiBar x ≤ 1 / x * phi x

theorem OneDimConvexDom.mills_ratio_bound (x : ℝ) : 0 < x → phi x / PhiBar x ≤ x + 1 / x

theorem OneDimConvexDom.R_strict_mono_on (h_cond1 : a * (1 - 1 / c0 ^ 2) > 1) (h_cond2 : c0 > 1) : StrictMonoOn (fun (u : ℝ) => R c0 u) (Set.Ici a)

Ratio monotonicity used in the Gaussian-vs-envelope comparison (Rmono in LaTeX).

theorem OneDimConvexDom.J_deriv_ge_a (u : ℝ) (hu : a < u) : deriv J u = -s u

theorem OneDimConvexDom.D_deriv_ge_a (h_cond2 : c0 > 1) (u : ℝ) (hu : a < u) : deriv (fun (u : ℝ) => gClosed c0 u - J u) u = 2 * Real.exp (-u ^ 2 / 2) * (1 - R c0 u)

theorem OneDimConvexDom.g_c0_tendsto_zero (h_cond2 : c0 > 1) : Filter.Tendsto (fun (u : ℝ) => gClosed c0 u) Filter.atTop (nhds 0)

theorem OneDimConvexDom.monotone_ratio_principle {a : ℝ} {D κ R : ℝ → ℝ} (hcont : ContinuousOn D (Set.Ici a)) (hdiff : DifferentiableOn ℝ D (Set.Ioi a)) (hderiv : ∀ u > a, deriv D u = κ u * (1 - R u)) (hkappa_pos : ∀ u > a, 0 < κ u) (hR_mono : MonotoneOn R (Set.Ioi a)) (h_start : 0 ≤ D a) (h_end : Filter.Tendsto D Filter.atTop (nhds 0)) (u : ℝ) : u ≥ a → 0 ≤ D u

Monotone-ratio principle used in the Gaussian-vs-envelope comparison.

theorem OneDimConvexDom.gaussian_dominates_J (u : ℝ) : 0 ≤ u → J u ≤ gClosed c0 u

5. Convex domination at scale c0

theorem OneDimConvexDom.mean_gaussianScale (c : ℝ) : mean (gaussianScale c) = 0

theorem OneDimConvexDom.J_ge_tangent_line (u : ℝ) : 0 ≤ u → B - p0 * u ≤ J u

6a. Extremal measure construction

noncomputable def OneDimConvexDom.fStar (x : ℝ) : ℝ

Equations

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

noncomputable def OneDimConvexDom.muStar : MeasureTheory.Measure ℝ

Equations

• OneDimConvexDom.muStar = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (OneDimConvexDom.fStar x)

theorem OneDimConvexDom.fStar_nonneg (x : ℝ) : 0 ≤ fStar x

theorem OneDimConvexDom.fStar_measurable : Measurable fStar

theorem OneDimConvexDom.integral_Ioi_fStar_of_ge_a {t : ℝ} (ht : a ≤ t) : ∫ (x : ℝ) in Set.Ioi t, fStar x = 2 * Real.exp (-t ^ 2 / 2)

theorem OneDimConvexDom.integral_Ioi_fStar_of_lt_a {t : ℝ} (ht : t < a) (ht0 : 0 ≤ t) : ∫ (x : ℝ) in Set.Ioi t, fStar x = 2 * Real.exp (-a ^ 2 / 2)

theorem OneDimConvexDom.integral_Ioi_muStar_meas_gt_eq (t : ℝ) : prob muStar (Set.Ioi t) = ∫ (x : ℝ) in Set.Ioi t, fStar x

theorem OneDimConvexDom.rightTail_muStar (t : ℝ) : 0 ≤ t → prob muStar {x : ℝ | x > t} = if t < OneDimConvexDom.a then p0 else 2 * Real.exp (-t ^ 2 / 2)

theorem OneDimConvexDom.hasDerivAt_two_exp_neg_sq_half (x : ℝ) : HasDerivAt (fun (x : ℝ) => 2 * Real.exp (-x ^ 2 / 2)) (-2 * x * Real.exp (-x ^ 2 / 2)) x

theorem OneDimConvexDom.integral_Icc_neg_a_neg_t_fStar {t : ℝ} (ht0 : t0 ≤ t) (hta : t ≤ a) : ∫ (x : ℝ) in Set.Icc (-a) (-t), fStar x = 2 * Real.exp (-t ^ 2 / 2) - p0

theorem OneDimConvexDom.integral_Iio_fStar_of_ge_t0_lt_a {t : ℝ} (ht0 : t0 ≤ t) (hta : t < a) : ∫ (x : ℝ) in Set.Iio (-t), fStar x = 2 * Real.exp (-t ^ 2 / 2) - p0

theorem OneDimConvexDom.integral_Iio_fStar_of_ge_a {t : ℝ} (hta : a ≤ t) : ∫ (x : ℝ) in Set.Iio (-t), fStar x = 0

theorem OneDimConvexDom.integral_Iio_muStar_meas_lt_eq (t : ℝ) : prob muStar (Set.Iio t) = ∫ (x : ℝ) in Set.Iio t, fStar x

theorem OneDimConvexDom.integral_Iio_fStar_of_lt_t0 {t : ℝ} (ht : t < t0) (ht0_nonneg : 0 ≤ t) : ∫ (x : ℝ) in Set.Iio (-t), fStar x = 1 - p0

theorem OneDimConvexDom.leftTail_muStar (t : ℝ) : 0 ≤ t → prob muStar {x : ℝ | x < -t} = if t < t0 then 1 - p0 else if t < OneDimConvexDom.a then 2 * Real.exp (-t ^ 2 / 2) - p0 else 0

theorem OneDimConvexDom.muStar_isProbability : MeasureTheory.IsProbabilityMeasure muStar

theorem OneDimConvexDom.z_nonneg : 0 ≤ z

theorem OneDimConvexDom.two_exp_neg_t0_sq_div_two_eq_one : 2 * Real.exp (-t0 ^ 2 / 2) = 1

theorem OneDimConvexDom.s_eq_one_of_nonneg_lt_t0 {t : ℝ} (ht0 : 0 ≤ t) (ht : t < t0) : s t = 1

theorem OneDimConvexDom.s_eq_gauss_tail_of_ge_t0 {t : ℝ} (ht : t0 ≤ t) : s t = 2 * Real.exp (-t ^ 2 / 2)

theorem OneDimConvexDom.absTail_muStar_eq_s (t : ℝ) : 0 ≤ t → absTail muStar t = s t

theorem OneDimConvexDom.stopLoss_muStar_eq_J (u : ℝ) : 0 ≤ u → stopLoss muStar u = J u

theorem OneDimConvexDom.fStar_le_two_abs_mul_exp (x : ℝ) : fStar x ≤ 2 * |x| * Real.exp (-x ^ 2 / 2)

theorem OneDimConvexDom.integrable_abs_mul_fStar : MeasureTheory.Integrable (fun (x : ℝ) => |x| * fStar x) MeasureTheory.volume

theorem OneDimConvexDom.integrable_id_muStar : MeasureTheory.Integrable (fun (x : ℝ) => x) muStar

theorem OneDimConvexDom.integral_leftTail_muStar_eq_B : ∫ (t : ℝ) in Set.Ioi 0, prob muStar {x : ℝ | x < -t} = B

theorem OneDimConvexDom.mean_muStar : mean muStar = 0

theorem OneDimConvexDom.exists_extremal_measure : ∃ (muStar : MeasureTheory.Measure ℝ), MeasureTheory.IsProbabilityMeasure muStar ∧ mean muStar = 0 ∧ (∀ (t : ℝ), 0 ≤ t → absTail muStar t = s t) ∧ ∀ (u : ℝ), 0 ≤ u → stopLoss muStar u = J u

theorem OneDimConvexDom.optimality_c0 (c : ℝ) : 0 < c → c < c0 → ∃ (muStar : MeasureTheory.Measure ℝ), MeasureTheory.IsProbabilityMeasure muStar ∧ mean muStar = 0 ∧ subgaussianTail muStar ∧ ∃ (u : ℝ), stopLoss muStar u > stopLoss (gaussianScale c) u

Main Convex-Domination Pipeline (Grouped API)

theorem OneDimConvexDom.stopLossDom_c0 {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) (htail : subgaussianTail mu) (hmean : mean mu = 0) : StopLossDom mu (gaussianScale c0)

theorem OneDimConvexDom.convexDomination_c0 {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) (htail : subgaussianTail mu) (hmean : mean mu = 0) {f : ℝ → ℝ} (hf : IsSimpleConvex f) (hmu : MeasureTheory.Integrable f mu) (hG : MeasureTheory.Integrable f (gaussianScale c0)) : ∫ (x : ℝ), f x ∂mu ≤ ∫ (x : ℝ), f x ∂gaussianScale c0

theorem OneDimConvexDom.convexDomination_c0_simple {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) (htail : subgaussianTail mu) (hmean : mean mu = 0) {f : ℝ → ℝ} (hf : IsSimpleConvex f) (hmu : MeasureTheory.Integrable f mu) (hG : MeasureTheory.Integrable f (gaussianScale c0)) : ∫ (x : ℝ), f x ∂mu ≤ ∫ (x : ℝ), f x ∂gaussianScale c0

Simple-convex endpoint at scale c0 (renamed interface).

theorem OneDimConvexDom.simpleConvex_integrable {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) {f : ℝ → ℝ} (hf : IsSimpleConvex f) : MeasureTheory.Integrable f mu

The only remaining missing ingredient for full convex domination: reduce an arbitrary convex integrand to the simple-convex case.

theorem OneDimConvexDom.gaussianScale_integrable_id (c : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => x) (gaussianScale c)

Aristotle finite max-affine proof (in-file)

def OneDimConvexDom.MaxAffineIsSimpleStatement.psi (u x : ℝ) : ℝ

In-file Aristotle proof: MaxAffineIsSimpleStatement.psi through max_affine_is_simple. Transport to this file's IsSimpleConvex/psi via the bridge theorem below.

Equations

• OneDimConvexDom.MaxAffineIsSimpleStatement.psi u x = max (x - u) 0

def OneDimConvexDom.MaxAffineIsSimpleStatement.IsSimpleConvex (f : ℝ → ℝ) : Prop

Equations

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

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.IsSimpleConvex_affine (a b : ℝ) : IsSimpleConvex fun (x : ℝ) => a * x + b

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.IsSimpleConvex_add {f g : ℝ → ℝ} (hf : IsSimpleConvex f) (hg : IsSimpleConvex g) : IsSimpleConvex (f + g)

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.max_affine_pair_is_simple (a b c d : ℝ) : IsSimpleConvex fun (x : ℝ) => max (a * x + b) (c * x + d)

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.IsSimpleConvex_add_affine {f : ℝ → ℝ} (hf : IsSimpleConvex f) (a b : ℝ) : IsSimpleConvex fun (x : ℝ) => f x + (a * x + b)

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.IsSimpleConvex_induction {P : (ℝ → ℝ) → Prop} (h_affine : ∀ (a b : ℝ), P fun (x : ℝ) => a * x + b) (h_add_hinge : ∀ (f : ℝ → ℝ) (u w : ℝ), P f → 0 ≤ w → P fun (x : ℝ) => f x + w * psi u x) (f : ℝ → ℝ) : IsSimpleConvex f → P f

def OneDimConvexDom.MaxAffineIsSimpleStatement.slope_left (a : ℝ) (s : Finset ℝ) (w : ℝ → ℝ) (x : ℝ) : ℝ

Equations

• OneDimConvexDom.MaxAffineIsSimpleStatement.slope_left a s w x = a + ∑ v ∈ s, if v < x then w v else 0

def OneDimConvexDom.MaxAffineIsSimpleStatement.slope_right (a : ℝ) (s : Finset ℝ) (w : ℝ → ℝ) (x : ℝ) : ℝ

Equations

• OneDimConvexDom.MaxAffineIsSimpleStatement.slope_right a s w x = a + ∑ v ∈ s, if v ≤ x then w v else 0

def OneDimConvexDom.MaxAffineIsSimpleStatement.glue_s (s t : Finset ℝ) (u : ℝ) : Finset ℝ

Equations

• OneDimConvexDom.MaxAffineIsSimpleStatement.glue_s s t u = {v ∈ s | v < u} ∪ {v ∈ t | v > u} ∪ {u}

def OneDimConvexDom.MaxAffineIsSimpleStatement.glue_w (s t : Finset ℝ) (w z : ℝ → ℝ) (u a c v : ℝ) : ℝ

Equations

• OneDimConvexDom.MaxAffineIsSimpleStatement.glue_w s t w z u a c v = if v < u then w v else if v > u then z v else (c + ∑ k ∈ t, if k ≤ u then z k else 0) - (a + ∑ k ∈ s, if k < u then w k else 0)

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.glue_w_nonneg (s t : Finset ℝ) (w z : ℝ → ℝ) (u a b c d : ℝ) (hw : ∀ v ∈ s, 0 ≤ w v) (hz : ∀ v ∈ t, 0 ≤ z v) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), f x = a * x + b + ∑ v ∈ s, w v * psi v x) (g : ℝ → ℝ) (hg : ∀ (x : ℝ), g x = c * x + d + ∑ v ∈ t, z v * psi v x) (h_eq : f u = g u) (h_le : ∀ x ≤ u, g x ≤ f x) (h_ge : ∀ x ≥ u, f x ≤ g x) (v : ℝ) : v ∈ glue_s s t u → 0 ≤ glue_w s t w z u a c v

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.glue_eq (s t : Finset ℝ) (w z : ℝ → ℝ) (u a b c d : ℝ) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), f x = a * x + b + ∑ v ∈ s, w v * psi v x) (g : ℝ → ℝ) (hg : ∀ (x : ℝ), g x = c * x + d + ∑ v ∈ t, z v * psi v x) (h_eq : f u = g u) (x : ℝ) : (if x ≤ u then f x else g x) = a * x + b + ∑ v ∈ glue_s s t u, glue_w s t w z u a c v * psi v x

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.IsSimpleConvex_glue (f g : ℝ → ℝ) (u : ℝ) (hf : IsSimpleConvex f) (hg : IsSimpleConvex g) (h_eq : f u = g u) (h_le : ∀ x ≤ u, g x ≤ f x) (h_ge : ∀ x ≥ u, f x ≤ g x) : IsSimpleConvex fun (x : ℝ) => if x ≤ u then f x else g x

def OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_s (s : Finset ℝ) (u v : ℝ) : Finset ℝ

Equations

• OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_s s u v = {x ∈ s | x ≤ u ∨ x ≥ v} ∪ {u, v}

def OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_w (s : Finset ℝ) (w : ℝ → ℝ) (u v x : ℝ) : ℝ

Equations

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

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_w_nonneg (s : Finset ℝ) (w : ℝ → ℝ) (u v : ℝ) (hw : ∀ x ∈ s, 0 ≤ w x) (h_uv : u < v) (x : ℝ) : x ∈ flatten_s s u v → 0 ≤ flatten_w s w u v x

def OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_w_v2 (s : Finset ℝ) (w : ℝ → ℝ) (u v x : ℝ) : ℝ

Equations

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

def OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_w_v3 (s : Finset ℝ) (w : ℝ → ℝ) (u v x : ℝ) : ℝ

Equations

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

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_w_v3_nonneg (s : Finset ℝ) (w : ℝ → ℝ) (u v : ℝ) (hw : ∀ x ∈ s, 0 ≤ w x) (h_uv : u < v) (x : ℝ) : x ∈ flatten_s s u v → 0 ≤ flatten_w_v3 s w u v x

def OneDimConvexDom.MaxAffineIsSimpleStatement.Cu (s : Finset ℝ) (w : ℝ → ℝ) (u v : ℝ) : ℝ

Equations

• OneDimConvexDom.MaxAffineIsSimpleStatement.Cu s w u v = 1 / (v - u) * ∑ k ∈ s, if u < k ∧ k < v then w k * (v - k) else 0

def OneDimConvexDom.MaxAffineIsSimpleStatement.Cv (s : Finset ℝ) (w : ℝ → ℝ) (u v : ℝ) : ℝ

Equations

• OneDimConvexDom.MaxAffineIsSimpleStatement.Cv s w u v = 1 / (v - u) * ∑ k ∈ s, if u < k ∧ k < v then w k * (k - u) else 0

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.Cu_add_Cv (s : Finset ℝ) (w : ℝ → ℝ) (u v : ℝ) (h_ne : u ≠ v) : Cu s w u v + Cv s w u v = ∑ k ∈ s, if u < k ∧ k < v then w k else 0

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.u_Cu_add_v_Cv (s : Finset ℝ) (w : ℝ → ℝ) (u v : ℝ) (h_ne : u ≠ v) : u * Cu s w u v + v * Cv s w u v = ∑ k ∈ s, if u < k ∧ k < v then w k * k else 0

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_w_v3_sum (s : Finset ℝ) (w : ℝ → ℝ) (u v : ℝ) (h_uv : u < v) : ∑ k ∈ flatten_s s u v, flatten_w_v3 s w u v k = s.sum w

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_w_v3_moment (s : Finset ℝ) (w : ℝ → ℝ) (u v : ℝ) (h_uv : u < v) : ∑ k ∈ flatten_s s u v, flatten_w_v3 s w u v k * k = ∑ k ∈ s, w k * k

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_w_v3_moment' (s : Finset ℝ) (w : ℝ → ℝ) (u v : ℝ) (h_uv : u < v) : ∑ k ∈ flatten_s s u v, flatten_w_v3 s w u v k * k = ∑ k ∈ s, w k * k

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_w_v3_moment_eq (s : Finset ℝ) (w : ℝ → ℝ) (u v : ℝ) (h_uv : u < v) : ∑ k ∈ flatten_s s u v, flatten_w_v3 s w u v k * k = ∑ k ∈ s, w k * k

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.sum_psi_eq_of_moments_eq (s1 s2 : Finset ℝ) (w1 w2 : ℝ → ℝ) (v : ℝ) (h_sum : s1.sum w1 = s2.sum w2) (h_moment : ∑ k ∈ s1, w1 k * k = ∑ k ∈ s2, w2 k * k) (h_supp : ∀ k ≥ v, (k ∈ s1 ↔ k ∈ s2) ∧ (k ∈ s1 → w1 k = w2 k)) (x : ℝ) : x ≥ v → ∑ k ∈ s1, w1 k * psi k x = ∑ k ∈ s2, w2 k * psi k x

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.sum_psi_eq_ge_v (s1 s2 : Finset ℝ) (w1 w2 : ℝ → ℝ) (v : ℝ) (h_sum : s1.sum w1 = s2.sum w2) (h_moment : ∑ k ∈ s1, w1 k * k = ∑ k ∈ s2, w2 k * k) (h_eq : ∀ k > v, (k ∈ s1 ↔ k ∈ s2) ∧ (k ∈ s1 → w1 k = w2 k)) (x : ℝ) : x ≥ v → ∑ k ∈ s1, w1 k * psi k x = ∑ k ∈ s2, w2 k * psi k x

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_eq_le_u (s : Finset ℝ) (w : ℝ → ℝ) (u v a b : ℝ) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), f x = a * x + b + ∑ k ∈ s, w k * psi k x) (h_uv : u < v) (x : ℝ) : x ≤ u → a * x + b + ∑ k ∈ flatten_s s u v, flatten_w_v3 s w u v k * psi k x = f x

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_eq_ge_v (s : Finset ℝ) (w : ℝ → ℝ) (u v a b : ℝ) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), f x = a * x + b + ∑ k ∈ s, w k * psi k x) (h_uv : u < v) (x : ℝ) : x ≥ v → a * x + b + ∑ k ∈ flatten_s s u v, flatten_w_v3 s w u v k * psi k x = f x

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.flatten_eq_ge_v' (s : Finset ℝ) (w : ℝ → ℝ) (u v a b : ℝ) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), f x = a * x + b + ∑ k ∈ s, w k * psi k x) (h_uv : u < v) (x : ℝ) : x ≥ v → a * x + b + ∑ k ∈ flatten_s s u v, flatten_w_v3 s w u v k * psi k x = f x

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.IsSimpleConvex_max_affine_simple (f : ℝ → ℝ) (hf : IsSimpleConvex f) (a b : ℝ) : IsSimpleConvex fun (x : ℝ) => max (a * x + b) (f x)

theorem OneDimConvexDom.MaxAffineIsSimpleStatement.max_affine_is_simple {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (hs : s.Nonempty) (L : ι → ℝ →L[ℝ] ℝ) (c : ι → ℝ) : IsSimpleConvex fun (x : ℝ) => s.sup' hs fun (i : ι) => (L i) x + c i

theorem OneDimConvexDom.max_affine_is_simple {ι : Type u_1} (s : Finset ι) (hs : s.Nonempty) (L : ι → ℝ →L[ℝ] ℝ) (c : ι → ℝ) : IsSimpleConvex fun (x : ℝ) => s.sup' hs fun (i : ι) => (L i) x + c i

Bridge: transport Aristotle's max_affine_is_simple to this file's IsSimpleConvex/psi.

theorem OneDimConvexDom.real_univ_sSup_of_nat_affine_le_eq {f : ℝ → ℝ} (hLsc : LowerSemicontinuous f) (hConv : ConvexOn ℝ Set.univ f) : ∃ (l : ℕ → ℝ →L[ℝ] ℝ) (c : ℕ → ℝ), (∀ (i : ℕ) (x : ℝ), (l i) x + c i ≤ f x) ∧ ⨆ (i : ℕ), ⇑(l i) + Function.const ℝ (c i) = f

theorem OneDimConvexDom.convex_simpleApprox_exists {f : ℝ → ℝ} (hfConv : ConvexOn ℝ Set.univ f) : ∃ (fn : ℕ → ℝ → ℝ), (∀ (n : ℕ), IsSimpleConvex (fn n)) ∧ (∀ (x : ℝ), Monotone fun (n : ℕ) => fn n x) ∧ ∀ (x : ℝ), Filter.Tendsto (fun (n : ℕ) => fn n x) Filter.atTop (nhds (f x))

noncomputable def OneDimConvexDom.simpleApproxSeq {f : ℝ → ℝ} (hfConv : ConvexOn ℝ Set.univ f) : ℕ → ℝ → ℝ

Equations

• OneDimConvexDom.simpleApproxSeq hfConv = Classical.choose ⋯

theorem OneDimConvexDom.simpleApproxSeq_isSimple {f : ℝ → ℝ} (hfConv : ConvexOn ℝ Set.univ f) (n : ℕ) : IsSimpleConvex (simpleApproxSeq hfConv n)

theorem OneDimConvexDom.simpleApproxSeq_mono {f : ℝ → ℝ} (hfConv : ConvexOn ℝ Set.univ f) (x : ℝ) : Monotone fun (n : ℕ) => simpleApproxSeq hfConv n x

theorem OneDimConvexDom.simpleApproxSeq_tendsto {f : ℝ → ℝ} (hfConv : ConvexOn ℝ Set.univ f) (x : ℝ) : Filter.Tendsto (fun (n : ℕ) => simpleApproxSeq hfConv n x) Filter.atTop (nhds (f x))

theorem OneDimConvexDom.simpleApproxSeq_integrable_mu {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) {f : ℝ → ℝ} (hfConv : ConvexOn ℝ Set.univ f) (n : ℕ) : MeasureTheory.Integrable (simpleApproxSeq hfConv n) mu

theorem OneDimConvexDom.simpleApproxSeq_integrable_gaussian {f : ℝ → ℝ} (hfConv : ConvexOn ℝ Set.univ f) (n : ℕ) : MeasureTheory.Integrable (simpleApproxSeq hfConv n) (gaussianScale c0)

theorem OneDimConvexDom.simpleApproxSeq_integral_le {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) {f : ℝ → ℝ} (hfConv : ConvexOn ℝ Set.univ f) (hSimpleStep : ∀ {g : ℝ → ℝ}, IsSimpleConvex g → MeasureTheory.Integrable g mu → MeasureTheory.Integrable g (gaussianScale c0) → ∫ (x : ℝ), g x ∂mu ≤ ∫ (x : ℝ), g x ∂gaussianScale c0) (n : ℕ) : ∫ (x : ℝ), simpleApproxSeq hfConv n x ∂mu ≤ ∫ (x : ℝ), simpleApproxSeq hfConv n x ∂gaussianScale c0

theorem OneDimConvexDom.convexReduction_to_simple_c0 {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) (_htail : subgaussianTail mu) (_hmean : mean mu = 0) {f : ℝ → ℝ} (hfConv : ConvexOn ℝ Set.univ f) (hmu : MeasureTheory.Integrable f mu) (hG : MeasureTheory.Integrable f (gaussianScale c0)) (hSimpleStep : ∀ {g : ℝ → ℝ}, IsSimpleConvex g → MeasureTheory.Integrable g mu → MeasureTheory.Integrable g (gaussianScale c0) → ∫ (x : ℝ), g x ∂mu ≤ ∫ (x : ℝ), g x ∂gaussianScale c0) : ∫ (x : ℝ), f x ∂mu ≤ ∫ (x : ℝ), f x ∂gaussianScale c0

theorem OneDimConvexDom.convexDomination_c0_via_reduction {mu : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure mu] (hIntMuId : MeasureTheory.Integrable (fun (x : ℝ) => x) mu) (htail : subgaussianTail mu) (hmean : mean mu = 0) {f : ℝ → ℝ} (hfConv : ConvexOn ℝ Set.univ f) (hmu : MeasureTheory.Integrable f mu) (hG : MeasureTheory.Integrable f (gaussianScale c0)) : ∫ (x : ℝ), f x ∂mu ≤ ∫ (x : ℝ), f x ∂gaussianScale c0

Two-step interface theorem:

1. reduce convex f to simple-convex test functions,
2. invoke the already-proved c0 simple-convex bound.