Coarse-graining support: Support.Book.Ch04.Theorems.Concentration

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

Public Section 4.2 concentration theorems

This file exposes the already-proved independent-sums results from Section 4.2 under the public Chapter 4 namespace. Unlike the local-observable and partition-average files, these are direct imported theorem endpoints: each theorem is proved by the existing probability mini-library.

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.gammaGrowthConst (σ : ℝ) : ℝ

Explicit growth constant for the stretched-exponential class.

Equations

• HCPolySupport.Book.Ch04.gammaGrowthConst σ = HCPolySupport.IndependentSums.gammaGrowthConst σ

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.psiGrowthConst (σ : ℝ) : ℝ

Explicit growth constant for the log-normal class.

Equations

• HCPolySupport.Book.Ch04.psiGrowthConst σ = HCPolySupport.IndependentSums.psiGrowthConst σ

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.psiGrowthTriangleConst (K : ℝ) : ℝ

The finite-family weak-tail triangle constant supplied by the Chapter 4 growth hypothesis.

Equations

• HCPolySupport.Book.Ch04.psiGrowthTriangleConst K = 4 * K ^ 12

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.gammaTriangleConst (σ : ℝ) : ℝ

The stretched-exponential weak-tail triangle constant.

Equations

• HCPolySupport.Book.Ch04.gammaTriangleConst σ = HCPolySupport.IndependentSums.gammaTriangleConst σ

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.psiSigmaTriangleConst (σ : ℝ) : ℝ

The log-normal weak-tail triangle constant.

Equations

• HCPolySupport.Book.Ch04.psiSigmaTriangleConst σ = HCPolySupport.IndependentSums.psiSigmaTriangleConst σ

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.gammaMomentConst (σ : ℝ) : ℝ

The moment-growth constant attached to Gamma_sigma.

Equations

• HCPolySupport.Book.Ch04.gammaMomentConst σ = HCPolySupport.IndependentSums.gammaMomentConst σ

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.gammaIndicatorScale (σ p : ℝ) : ℝ

The event-indicator scale |log p|^{-1/sigma} for Gamma_sigma tails.

Equations

• HCPolySupport.Book.Ch04.gammaIndicatorScale σ p = HCPolySupport.IndependentSums.gammaIndicatorScale σ p

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.gammaProductConst (σ₁ σ₂ : ℝ) : ℝ

Explicit product constant for the Gamma_sigma calculus. If tau = sigma_1 sigma_2 / (sigma_1 + sigma_2), then the product rule below uses the witness 2^(1/tau) A_1 A_2.

Equations

• HCPolySupport.Book.Ch04.gammaProductConst σ₁ σ₂ = 2 ^ (σ₁ * σ₂ / (σ₁ + σ₂))⁻¹

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.rosenthalBennettIntegralConst : ℝ

The Rosenthal/Bennett universal constant used in the finite-moment endpoint.

Equations

• HCPolySupport.Book.Ch04.rosenthalBennettIntegralConst = HCPolySupport.IndependentSums.rosenthalBennettIntegralConst

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.gammaSigmaExpRegimeEndpointConst (σ : ℝ) : ℝ

The exponential-regime endpoint constant for centered independent Gamma_sigma summands.

Equations

• HCPolySupport.Book.Ch04.gammaSigmaExpRegimeEndpointConst σ = HCPolySupport.IndependentSums.gammaSigmaExpRegimeEndpointConst σ

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.gammaSigmaHeavyTailEndpointConst (σ : ℝ) : ℝ

The heavy-tail endpoint constant for centered independent Gamma_sigma summands on the range 0 < sigma < 1.

Equations

• HCPolySupport.Book.Ch04.gammaSigmaHeavyTailEndpointConst σ = HCPolySupport.IndependentSums.gammaSigmaHeavyTailEndpointConst σ

noncomputable def HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst (σ : ℝ) : ℝ

A public constant for the full 0 < sigma ≤ 2 centered independent Gamma_sigma concentration theorem.

Equations

• HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst σ = if σ < 1 then HCPolySupport.Book.Ch04.gammaSigmaHeavyTailEndpointConst σ else HCPolySupport.Book.Ch04.gammaSigmaExpRegimeEndpointConst σ

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.psiSigmaIndependentSumConst (σ : ℝ) : ℝ

The log-normal centered independent-sum constant.

Equations

• HCPolySupport.Book.Ch04.psiSigmaIndependentSumConst σ = HCPolySupport.IndependentSums.psiSigmaIndependentSumConst σ

Weak-tail model classes and calculus

theorem HCPolySupport.Book.Ch04.admissiblePsi_gammaSigma {σ : ℝ} (hσ : 0 ≤ σ) : AdmissiblePsi (gammaSigma σ)

The stretched-exponential model class is admissible.

theorem HCPolySupport.Book.Ch04.admissiblePsi_psiSigma {σ : ℝ} (hσ : 0 ≤ σ) : AdmissiblePsi (psiSigma σ)

The log-normal model class is admissible.

theorem HCPolySupport.Book.Ch04.isBigOWith_gammaSigma_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A σ : ℝ} : IsBigOWith μ (gammaSigma σ) X A ↔ ∀ ⦃t : ℝ⦄, 1 ≤ t → μ.real (upperTailEvent X (A * t)) ≤ Real.exp (-t ^ σ)

Tail interpretation of the one-sided relation X ≤ O_{Gamma_sigma}(A).

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A σ : ℝ} : IsBigO μ (gammaSigma σ) X A ↔ ∀ ⦃t : ℝ⦄, 1 ≤ t → μ.real (absTailEvent X (A * t)) ≤ Real.exp (-t ^ σ)

Tail interpretation of X = O_{Gamma_sigma}(A).

theorem HCPolySupport.Book.Ch04.IsBigOWith.gammaSigma_mono_exponent {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A ρ σ : ℝ} (hρσ : ρ ≤ σ) (hX : IsBigOWith μ (gammaSigma σ) X A) : IsBigOWith μ (gammaSigma ρ) X A

A stretched-exponential tail at exponent σ implies the same scale at any smaller exponent ρ.

theorem HCPolySupport.Book.Ch04.IsBigO.gammaSigma_mono_exponent {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A ρ σ : ℝ} (hρσ : ρ ≤ σ) (hX : IsBigO μ (gammaSigma σ) X A) : IsBigO μ (gammaSigma ρ) X A

A symmetric stretched-exponential tail at exponent σ implies the same scale at any smaller exponent ρ.

theorem HCPolySupport.Book.Ch04.isBigOWith_psiSigma_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A σ : ℝ} : IsBigOWith μ (psiSigma σ) X A ↔ ∀ ⦃t : ℝ⦄, 1 ≤ t → μ.real (upperTailEvent X (A * t)) ≤ Real.exp (-((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2))

Tail interpretation of the one-sided relation X ≤ O_{Psi_sigma}(A).

theorem HCPolySupport.Book.Ch04.isBigO_psiSigma_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A σ : ℝ} : IsBigO μ (psiSigma σ) X A ↔ ∀ ⦃t : ℝ⦄, 1 ≤ t → μ.real (absTailEvent X (A * t)) ≤ Real.exp (-((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2))

Tail interpretation of X = O_{Psi_sigma}(A).

theorem HCPolySupport.Book.Ch04.hasPsiGrowth_gammaSigma {σ : ℝ} (hσ : 0 < σ) : HasPsiGrowth (gammaSigma σ) (gammaGrowthConst σ)

Gamma_sigma satisfies the Chapter 4 weak-tail growth hypothesis.

theorem HCPolySupport.Book.Ch04.two_le_gammaGrowthConst (σ : ℝ) : 2 ≤ gammaGrowthConst σ

The explicit Gamma_sigma growth constant is admissible for the Chapter 4 calculus.

theorem HCPolySupport.Book.Ch04.hasPsiGrowth_psiSigma {σ : ℝ} (hσ : 1 ≤ σ) : HasPsiGrowth (psiSigma σ) (psiGrowthConst σ)

Psi_sigma satisfies the Chapter 4 weak-tail growth hypothesis.

theorem HCPolySupport.Book.Ch04.two_le_psiGrowthConst (σ : ℝ) : 2 ≤ psiGrowthConst σ

The explicit Psi_sigma growth constant is admissible for the Chapter 4 calculus.

theorem HCPolySupport.Book.Ch04.hasPsiGrowth_rpow_absorption {Ψ : ℝ → ℝ} {K p t : ℝ} (hK : 1 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (ht : 1 ≤ t) : t ^ p * Ψ t ≤ Ψ (K ^ ⌈p⌉₊ * t)

Polynomial powers can be absorbed by dilating a weak-tail profile satisfying the Chapter 4 growth hypothesis.

theorem HCPolySupport.Book.Ch04.admissiblePsi_minimalGrowth {Ψ : ℝ → ℝ} {K t : ℝ} (hK : 2 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (ht : K ^ 2 ≤ t) : Real.exp (Real.log t ^ 2 / (9 * Real.log K)) ≤ Ψ t

The growth hypothesis forces log-squared minimal growth of an admissible weak-tail profile.

theorem HCPolySupport.Book.Ch04.admissiblePsi_doubling {Ψ : ℝ → ℝ} {K q t s : ℝ} (hK : 2 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (hq : 2 ≤ q) (ht : 1 ≤ t) (hs : 1 ≤ s) : s ^ q ≤ K ^ (3 * q ^ 2) * (Ψ (t * s) / Ψ t)

The growth hypothesis yields the abstract doubling estimate used in the weak-tail triangle inequality.

theorem HCPolySupport.Book.Ch04.admissiblePsi_hasPsiAbstractDoubling_two {Ψ : ℝ → ℝ} {K : ℝ} (hK : 2 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) : HasPsiAbstractDoubling Ψ 2 (K ^ 12)

The q = 2 abstract doubling package generated by the growth hypothesis.

theorem HCPolySupport.Book.Ch04.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 ω) (psiGrowthTriangleConst K * s.sum a)

Finite-family generalized triangle inequality for a weak-tail profile satisfying the Chapter 4 growth hypothesis.

theorem HCPolySupport.Book.Ch04.isBigO_finsetAverage_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 (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (psiGrowthTriangleConst K * ((↑s.card)⁻¹ * s.sum a))

Average version of the growth-based weak-tail triangle inequality.

theorem HCPolySupport.Book.Ch04.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 for Gamma_sigma tails.

theorem HCPolySupport.Book.Ch04.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 generalized triangle inequality for Gamma_sigma tails.

theorem HCPolySupport.Book.Ch04.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 for Psi_sigma tails.

theorem HCPolySupport.Book.Ch04.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 generalized triangle inequality for Psi_sigma tails.

theorem HCPolySupport.Book.Ch04.isBigOWith_gammaSigma_mul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {A B σ₁ σ₂ : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hσ₁ : 0 < σ₁) (hσ₂ : 0 < σ₂) (hA : 0 ≤ A) (_hB : 0 ≤ B) (_hX_nonneg : ∀ (ω : Ω), 0 ≤ X ω) (hY_nonneg : ∀ (ω : Ω), 0 ≤ Y ω) (hX : IsBigOWith μ (gammaSigma σ₁) X A) (hY : IsBigOWith μ (gammaSigma σ₂) Y B) : IsBigOWith μ (gammaSigma (σ₁ * σ₂ / (σ₁ + σ₂))) (fun (ω : Ω) => X ω * Y ω) (gammaProductConst σ₁ σ₂ * A * B)

Product rule for nonnegative stretched-exponential upper tails, with explicit constant 2^(1/tau), tau = sigma_1 sigma_2 / (sigma_1 + sigma_2).

theorem HCPolySupport.Book.Ch04.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)

Power rule for nonnegative stretched-exponential upper-tail bounds.

theorem HCPolySupport.Book.Ch04.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 power rule for stretched-exponential tails.

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

Finite maximum rule for common-scale nonnegative Gamma_sigma upper-tail bounds.

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_finset_sup'_of_scales {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) (hs : s.Nonempty) {X : ι → Ω → ℝ} {a : ι → ℝ} {σ : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hσ : 0 < σ) (hs_card : 2 ≤ s.card) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) (a i)) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => s.sup' hs fun (i : ι) => X i ω) ((3 * Real.log ↑s.card) ^ σ⁻¹ * s.sup' hs a)

Finite maximum rule for symmetric Gamma_sigma tails with nonuniform scales.

theorem HCPolySupport.Book.Ch04.isBigOWith_gammaSigma_indicator {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {E : Set Ω} {σ : ℝ} (hσ : 0 < σ) (hE_pos : 0 < μ.real E) (hE_lt_one : μ.real E < 1) : IsBigOWith μ (gammaSigma σ) (E.indicator fun (x : Ω) => 1) (gammaIndicatorScale σ (μ.real E))

Event indicators have the logarithmic Gamma_sigma scale from the notes.

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_indicator {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {E : Set Ω} {σ : ℝ} (hσ : 0 < σ) (hE_pos : 0 < μ.real E) (hE_lt_one : μ.real E < 1) : IsBigO μ (gammaSigma σ) (E.indicator fun (x : Ω) => 1) (gammaIndicatorScale σ (μ.real E))

Symmetric event-indicator Gamma_sigma bound.

Moment growth and Rosenthal

theorem HCPolySupport.Book.Ch04.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/sigma) implies stretched-exponential upper tails with the Chapter 4 constant e M.

theorem HCPolySupport.Book.Ch04.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 Gamma_sigma tails.

theorem HCPolySupport.Book.Ch04.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)

Tail control with witness K yields p^(1/sigma) moment growth.

theorem HCPolySupport.Book.Ch04.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

Explicit moment estimate associated to a Gamma_sigma tail witness.

theorem HCPolySupport.Book.Ch04.integral_abs_finsetSum_pow_rpow_inv_le_rosenthal_of_iIndepFun_of_integral_eq_zero {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℕ} (hp : 2 ≤ p) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ) (h_sq_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : (∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ) ^ (1 / ↑p) ≤ 2 * ↑p * (∫ (ω : Ω), (s.sup' hs fun (i : ι) => |X i ω|) ^ p ∂μ) ^ (1 / ↑p) + 4 * rosenthalBennettIntegralConst * (√↑p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))

Rosenthal's inequality in the max-term form from the notes.

theorem HCPolySupport.Book.Ch04.integral_absSum_pow_rpow_inv_le_rosenthalPolynomial {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℕ} (hp : 2 ≤ p) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hLp_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => |X i ω| ^ p) μ) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : (∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ) ^ (1 / ↑p) ≤ 2 * ↑p * (∑ i ∈ s, ∫ (ω : Ω), |X i ω| ^ p ∂μ) ^ (1 / ↑p) + 4 * rosenthalBennettIntegralConst * (√↑p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))

Rosenthal's polynomial-moment corollary for finite sums of centered independent real random variables.

theorem HCPolySupport.Book.Ch04.centeredIndependent_sum_moment_le_RosenthalBound {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℕ} {K : ℝ} (hp : 2 ≤ p) (hK_nonneg : 0 ≤ K) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hLp_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => |X i ω| ^ p) μ) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (hK : ∀ i ∈ s, (∫ (ω : Ω), |X i ω| ^ p ∂μ) ^ (1 / ↑p) ≤ K) : (∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ) ^ (1 / ↑p) ≤ 2 * ↑p * (↑s.card ^ (1 / ↑p) * K) + 4 * rosenthalBennettIntegralConst * (√↑p * (√↑s.card * K))

Uniform-K polynomial-moment Rosenthal corollary.

theorem HCPolySupport.Book.Ch04.integral_abs_finiteSum_pow_rpow_inv_le_rosenthal_uniform_polynomial {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℕ} {K : ℝ} (hp : 2 ≤ p) (hK_nonneg : 0 ≤ K) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_aemeas : ∀ (i : ι), AEMeasurable (X i) μ) (hLp_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => |X i ω| ^ p) μ) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (hK : ∀ i ∈ s, (∫ (ω : Ω), |X i ω| ^ p ∂μ) ^ (1 / ↑p) ≤ K) : (∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ) ^ (1 / ↑p) ≤ 2 * ↑p * (↑s.card ^ (1 / ↑p) * K) + 4 * rosenthalBennettIntegralConst * (√↑p * (√↑s.card * K))

Uniform-K polynomial-moment Rosenthal corollary for a.e.-measurable summands. This is the completed-law version used by Chapter 4 local-test observables: independence is kept on the original local observables, while the proof applies the measurable-mk representatives internally.

Independent-sum concentration endpoints

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_sum_iIndep_bigO_meanZero_expRegime {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hσ₁ : 1 ≤ σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (gammaSigmaExpRegimeEndpointConst σ * √↑s.card * K)

Direct concentration in the exponential regime 1 ≤ sigma ≤ 2.

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_average_iIndep_bigO_meanZero_expRegime {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hσ₁ : 1 ≤ σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (gammaSigmaExpRegimeEndpointConst σ * (√↑s.card / ↑s.card) * K)

Averaged direct concentration in the exponential regime 1 ≤ sigma ≤ 2.

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_finset_sum_of_iIndepFun_of_isBigO_of_integral_eq_zero {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hσ₀ : 0 < σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K) (h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (gammaSigmaIndependentSumConst σ * √↑s.card * K)

Full centered independent-sum concentration for Gamma_sigma, 0 < sigma ≤ 2.

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_finsetAverage_of_iIndepFun_of_isBigO_of_integral_eq_zero {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hσ₀ : 0 < σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K) (h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (gammaSigmaIndependentSumConst σ * (√↑s.card / ↑s.card) * K)

Averaged full centered independent-sum concentration for Gamma_sigma, 0 < sigma ≤ 2.

theorem HCPolySupport.Book.Ch04.upperTailProbability_finiteSum_le_exp_card_mul_add_card_mul_invPsi_of_invPsi {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Ψ : ℝ → ℝ} {X : ι → Ω → ℝ} {s : Finset ι} {a l L CΨ M : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ) (h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (hAdmissible : AdmissiblePsi Ψ) (hCΨ_nonneg : 0 ≤ CΨ) (hCΨ : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / Ψ t) ≤ ENNReal.ofReal CΨ) (hX : ∀ i ∈ s, IsBigO μ Ψ (X i) 1) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hL : 1 ≤ L) (hM : 1 ≤ M) (hconstraint : ∀ i ∈ s, ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 1 L → l * t ≤ Real.log (Ψ t) - 4 * Real.log t + Real.log M) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a) ≤ Real.exp (-l * a + ↑s.card * (l ^ 2 * (3 + M + CΨ))) + ↑s.card * (Ψ L)⁻¹

Generic heavy-tail concentration estimate for centered finite independent families under a weak-tail logarithmic constraint.

theorem HCPolySupport.Book.Ch04.isBigO_psiSigma_finset_sum_of_iIndepFun_of_isBigO_scale_of_integral_eq_zero {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ) (h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (hs : s.Nonempty) (hσ : 1 ≤ σ) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) : IsBigO μ (psiSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (psiSigmaIndependentSumConst σ * √↑s.card * K)

Log-normal centered independent-sum concentration.

theorem HCPolySupport.Book.Ch04.isBigO_psiSigma_finsetAverage_of_iIndepFun_of_isBigO_scale_of_integral_eq_zero {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ) (h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (hs : s.Nonempty) (hσ : 1 ≤ σ) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) : IsBigO μ (psiSigma σ) (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (psiSigmaIndependentSumConst σ * (√↑s.card / ↑s.card) * K)

Averaged log-normal centered independent-sum concentration.

Log-normal bridge

theorem HCPolySupport.Book.Ch04.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 imply log-normal upper tails for exp X - 1.

theorem HCPolySupport.Book.Ch04.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 imply the matching subgaussian upper-tail relation for X.