PrincipalResponseBudgetMoment

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.

Provider: the second moment of a one-sided two-term weak-Orlicz bound

This module supplies the single probabilistic step of the budget delta <=^2 |log gamma|^2 gamma of ABK26, inside the proof of e.use.also.for.the.upper.bound: the passage from the tail form of the induction hypothesis e.new.induction.for.shom (d.mathcalS.def) to a second moment.

  ... <= C 3^{t(m-h-n)} E[ mathcalE_{t,infinity,2}(cu_{m-h}; a_{m-h}, shom_{m-h})^2 ]
      <= C E^2 |log gamma|^2 gamma ,

and the last inequality is the only place where the induction state enters. The induction state is stated as the one-sided two-term weak-Orlicz relation

  mathcalE_{s,infinity,2}(cu_m; a_m, shom_m)
    <=  O_{Gamma_2}( E s^{-1} gamma^{1/2} )
      + O_{Gamma_{1/2}}( s^{-2} exp(-E^{-3} gamma^{-1}) ) ,

i.e. Algsuperdiff.Section3.Probability.IsTwoTermBigOWith at the two stretched-exponential tail functions Gamma_2 and Gamma_{1/2}. What is proved below is the general fact that such a relation for a nonnegative random variable controls its second moment by the two scales:

  E[X^2]  <=  c(sigma_1) A_1^2 + c(sigma_2) A_2^2 ,

with c(sigma) the explicit absolute constant orliczSecondMomentConst.

How the two witnesses are handled

IsTwoTermBigOWith supplies measurable witnesses Y, Z with X <= Y + Z pointwise and a one-sided tail for each. The witnesses are not assumed nonnegative, so the layer-cake moment bound of CoarseGraining's Homogenization.Probability.IndependentSums.GammaSigma.Basic (integral_rpow_le_of_isBigOWith_gammaSigma) is applied to their positive parts max(Y,0), max(Z,0), which carry the same one-sided upper tails because the tail threshold A t is positive for t >= 1 and A > 0. Since 0 <= X <= max(Y,0) + max(Z,0), the elementary inequality (u+v)^2 <= 2u^2 + 2v^2 finishes. No symmetrization and no lower tail is used, matching the one-sided source notation.

Scope

Nothing here mentions the manuscript's cube, probe, defect, or scales: the statements are about an arbitrary nonnegative random variable on a probability space. In particular no source node is claimed, and neither the value t = |log gamma|^{-1} nor the window s in [8 gamma, 1] of d.mathcalS.def appears.

Main results

• orliczSecondMomentConst: the explicit absolute second-moment constant of the stretched-exponential class Gamma_sigma, and its positivity.
• integrable_sq_of_isTwoTermBigOWith_gammaSigma: square integrability.
• integral_sq_le_of_isTwoTermBigOWith_gammaSigma: the second moment bound.

References

• ABK26, d.mathcalS.def, e.new.induction.for.shom.
• ABK26 (the budget of e.use.also.for.the.upper.bound).
• ABK26, Appendix (the weak-Orlicz notation).

Positive parts and the layer-cake moment at p = 2

The second-moment constant

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.orliczSecondMomentConst (sigma : ℝ) : ℝ

The explicit absolute second-moment constant of the stretched-exponential class Gamma_sigma: an O_{Gamma_sigma}(A) variable has second moment at most orliczSecondMomentConst sigma * A^2 after the factor 2 of the elementary inequality (u+v)^2 <= 2u^2 + 2v^2 is absorbed. It depends on nothing but sigma.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.orliczSecondMomentConst sigma = 2 * (HCPolySupport.IndependentSums.gammaMomentConst sigma * 2 ^ sigma⁻¹) ^ 2

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.orliczSecondMomentConst_pos {sigma : ℝ} (hsigma : 0 < sigma) : 0 < orliczSecondMomentConst sigma

The second moment of a two-term weak-Orlicz bound

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrable_sq_of_isTwoTermBigOWith_gammaSigma {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : Omega → ℝ} {A1 A2 sig1 sig2 : ℝ} (hsig1 : 0 < sig1) (hsig2 : 0 < sig2) (hXnonneg : ∀ (omega : Omega), 0 ≤ X omega) (h : Probability.IsTwoTermBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sig1) (HCPolySupport.IndependentSums.gammaSigma sig2) X A1 A2) : MeasureTheory.Integrable (fun (omega : Omega) => X omega ^ 2) mu

A nonnegative random variable obeying the one-sided two-term weak-Orlicz relation of d.mathcalS.def at two stretched-exponential classes is square integrable.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_sq_le_of_isTwoTermBigOWith_gammaSigma {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : Omega → ℝ} {A1 A2 sig1 sig2 : ℝ} (hsig1 : 0 < sig1) (hsig2 : 0 < sig2) (hXnonneg : ∀ (omega : Omega), 0 ≤ X omega) (h : Probability.IsTwoTermBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sig1) (HCPolySupport.IndependentSums.gammaSigma sig2) X A1 A2) : ∫ (omega : Omega), X omega ^ 2 ∂mu ≤ orliczSecondMomentConst sig1 * A1 ^ 2 + orliczSecondMomentConst sig2 * A2 ^ 2

The Orlicz-to-moment step of ABK26.

A nonnegative random variable satisfying X <= O_{Gamma_{sig1}}(A_1) + O_{Gamma_{sig2}}(A_2) in the one-sided sense of the ABK26 Appendix has second moment at most c(sig1) A_1^2 + c(sig2) A_2^2, with c = orliczSecondMomentConst an explicit absolute constant.

Applied to X = mathcalE_{s,infinity,2}(cu_m; a_m, shom_m) with the two scales of e.new.induction.for.shom, this is the only consumption of the induction state in the budget of e.use.also.for.the.upper.bound. No cube, probe or scale of the manuscript appears here.