Coarse-graining support: Support.Probability.IndependentSums.GammaSigma.Basic

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

noncomputable def HCPolySupport.IndependentSums.gammaIndicatorScale (σ p : ℝ) : ℝ

The Chapter 4 indicator scale attached to an event of probability p: for 0 < p < 1 this is the quantity |log p|^{-1/σ} written as (-log p)^(-1/σ).

Equations

• HCPolySupport.IndependentSums.gammaIndicatorScale σ p = (-Real.log p) ^ (-σ⁻¹)

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

An explicit Chapter 4 moment-growth constant for the stretched-exponential class Γ_σ. It is chosen large enough to absorb the elementary gamma-integral bound used in the tail-to-moment direction.

Equations

• HCPolySupport.IndependentSums.gammaMomentConst σ = 2 * Real.exp 1 * max 1 ((2 / (σ * Real.exp 1)) ^ σ⁻¹)

def HCPolySupport.IndependentSums.HasGammaMomentGrowthWith {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (σ : ℝ) (X : Ω → ℝ) (M : ℝ) : Prop

Absolute p^{1/σ} moment growth with witness M for the stretched- exponential Chapter 4 class.

Equations

• HCPolySupport.IndependentSums.HasGammaMomentGrowthWith μ σ X M = ∀ ⦃p : ℝ⦄, 1 ≤ p → MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ p) μ ∧ ∫ (ω : Ω), |X ω| ^ p ∂μ ≤ (M * p ^ σ⁻¹) ^ p

def HCPolySupport.IndependentSums.HasGammaMomentGrowth {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (σ : ℝ) (X : Ω → ℝ) : Prop

Existential absolute Γ_σ moment growth.

Equations

• HCPolySupport.IndependentSums.HasGammaMomentGrowth μ σ X = ∃ M > 0, HCPolySupport.IndependentSums.HasGammaMomentGrowthWith μ σ X M

theorem HCPolySupport.IndependentSums.gammaMomentConst_pos {σ : ℝ} (_hσ : 0 < σ) : 0 < gammaMomentConst σ

theorem HCPolySupport.IndependentSums.hasGammaMomentGrowthWith_iff_of_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {σ M : ℝ} {Y : Ω → ℝ} (hY_nonneg : ∀ (ω : Ω), 0 ≤ Y ω) : HasGammaMomentGrowthWith μ σ Y M ↔ ∀ ⦃p : ℝ⦄, 1 ≤ p → MeasureTheory.Integrable (fun (ω : Ω) => Y ω ^ p) μ ∧ ∫ (ω : Ω), Y ω ^ p ∂μ ≤ (M * p ^ σ⁻¹) ^ p

theorem HCPolySupport.IndependentSums.rpow_mul_exp_neg_half_le {r u : ℝ} (hr : 0 < r) (hu : 0 < u) : u ^ r * Real.exp (-u / 2) ≤ (2 * r / Real.exp 1) ^ r

theorem HCPolySupport.IndependentSums.gamma_add_one_le_two_mul_rpow_div_exp {r : ℝ} (hr : 0 < r) : Real.Gamma (r + 1) ≤ 2 * (2 * r / Real.exp 1) ^ r

theorem HCPolySupport.IndependentSums.integrableOn_rpow_mul_exp_neg_rpow_of_pos {σ p : ℝ} (hσ : 0 < σ) (hp : 0 < p) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ (p - 1) * Real.exp (-t ^ σ)) (Set.Ioi 0) MeasureTheory.volume

theorem HCPolySupport.IndependentSums.gamma_moment_kernel_bound {σ p : ℝ} (hσ : 0 < σ) (hp : 1 ≤ p) : Real.exp 1 * p * (1 / σ * Real.Gamma (p / σ)) ≤ (gammaMomentConst σ * p ^ σ⁻¹) ^ p

theorem HCPolySupport.IndependentSums.lintegral_rpow_le_of_isBigOWith_gammaSigma_unit {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {σ p : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hp : 1 ≤ p) (hY_nonneg : ∀ (ω : Ω), 0 ≤ Y ω) (hYm : AEMeasurable Y μ) (hY : IsBigOWith μ (gammaSigma σ) Y 1) : ∫⁻ (ω : Ω), ENNReal.ofReal (Y ω ^ p) ∂μ ≤ ENNReal.ofReal ((gammaMomentConst σ * p ^ σ⁻¹) ^ p)

Reverse Γ_σ moment estimate at unit scale: stretched-exponential upper tails imply p^{1/σ} moment growth for every p ≥ 1.

theorem HCPolySupport.IndependentSums.lintegral_rpow_le_of_isBigOWith_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {K σ p : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hK : 0 < K) (hp : 1 ≤ p) (hY_nonneg : ∀ (ω : Ω), 0 ≤ Y ω) (hYm : AEMeasurable Y μ) (hY : IsBigOWith μ (gammaSigma σ) Y K) : ∫⁻ (ω : Ω), ENNReal.ofReal (Y ω ^ p) ∂μ ≤ ENNReal.ofReal ((gammaMomentConst σ * p ^ σ⁻¹ * K) ^ p)

Stretched-exponential upper tails imply p^{1/σ} moment growth at an arbitrary scale.

theorem HCPolySupport.IndependentSums.integral_rpow_le_of_isBigOWith_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {K σ p : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hK : 0 < K) (hp : 1 ≤ p) (hY_nonneg : ∀ (ω : Ω), 0 ≤ Y ω) (hYm : AEMeasurable Y μ) (hY : IsBigOWith μ (gammaSigma σ) Y K) : ∫ (ω : Ω), Y ω ^ p ∂μ ≤ (gammaMomentConst σ * p ^ σ⁻¹ * K) ^ p

Real-integral version of lintegral_rpow_le_of_isBigOWith_gammaSigma.

theorem HCPolySupport.IndependentSums.integrable_rpow_of_isBigOWith_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {K σ p : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hK : 0 < K) (hp : 1 ≤ p) (hY_nonneg : ∀ (ω : Ω), 0 ≤ Y ω) (hYm : AEMeasurable Y μ) (hY : IsBigOWith μ (gammaSigma σ) Y K) : MeasureTheory.Integrable (fun (ω : Ω) => Y ω ^ p) μ

Integrability consequence of stretched-exponential upper-tail control.

theorem HCPolySupport.IndependentSums.integral_abs_rpow_le_of_isBigO_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {K σ p : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hK : 0 < K) (hp : 1 ≤ p) (hXm : AEMeasurable X μ) (hX : IsBigO μ (gammaSigma σ) X K) : ∫ (ω : Ω), |X ω| ^ p ∂μ ≤ (gammaMomentConst σ * p ^ σ⁻¹ * K) ^ p

Symmetric moment estimate for the stretched-exponential class.

theorem HCPolySupport.IndependentSums.isBigOWith_gammaSigma_rpow {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A σ p : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hp : 0 < p) (hA : 0 ≤ A) (hX_nonneg : ∀ (ω : Ω), 0 ≤ X ω) (hX : IsBigOWith μ (gammaSigma σ) X A) : IsBigOWith μ (gammaSigma (σ / p)) (fun (ω : Ω) => X ω ^ p) (A ^ p)

Power rule for the stretched-exponential class on nonnegative random variables.

theorem HCPolySupport.IndependentSums.isBigOWith_gammaSigma_rpow_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A σ p : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hp : 0 < p) (hA : 0 ≤ A) (hX_nonneg : ∀ (ω : Ω), 0 ≤ X ω) : IsBigOWith μ (gammaSigma σ) X A ↔ IsBigOWith μ (gammaSigma (σ / p)) (fun (ω : Ω) => X ω ^ p) (A ^ p)

Reversible power rule for stretched-exponential upper-tail bounds on nonnegative random variables.

theorem HCPolySupport.IndependentSums.isBigO_gammaSigma_rpow_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A σ p : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hp : 0 < p) (hA : 0 ≤ A) : IsBigO μ (gammaSigma σ) X A ↔ IsBigO μ (gammaSigma (σ / p)) (fun (ω : Ω) => |X ω| ^ p) (A ^ p)

Symmetric reversible power rule for the stretched-exponential class, expressed through the note-level quantity |X|^p.

theorem HCPolySupport.IndependentSums.isBigOWith_gammaSigma_of_moment_growth {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {M σ : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hM : 0 < M) (hY_nonneg : ∀ (ω : Ω), 0 ≤ Y ω) (hY : ∀ ⦃p : ℝ⦄, 1 ≤ p → MeasureTheory.Integrable (fun (ω : Ω) => Y ω ^ p) μ ∧ ∫ (ω : Ω), Y ω ^ p ∂μ ≤ (M * p ^ σ⁻¹) ^ p) : IsBigOWith μ (gammaSigma σ) Y (Real.exp 1 * M)

Moment growth of order p^{1/σ} implies stretched-exponential upper tails with the Chapter 4 constant e M.

theorem HCPolySupport.IndependentSums.isBigO_gammaSigma_of_moment_growth {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {M σ : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hM : 0 < M) (hX : ∀ ⦃p : ℝ⦄, 1 ≤ p → MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ p) μ ∧ ∫ (ω : Ω), |X ω| ^ p ∂μ ≤ (M * p ^ σ⁻¹) ^ p) : IsBigO μ (gammaSigma σ) X (Real.exp 1 * M)

Symmetric moment-growth criterion for the stretched-exponential class.

theorem HCPolySupport.IndependentSums.hasGammaMomentGrowthWith_of_isBigOWith_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {K σ : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hK : 0 < K) (hY_nonneg : ∀ (ω : Ω), 0 ≤ Y ω) (hYm : AEMeasurable Y μ) (hY : IsBigOWith μ (gammaSigma σ) Y K) : HasGammaMomentGrowthWith μ σ Y (gammaMomentConst σ * K)

Tail control with witness K yields p^{1/σ} absolute moment growth with the explicit Chapter 4 witness gammaMomentConst σ * K.

theorem HCPolySupport.IndependentSums.isBigOWith_gammaSigma_of_hasGammaMomentGrowthWith_of_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {M σ : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hM : 0 < M) (hY_nonneg : ∀ (ω : Ω), 0 ≤ Y ω) (hY : HasGammaMomentGrowthWith μ σ Y M) : IsBigOWith μ (gammaSigma σ) Y (Real.exp 1 * M)

Absolute p^{1/σ} moment growth implies stretched-exponential upper tails with the Chapter 4 constant e M, provided the random variable is nonnegative.

theorem HCPolySupport.IndependentSums.hasGammaMomentGrowthWith_of_isBigO_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {K σ : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hK : 0 < K) (hXm : AEMeasurable X μ) (hX : IsBigO μ (gammaSigma σ) X K) : HasGammaMomentGrowthWith μ σ X (gammaMomentConst σ * K)

Symmetric tail control with witness K yields witness-level absolute moment growth with the explicit Chapter 4 constant gammaMomentConst σ * K.

theorem HCPolySupport.IndependentSums.hasGammaMomentGrowth_of_isBigO_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {K σ : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hK : 0 < K) (hXm : AEMeasurable X μ) (hX : IsBigO μ (gammaSigma σ) X K) : HasGammaMomentGrowth μ σ X

Tail control in the symmetric O_{Γ_σ} sense yields existential absolute moment growth.

theorem HCPolySupport.IndependentSums.isBigO_gammaSigma_of_hasGammaMomentGrowthWith {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {M σ : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hM : 0 < M) (hX : HasGammaMomentGrowthWith μ σ X M) : IsBigO μ (gammaSigma σ) X (Real.exp 1 * M)

Witness-level absolute moment growth directly upgrades to the symmetric O_{Γ_σ} relation.

theorem HCPolySupport.IndependentSums.hasGammaMomentGrowth_iff_exists_isBigOWith_gammaSigma_of_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {σ : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hY_nonneg : ∀ (ω : Ω), 0 ≤ Y ω) (hYm : AEMeasurable Y μ) : HasGammaMomentGrowth μ σ Y ↔ ∃ K > 0, IsBigOWith μ (gammaSigma σ) Y K

For nonnegative random variables, existential Γ_σ moment growth is equivalent to an upper-tail O_{Γ_σ} witness.

theorem HCPolySupport.IndependentSums.hasGammaMomentGrowth_iff_exists_isBigO_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {σ : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hXm : AEMeasurable X μ) : HasGammaMomentGrowth μ σ X ↔ ∃ K > 0, IsBigO μ (gammaSigma σ) X K

Existential Γ_σ moment growth is equivalent to the symmetric stretched-exponential O_{Γ_σ} relation.