Coarse-graining support: Support.Probability.IndependentSums.Triangle

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Finite-sum reduction lemmas for the Chapter 4 weak-Orlicz triangle inequality.

This file formalizes the deterministic truncation step and the finite-family Markov reduction from Step 5 of the notes. The one-variable tail integral bound will plug into these lemmas downstream.

noncomputable def HCPolySupport.IndependentSums.upperTailIndicator {Ω : Type u_1} (X : Ω → ℝ) (r : ℝ) : Ω → ℝ

The truncated upper-tail variable X 1_{X > r} used in the Step 5 proof of the generalized triangle inequality.

Equations

• HCPolySupport.IndependentSums.upperTailIndicator X r = (HCPolySupport.IndependentSums.upperTailEvent X r).indicator X

@[simp]

theorem HCPolySupport.IndependentSums.upperTailIndicator_apply {Ω : Type u_1} (X : Ω → ℝ) (r : ℝ) (ω : Ω) : upperTailIndicator X r ω = if r < X ω then X ω else 0

theorem HCPolySupport.IndependentSums.upperTailIndicator_of_lt {Ω : Type u_1} {X : Ω → ℝ} {r : ℝ} {ω : Ω} (h : r < X ω) : upperTailIndicator X r ω = X ω

theorem HCPolySupport.IndependentSums.upperTailIndicator_of_not_lt {Ω : Type u_1} {X : Ω → ℝ} {r : ℝ} {ω : Ω} (h : ¬r < X ω) : upperTailIndicator X r ω = 0

theorem HCPolySupport.IndependentSums.upperTailIndicator_nonneg {Ω : Type u_1} {X : Ω → ℝ} {r : ℝ} (hr : 0 ≤ r) (ω : Ω) : 0 ≤ upperTailIndicator X r ω

theorem HCPolySupport.IndependentSums.le_upperTailIndicator_add {Ω : Type u_1} {X : Ω → ℝ} {r : ℝ} (hr : 0 ≤ r) (ω : Ω) : X ω ≤ upperTailIndicator X r ω + r

theorem HCPolySupport.IndependentSums.sum_le_sum_upperTailIndicator_add_sum {Ω : Type u_1} {ι : Type u_2} (s : Finset ι) {X : ι → Ω → ℝ} {r : ι → ℝ} (hr : ∀ i ∈ s, 0 ≤ r i) (ω : Ω) : ∑ i ∈ s, X i ω ≤ ∑ i ∈ s, upperTailIndicator (X i) (r i) ω + s.sum r

theorem HCPolySupport.IndependentSums.upperTailEvent_finset_sum_subset_upperTailIndicator_finset_sum {Ω : Type u_1} {ι : Type u_2} (s : Finset ι) {X : ι → Ω → ℝ} {r : ι → ℝ} {b : ℝ} (hr : ∀ i ∈ s, 0 ≤ r i) : upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) (b + s.sum r) ⊆ upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, upperTailIndicator (X i) (r i) ω) b

If a finite sum exceeds b + Σ rᵢ, then the sum of the corresponding upper-tail truncations exceeds b.

theorem HCPolySupport.IndependentSums.absTailEvent_finset_sum_subset_upperTailEvent_sum_abs {Ω : Type u_1} {ι : Type u_2} (s : Finset ι) {X : ι → Ω → ℝ} {b : ℝ} : absTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) b ⊆ upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, |X i ω|) b

The absolute tail of a finite sum is controlled by the one-sided tail of the sum of the absolute values.

theorem HCPolySupport.IndependentSums.upperTailEvent_upperTailIndicator_eq_upperTailEvent_left {Ω : Type u_1} {X : Ω → ℝ} {c s : ℝ} (hs : 0 < s) (hsc : s ≤ c) : upperTailEvent (upperTailIndicator X c) s = upperTailEvent X c

theorem HCPolySupport.IndependentSums.upperTailEvent_upperTailIndicator_eq_upperTailEvent_right {Ω : Type u_1} {X : Ω → ℝ} {c s : ℝ} (hc : 0 ≤ c) (hcs : c ≤ s) : upperTailEvent (upperTailIndicator X c) s = upperTailEvent X s

theorem HCPolySupport.IndependentSums.upperTailIndicator_measurable {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {r : ℝ} (hX : Measurable X) : Measurable (upperTailIndicator X r)

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_upperTailIndicator_eq_upperTailEvent_left {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c s : ℝ} (hs : 0 < s) (hsc : s ≤ c) : μ.real (upperTailEvent (upperTailIndicator X c) s) = μ.real (upperTailEvent X c)

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_upperTailIndicator_eq_upperTailEvent_right {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c s : ℝ} (hc : 0 ≤ c) (hcs : c ≤ s) : μ.real (upperTailEvent (upperTailIndicator X c) s) = μ.real (upperTailEvent X s)

theorem HCPolySupport.IndependentSums.lintegral_upperTailIndicator_le_of_isBigOWith {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {a q C₀ t : ℝ} (hD : HasPsiAbstractDoubling Ψ q C₀) (hAdmissible : AdmissiblePsi Ψ) (hq : 1 < q) (ha : 0 < a) (ht : 1 ≤ t) (hX : IsBigOWith μ Ψ X a) (hXm : Measurable X) : ∫⁻ (ω : Ω), ENNReal.ofReal (upperTailIndicator X (a * t) ω) ∂μ ≤ ENNReal.ofReal (a * t * (1 + C₀ / (q - 1)) * (Ψ t)⁻¹)

theorem HCPolySupport.IndependentSums.integrable_upperTailIndicator_of_isBigOWith {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {a q C₀ t : ℝ} (hD : HasPsiAbstractDoubling Ψ q C₀) (hAdmissible : AdmissiblePsi Ψ) (hq : 1 < q) (ha : 0 < a) (ht : 1 ≤ t) (hX : IsBigOWith μ Ψ X a) (hXm : Measurable X) : MeasureTheory.Integrable (upperTailIndicator X (a * t)) μ

theorem HCPolySupport.IndependentSums.integral_upperTailIndicator_le_of_isBigOWith {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {a q C₀ t : ℝ} (hD : HasPsiAbstractDoubling Ψ q C₀) (hAdmissible : AdmissiblePsi Ψ) (hq : 1 < q) (ha : 0 < a) (ht : 1 ≤ t) (hX : IsBigOWith μ Ψ X a) (hXm : Measurable X) : ∫ (ω : Ω), upperTailIndicator X (a * t) ω ∂μ ≤ a * t * (1 + C₀ / (q - 1)) * (Ψ t)⁻¹

theorem HCPolySupport.IndependentSums.mul_measureReal_upperTailEvent_finset_sum_le_integral_finset_sum {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {Y : ι → Ω → ℝ} {b : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hb : 0 ≤ b) (hY_nonneg : ∀ i ∈ s, ∀ (ω : Ω), 0 ≤ Y i ω) (hY_int : ∀ i ∈ s, MeasureTheory.Integrable (Y i) μ) : b * μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, Y i ω) b) ≤ ∑ i ∈ s, ∫ (ω : Ω), Y i ω ∂μ

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_finset_sum_le_div {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {Y : ι → Ω → ℝ} {b : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hb : 0 < b) (hY_nonneg : ∀ i ∈ s, ∀ (ω : Ω), 0 ≤ Y i ω) (hY_int : ∀ i ∈ s, MeasureTheory.Integrable (Y i) μ) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, Y i ω) b) ≤ (∑ i ∈ s, ∫ (ω : Ω), Y i ω ∂μ) / b

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_finset_sum_le_div_of_upperTailIndicator {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {r : ι → ℝ} {b : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hr : ∀ i ∈ s, 0 ≤ r i) (hb : 0 < b) (hInt : ∀ i ∈ s, MeasureTheory.Integrable (upperTailIndicator (X i) (r i)) μ) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) (b + s.sum r)) ≤ (∑ i ∈ s, ∫ (ω : Ω), upperTailIndicator (X i) (r i) ω ∂μ) / b

The finite-sum Step 5 reduction: after truncating each variable at level rᵢ, the upper tail of the original sum is controlled by Markov's inequality applied to the truncated sum.

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_finset_sum_le_of_isBigOWith {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {Ψ : ℝ → ℝ} {q C₀ t : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hD : HasPsiAbstractDoubling Ψ q C₀) (hAdmissible : AdmissiblePsi Ψ) (hq : 1 < q) (hs : s.Nonempty) (ht : 2 ≤ t) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigOWith μ Ψ (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) (s.sum a * t)) ≤ (1 + C₀ / (q - 1)) * (Ψ (t / 2))⁻¹

Step 5 pre-triangle estimate in weak-Orlicz form: after truncating each variable at level aᵢ * (t / 2), the finite-sum Markov reduction and the one-variable truncation bound combine into the tail estimate at scale (∑ aᵢ) * t.

theorem HCPolySupport.IndependentSums.measureReal_absTailEvent_finset_sum_le_of_isBigO {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {Ψ : ℝ → ℝ} {q C₀ t : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hD : HasPsiAbstractDoubling Ψ q C₀) (hAdmissible : AdmissiblePsi Ψ) (hq : 1 < q) (hs : s.Nonempty) (ht : 2 ≤ t) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ Ψ (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) : μ.real (absTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) (s.sum a * t)) ≤ (1 + C₀ / (q - 1)) * (Ψ (t / 2))⁻¹

The symmetric Step 5 estimate used for the weak-Orlicz triangle inequality: control the absolute tail of a finite sum from IsBigO data on the summands.

noncomputable def HCPolySupport.IndependentSums.psiTriangleConst (q C₀ : ℝ) : ℝ

The explicit Chapter 4 dilation constant produced by the abstract doubling-based triangle inequality.

Equations

• HCPolySupport.IndependentSums.psiTriangleConst q C₀ = 2 * (C₀ * (1 + C₀ / (q - 1))) ^ (1 / q)

theorem HCPolySupport.IndependentSums.psiTriangleConst_two_le_four_mul {C : ℝ} (hC : 1 ≤ C) : psiTriangleConst 2 C ≤ 4 * C

theorem HCPolySupport.IndependentSums.prefactor_mul_inv_le_inv_of_hasPsiAbstractDoubling {Ψ : ℝ → ℝ} {q C₀ B σ t : ℝ} (hD : HasPsiAbstractDoubling Ψ q C₀) (hAdmissible : AdmissiblePsi Ψ) (ht : 1 ≤ t) (hσ : 1 ≤ σ) (hB_nonneg : 0 ≤ B) (hfac : B * (C₀ * σ ^ (-q)) ≤ 1) : B * (Ψ (σ * t))⁻¹ ≤ (Ψ t)⁻¹

A prefactor in front of an inverse Ψ tail can be absorbed into a dilation witness σ, provided the abstract doubling estimate makes the factor small enough.

theorem HCPolySupport.IndependentSums.isBigO_finset_sum_of_hasPsiAbstractDoubling {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {Ψ : ℝ → ℝ} {q C₀ σ : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hD : HasPsiAbstractDoubling Ψ q C₀) (hAdmissible : AdmissiblePsi Ψ) (hq : 1 < q) (hs : s.Nonempty) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ Ψ (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) (hσ : 1 ≤ σ) (hσ_small : (1 + C₀ / (q - 1)) * (C₀ * σ ^ (-q)) ≤ 1) : IsBigO μ Ψ (fun (ω : Ω) => ∑ i ∈ s, X i ω) (2 * σ * s.sum a)

The finite-family weak-Orlicz triangle inequality with an explicit dilation witness σ. The witness is carried as data rather than hidden inside the scale, so later model-specific choices of σ can be formalized independently.

theorem HCPolySupport.IndependentSums.isBigO_finset_sum_of_isBigO {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {Ψ : ℝ → ℝ} {q C₀ : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hD : HasPsiAbstractDoubling Ψ q C₀) (hAdmissible : AdmissiblePsi Ψ) (hq : 1 < q) (hs : s.Nonempty) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ Ψ (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) : IsBigO μ Ψ (fun (ω : Ω) => ∑ i ∈ s, X i ω) (psiTriangleConst q C₀ * s.sum a)

The first finished finite-family weak-Orlicz triangle theorem. The scale constant is expressed explicitly in terms of the abstract doubling data, while the witness-based theorem above remains available for later refinements.

theorem HCPolySupport.IndependentSums.isBigO_finset_sum_of_isBigO_growth {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {Ψ : ℝ → ℝ} {K : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hK : 2 ≤ K) (hGrowth : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (hs : s.Nonempty) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ Ψ (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) : IsBigO μ Ψ (fun (ω : Ω) => ∑ i ∈ s, X i ω) (psiTriangleConst 2 (K ^ 12) * s.sum a)

Growth-hypothesis specialization of the finite-family weak-Orlicz triangle inequality, using the abstract doubling constant already derived in PsiCalculus.lean.

theorem HCPolySupport.IndependentSums.isBigO_finset_sum_of_isBigO_growth_four_mul {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {Ψ : ℝ → ℝ} {K : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hK : 2 ≤ K) (hGrowth : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (hs : s.Nonempty) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ Ψ (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) : IsBigO μ Ψ (fun (ω : Ω) => ∑ i ∈ s, X i ω) (4 * K ^ 12 * s.sum a)

A note-facing simplification of the growth-based triangle theorem: the explicit abstract constant is bounded by 4 K^12.

theorem HCPolySupport.IndependentSums.isBigO_finsetAverage_of_isBigO {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {Ψ : ℝ → ℝ} {q C₀ : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hD : HasPsiAbstractDoubling Ψ q C₀) (hAdmissible : AdmissiblePsi Ψ) (hq : 1 < q) (hs : s.Nonempty) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ Ψ (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) : IsBigO μ Ψ (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (psiTriangleConst q C₀ * ((↑s.card)⁻¹ * s.sum a))

Average version of the finite-family weak-Orlicz triangle theorem.

theorem HCPolySupport.IndependentSums.isBigO_finsetAverage_of_isBigO_growth_four_mul {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {Ψ : ℝ → ℝ} {K : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hK : 2 ≤ K) (hGrowth : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (hs : s.Nonempty) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ Ψ (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) : IsBigO μ Ψ (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (4 * K ^ 12 * ((↑s.card)⁻¹ * s.sum a))

Note-facing average version of the growth-based triangle theorem with the coarse constant simplified to 4 K^12.

noncomputable def HCPolySupport.IndependentSums.gammaTriangleConst (σ : ℝ) : ℝ

The explicit stretched-exponential triangle constant obtained by feeding the concrete Γ_σ growth witness into the general O_Ψ calculus.

Equations

• HCPolySupport.IndependentSums.gammaTriangleConst σ = 4 * HCPolySupport.IndependentSums.gammaGrowthConst σ ^ 12

theorem HCPolySupport.IndependentSums.isBigO_finset_sum_of_isBigO_gammaSigma {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {σ : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hσ : 0 < σ) (hs : s.Nonempty) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (gammaTriangleConst σ * s.sum a)

Finite-family generalized triangle inequality specialized to the stretched-exponential class Γ_σ.

theorem HCPolySupport.IndependentSums.isBigO_finsetAverage_of_isBigO_gammaSigma {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {σ : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hσ : 0 < σ) (hs : s.Nonempty) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (gammaTriangleConst σ * ((↑s.card)⁻¹ * s.sum a))

Average version of the stretched-exponential generalized triangle inequality.

noncomputable def HCPolySupport.IndependentSums.psiSigmaTriangleConst (σ : ℝ) : ℝ

The explicit Chapter 4 triangle constant for the log-normal model class Ψ_σ, obtained from the growth constant K_{Ψ_σ} = 2 exp(2σ²).

Equations

• HCPolySupport.IndependentSums.psiSigmaTriangleConst σ = 4 * HCPolySupport.IndependentSums.psiGrowthConst σ ^ 12

theorem HCPolySupport.IndependentSums.isBigO_finset_sum_of_isBigO_psiSigma {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {σ : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hσ : 1 ≤ σ) (hs : s.Nonempty) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) : IsBigO μ (psiSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (psiSigmaTriangleConst σ * s.sum a)

Finite-family generalized triangle inequality specialized to the log-normal class Ψ_σ.

theorem HCPolySupport.IndependentSums.isBigO_finsetAverage_of_isBigO_psiSigma {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {σ : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hσ : 1 ≤ σ) (hs : s.Nonempty) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) : IsBigO μ (psiSigma σ) (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (psiSigmaTriangleConst σ * ((↑s.card)⁻¹ * s.sum a))

Average version of the log-normal generalized triangle inequality.