TwoTermPromotion #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Promotion of a one-sided Orlicz bound to the two-term shape #
Model-free: a one-sided Gamma_{sigma_1} bound gives the two-term shape at any
larger first amplitude and any positive second amplitude, by taking the second
witness identically 0.
theorem
Algsuperdiff.Section3.Provider.Orlicz.isTwoTermBigOWith_of_isOneSidedOrlicz
{Omega : Type u_1}
[MeasurableSpace Omega]
{mu : MeasureTheory.Measure Omega}
[MeasureTheory.IsFiniteMeasure mu]
{X : Omega → ℝ}
{A A1 A2 s1 s2 : ℝ}
(hs1 : 0 < s1)
(hs2 : 0 < s2)
(hX : Probability.IsOneSidedOrlicz mu (HCPolySupport.IndependentSums.gammaSigma s1) X A)
(hA1 : A ≤ A1)
(hA1pos : 0 < A1)
(hA2 : 0 < A2)
:
A one-sided Gamma_{sigma_1} bound gives the two-term shape used by
inductionState, at any larger first amplitude and any positive second
amplitude: take the second witness identically 0, whose upper tail event is
empty at every threshold t >= 1.