Orlicz-to-tail concentration bridges

This file contains the first implication proofs from the Orlicz layer to the tail layer. The proofs use Mathlib's lintegral Markov inequality directly: the Orlicz predicates are already stated as nonnegative lintegral bounds.

Verified Wikipedia references:

• Orlicz space: https://en.wikipedia.org/wiki/Orlicz_space
• Markov's inequality: https://en.wikipedia.org/wiki/Markov%27s_inequality

theorem HighDimProb.lintegral_exp_sq_div_le_two_of_psi2Bound {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RealRandomVariable Ω} {K : ℝ} (hψ : Psi2Bound P X K) : ∫⁻ (ω : Ω), ENNReal.ofReal (Real.exp ((|X ω| / K) ^ 2)) ∂P ≤ 2

A Psi2Bound gives the exponential-square moment bound with constant 2.

The probability assumption is necessary: Psi2Bound alone does not control the mass of the underlying measure when the Orlicz integrand vanishes.

Formula reference: the psi_2 Orlicz integrand is exp ((|X| / K)^2) - 1; adding the probability mass gives the bound for exp ((|X| / K)^2). See https://en.wikipedia.org/wiki/Orlicz_space

theorem HighDimProb.lintegral_exp_abs_div_le_two_of_psi1Bound {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RealRandomVariable Ω} {K : ℝ} (hψ : Psi1Bound P X K) : ∫⁻ (ω : Ω), ENNReal.ofReal (Real.exp (|X ω| / K)) ∂P ≤ 2

A Psi1Bound gives the exponential-linear moment bound with constant 2.

The probability assumption is necessary for the same reason as in the psi_2 case: the Orlicz bound controls only the shifted exponential integrand.

Formula reference: the psi_1 Orlicz integrand is exp (|X| / K) - 1; adding the probability mass gives the bound for exp (|X| / K). See https://en.wikipedia.org/wiki/Orlicz_space

theorem HighDimProb.subGaussianTail_of_psi2Bound {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RealRandomVariable Ω} {K : ℝ} (hX : IsRealRandomVariable P X) (hψ : Psi2Bound P X K) : SubGaussianTail P X K

The psi_2 Orlicz bound implies the HighDimProb two-sided subGaussian tail bound with the same scale.

Measurability is kept separate because Psi2Bound is an integral bound predicate, not a random-variable predicate.

Formula reference: applying Markov's inequality to exp ((|X| / K)^2) yields a two-sided psi_2 tail 2 * exp (-(t^2 / K^2)); see https://en.wikipedia.org/wiki/Markov%27s_inequality and https://en.wikipedia.org/wiki/Orlicz_space

theorem HighDimProb.subExponentialTail_of_psi1Bound {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RealRandomVariable Ω} {K : ℝ} (hX : IsRealRandomVariable P X) (hψ : Psi1Bound P X K) : SubExponentialTail P X K

The psi_1 Orlicz bound implies the HighDimProb two-sided subExponential tail bound with the same scale.

Measurability is kept separate for the same reason as in subGaussianTail_of_psi2Bound.

Formula reference: applying Markov's inequality to exp (|X| / K) yields the two-sided psi_1 tail 2 * exp (-(t / K)); see https://en.wikipedia.org/wiki/Markov%27s_inequality and https://en.wikipedia.org/wiki/Orlicz_space