TsumTriangle

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

Countable generalized triangle inequality for stretched-exponential tails

This module upgrades the finite-family weak-Orlicz triangle inequality of CoarseGraining to a countable family, which is the form used by the ABK26 Appendix.

CoarseGraining proves the finite-family estimate Homogenization.IndependentSums.isBigO_finset_sum_of_isBigO_gammaSigma with the explicit constant gammaTriangleConst σ. The countable statement is obtained by continuity from below: for a nonnegative family the partial-sum upper-tail events increase to the upper-tail event of the series, and each of them is controlled at the common scale gammaTriangleConst σ * ∑' k, a k.

Main results

• Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_iff_isBigO_of_nonneg: for a pointwise nonnegative random variable the one-sided and symmetric weak-Orlicz relations coincide.
• Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_tsum_of_isBigOWith_sum_range_succ: continuity from below for a general tail function Ψ.
• Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_tsum: the countable triangle inequality for Γ_σ.
• Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_tsum_of_tsum_le: the same estimate stated against an arbitrary majorant of ∑' k, a k.

References

• ABK26, Lemma l.Gamma.sigma.triangle.
• ABK26, Appendix.

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_iff_isBigO_of_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ψ : ℝ → ℝ} {Y : Ω → ℝ} {A : ℝ} (hY : ∀ (ω : Ω), 0 ≤ Y ω) : HCPolySupport.IndependentSums.IsBigOWith μ Ψ Y A ↔ HCPolySupport.IndependentSums.IsBigO μ Ψ Y A

For a pointwise nonnegative random variable the one-sided weak-Orlicz relation X ≤ O_Ψ(A) and the symmetric relation X = O_Ψ(A) agree, because |X| = X.

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_tsum_of_isBigOWith_sum_range_succ {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X : ℕ → Ω → ℝ} {A : ℝ} (hX_nonneg : ∀ (k : ℕ) (ω : Ω), 0 ≤ X k ω) (hsum : ∀ (N : ℕ), HCPolySupport.IndependentSums.IsBigOWith μ Ψ (fun (ω : Ω) => ∑ k ∈ Finset.range (N + 1), X k ω) A) : HCPolySupport.IndependentSums.IsBigOWith μ Ψ (fun (ω : Ω) => ∑' (k : ℕ), X k ω) A

Continuity from below for weak-Orlicz upper tails of a nonnegative series.

If every partial sum ∑_{k < N+1} X k obeys the same one-sided bound at scale A, then so does the series ∑' k, X k. Only the partial sums over the nonempty ranges are required, which is what the finite triangle inequality supplies.

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_tsum {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → ℝ} {a : ℕ → ℝ} {σ : ℝ} (hσ : 0 < σ) (hX_nonneg : ∀ (k : ℕ) (ω : Ω), 0 ≤ X k ω) (hX_meas : ∀ (k : ℕ), Measurable (X k)) (ha : ∀ (k : ℕ), 0 < a k) (ha_summable : Summable a) (hX : ∀ (k : ℕ), HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (X k) (a k)) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => ∑' (k : ℕ), X k ω) (HCPolySupport.IndependentSums.gammaTriangleConst σ * ∑' (k : ℕ), a k)

Generalized triangle inequality for a countable family of nonnegative random variables with stretched-exponential upper tails.

This is the ABK26 statement l.Gamma.sigma.triangle with CoarseGraining's explicit constant gammaTriangleConst σ in place of the source's 1 + C σ^{-1/σ} 1_{σ < 1}.

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_tsum_of_tsum_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → ℝ} {a : ℕ → ℝ} {σ B : ℝ} (hσ : 0 < σ) (hX_nonneg : ∀ (k : ℕ) (ω : Ω), 0 ≤ X k ω) (hX_meas : ∀ (k : ℕ), Measurable (X k)) (ha : ∀ (k : ℕ), 0 < a k) (ha_summable : Summable a) (hX : ∀ (k : ℕ), HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (X k) (a k)) (hB : ∑' (k : ℕ), a k ≤ B) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => ∑' (k : ℕ), X k ω) (HCPolySupport.IndependentSums.gammaTriangleConst σ * B)

The countable triangle inequality stated against an arbitrary majorant B of the scale series, which is the form used at ABK26 call sites.

A.e.-measurable summands

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_tsum_aemeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → ℝ} {a : ℕ → ℝ} {σ : ℝ} (hσ : 0 < σ) (hX_nonneg : ∀ (k : ℕ) (ω : Ω), 0 ≤ X k ω) (hX_meas : ∀ (k : ℕ), AEMeasurable (X k) μ) (ha : ∀ (k : ℕ), 0 < a k) (ha_summable : Summable a) (hX : ∀ (k : ℕ), HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (X k) (a k)) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => ∑' (k : ℕ), X k ω) (HCPolySupport.IndependentSums.gammaTriangleConst σ * ∑' (k : ℕ), a k)

Countable Gamma_sigma triangle inequality for nonnegative summands that are only a.e.-measurable. This is the countable extension of CoarseGraining's finite isBigO_finset_sum_of_isBigO_gammaSigma_aemeasurable; it introduces no measurable-representative premise at the call site.