Coarse-graining support: Support.Probability.IndependentSums.PsiSigma.Calculus

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

theorem HCPolySupport.IndependentSums.isBigOWith_psiSigma_exp_sub_one_of_isBigOWith_gammaTwo {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {σ : ℝ} (hσ : 1 ≤ σ) (hX : IsBigOWith μ (gammaSigma 2) X σ) : IsBigOWith μ (psiSigma σ) (fun (ω : Ω) => Real.exp (X ω) - 1) (Real.exp σ - 1)

Subgaussian upper tails at scale σ imply log-normal upper tails for exp(X) - 1, with the explicit witness exp(σ) - 1. This is the forward bridge from the Chapter 4 log-normal remark in the t ≥ 1 weak-tail convention used by the project.

theorem HCPolySupport.IndependentSums.isBigOWith_gammaTwo_of_isBigOWith_psiSigma_exp_sub_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {σ : ℝ} (hσ : 1 ≤ σ) (hX : IsBigOWith μ (psiSigma σ) (fun (ω : Ω) => Real.exp (X ω) - 1) σ) : IsBigOWith μ (gammaSigma 2) X σ

Log-normal upper tails for exp(X) - 1 at scale σ imply the subgaussian upper-tail relation for X at the same scale. This is the exact reverse implication from the Chapter 4 log-normal remark.

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

Constant-scale finite-family log-normal triangle inequality.

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

Constant-scale average log-normal triangle inequality.

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

Unit-scale finite-family log-normal triangle inequality.

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

Unit-scale average log-normal triangle inequality.