TwoTermOrlicz

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

Two-term weak-Orlicz bounds

This module formalizes the one-sided two-term weak-Orlicz notation of the ABK26 Appendix. It records the source admissibility conditions on tail functions, measurable witness random variables, and a pointwise decomposition, without replacing the paper's one-sided tails by symmetric ones.

Main definitions

• Algsuperdiff.Section3.Probability.IsTwoTermBigOWithWitnesses: a fixed measurable witness pair for a two-term weak-Orlicz bound.
• Algsuperdiff.Section3.Probability.IsTwoTermBigOWith: the assertion X ≤ O_{Ψ₁}(A₁) + O_{Ψ₂}(A₂).
• Algsuperdiff.Section3.Probability.IsAdmissibleTail: the Appendix conditions on a tail function.

References

• ABK26, Appendix.

def Algsuperdiff.Section3.Probability.IsAdmissibleTail (Ψ : ℝ → ℝ) : Prop

The admissibility conditions imposed on a tail function in the ABK26 Appendix: it is increasing on the nonnegative reals, takes values at least one there, and its reciprocal has the stated weighted integrability.

Equations

• Algsuperdiff.Section3.Probability.IsAdmissibleTail Ψ = (HCPolySupport.IndependentSums.AdmissiblePsi Ψ ∧ MeasureTheory.IntegrableOn (fun (t : ℝ) => t / Ψ t) (Set.Ici 1) MeasureTheory.volume)

theorem Algsuperdiff.Section3.Probability.isAdmissibleTail_gammaSigma {σ : ℝ} (hσ : 0 < σ) : IsAdmissibleTail (HCPolySupport.IndependentSums.gammaSigma σ)

The stretched-exponential tail function satisfies the Appendix admissibility conditions whenever its exponent is positive.

def Algsuperdiff.Section3.Probability.IsTwoTermBigOWithWitnesses {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Ψ₁ Ψ₂ : ℝ → ℝ) (X Y Z : Ω → ℝ) (A₁ A₂ : ℝ) : Prop

A fixed witness pair for the one-sided two-term weak-Orlicz relation.

The tail functions are Appendix-admissible, the scales are positive, all three random variables are measurable, X is pointwise bounded above by Y + Z, and the two witnesses satisfy their respective one-sided weak-Orlicz tails.

Equations

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

def Algsuperdiff.Section3.Probability.IsTwoTermBigOWith {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Ψ₁ Ψ₂ : ℝ → ℝ) (X : Ω → ℝ) (A₁ A₂ : ℝ) : Prop

The one-sided two-term weak-Orlicz relation of the ABK26 Appendix.

IsTwoTermBigOWith μ Ψ₁ Ψ₂ X A₁ A₂ means that the positive scales A₁ and A₂ control measurable witnesses Y and Z, respectively, and that X is pointwise bounded above by their sum. Each witness has the source's one-sided weak-Orlicz tail, implemented by IndependentSums.IsBigOWith.

Equations

• Algsuperdiff.Section3.Probability.IsTwoTermBigOWith μ Ψ₁ Ψ₂ X A₁ A₂ = ∃ (Y : Ω → ℝ) (Z : Ω → ℝ), Algsuperdiff.Section3.Probability.IsTwoTermBigOWithWitnesses μ Ψ₁ Ψ₂ X Y Z A₁ A₂