Maximum

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

Maxima of stretched-exponential random variables over any nonempty family

CoarseGraining's finite-maximum estimate Homogenization.IndependentSums.isBigOWith_gammaSigma_finset_sup' carries the hypothesis 2 ≤ s.card, matching the source proof, which uses 2 log N ≥ 1. The ABK26 call sites also instantiate the estimate at singletons, where log 1 = 0 degenerates the amplitude.

This module removes the cardinality restriction by replacing log N with max 1 (log N). For 2 ≤ N this only enlarges the amplitude, and for N = 1 the supremum is a single member of the family and the amplitude factor is 3^{1/σ} ≥ 1. Both cases then follow by amplitude monotonicity, Homogenization.IndependentSums.IsBigOWith.mono_scale.

Main results

• Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_finset_sup'_of_nonempty
• Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_finset_sup'_of_scales_of_nonempty

References

• ABK26, Lemma l.maximums.Gamma.s.
• ABK26, Appendix.

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_finset_sup'_of_nonempty {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (s : Finset ι) (hs : s.Nonempty) {X : ι → Ω → ℝ} {A σ : ℝ} (hσ : 0 < σ) (hA : 0 ≤ A) (hX : ∀ i ∈ s, HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (X i) A) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => s.sup' hs fun (i : ι) => X i ω) ((3 * max 1 (Real.log ↑s.card)) ^ σ⁻¹ * A)

Maximum of a nonempty finite family of Γ_σ random variables at a common scale A, with no restriction on the cardinality.

The amplitude uses max 1 (log card) rather than the source's log card; the two agree up to an enlargement for 2 ≤ card, and the max is what makes the singleton case nondegenerate.

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_finset_sup'_of_scales_of_nonempty {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (s : Finset ι) (hs : s.Nonempty) {X : ι → Ω → ℝ} {a : ι → ℝ} {σ : ℝ} (hσ : 0 < σ) (ha : ∀ i ∈ s, 0 ≤ a i) (hX : ∀ i ∈ s, HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (X i) (a i)) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => s.sup' hs fun (i : ι) => X i ω) ((3 * max 1 (Real.log ↑s.card)) ^ σ⁻¹ * s.sup' hs a)

Maximum of a nonempty finite family of Γ_σ random variables with individual scales, controlled by the largest scale.