OneSidedOrlicz

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

One-sided weak-Orlicz relations

The ABK26 Appendix uses one-sided weak-Orlicz bounds for random variables, with measurable witnesses in its additive notation. This file records the literal one-term relation and its deterministic-shift A. The canonical two-term relation is IsTwoTermBigOWith from TwoTermOrlicz; it is reused here rather than duplicated. CoarseGraining's tail-event predicate does not itself carry measurability, so the source's random-variable requirement is stated explicitly here.

References

• ABK26.
• ABK26, the main-text uses of the one-sided bound.

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

The Appendix-literal source notation X ≤ O_Ψ(A): X is a measurable random variable with the stated one-sided upper tail at the positive scale A.

Equations

• Algsuperdiff.Section3.Probability.IsOneSidedOrlicz μ Ψ X A = (Algsuperdiff.Section3.Probability.IsAdmissibleTail Ψ ∧ 0 < A ∧ Measurable X ∧ HCPolySupport.IndependentSums.IsBigOWith μ Ψ X A)

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

The source notation X ≤ b + O_Ψ(A) for a deterministic shift b.

Equations

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

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

The source notation X ≤ b + O_{Ψ₁}(A₁) + O_{Ψ₂}(A₂) for a deterministic shift b.

Equations

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

theorem Algsuperdiff.Section3.Probability.deterministicShiftTwoTermOneSidedOrlicz_iff_exists {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ψ₁ Ψ₂ : ℝ → ℝ} {X : Ω → ℝ} {b A₁ A₂ : ℝ} : IsDeterministicShiftTwoTermOneSidedOrlicz μ Ψ₁ Ψ₂ X b A₁ A₂ ↔ ∃ (Y : Ω → ℝ) (Z : Ω → ℝ), IsAdmissibleTail Ψ₁ ∧ IsAdmissibleTail Ψ₂ ∧ 0 < A₁ ∧ 0 < A₂ ∧ Measurable X ∧ Measurable Y ∧ Measurable Z ∧ (∀ (ω : Ω), X ω ≤ b + Y ω + Z ω) ∧ HCPolySupport.IndependentSums.IsBigOWith μ Ψ₁ Y A₁ ∧ HCPolySupport.IndependentSums.IsBigOWith μ Ψ₂ Z A₂

theorem Algsuperdiff.Section3.Probability.isBigOWith_max_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ψ : ℝ → ℝ} {Y : Ω → ℝ} {A : ℝ} (hA : 0 < A) (hY : HCPolySupport.IndependentSums.IsBigOWith μ Ψ Y A) : HCPolySupport.IndependentSums.IsBigOWith μ Ψ (fun (ω : Ω) => max 0 (Y ω)) A

Clamping a witness below at zero preserves its one-sided tail at every positive scale, without requiring measurability or a finite measure.

theorem Algsuperdiff.Section3.Probability.isBigOWith_gammaSigma_of_eq_zero {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {X : Omega → ℝ} {sigma A : ℝ} (hA : 0 ≤ A) (hX : ∀ (omega : Omega), X omega = 0) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) X A

A pointwise zero observable has every nonnegative Gamma scale. The tail event is empty, so measurability and measure finiteness are unnecessary.