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

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

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

The explicit Γ_σ moment-growth triangle constant obtained by combining the Chapter 4 tail/moment bridge with the independent-sums Γ_σ triangle inequality.

Equations

• HCPolySupport.IndependentSums.gammaMomentTriangleConst σ = HCPolySupport.IndependentSums.gammaMomentConst σ * Real.exp 1 * HCPolySupport.IndependentSums.gammaTriangleConst σ

theorem HCPolySupport.IndependentSums.gammaTriangleConst_pos {σ : ℝ} : 0 < gammaTriangleConst σ

theorem HCPolySupport.IndependentSums.gammaMomentTriangleConst_pos {σ : ℝ} (hσ : 0 < σ) : 0 < gammaMomentTriangleConst σ

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

Finite-family generalized triangle inequality in witness-level Γ_σ moment-growth form.

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

Average version of the witness-level Γ_σ moment-growth triangle inequality.

theorem HCPolySupport.IndependentSums.hasGammaMomentGrowth_finset_sum {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ι : Type u_2} (s : Finset ι) {X : ι → Ω → ℝ} {σ : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hs : s.Nonempty) (hX : ∀ i ∈ s, HasGammaMomentGrowth μ σ (X i)) (hXm : ∀ i ∈ s, Measurable (X i)) : HasGammaMomentGrowth μ σ fun (ω : Ω) => ∑ i ∈ s, X i ω

Finite-family generalized triangle inequality for existential Γ_σ moment-growth witnesses.

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

Average version of the existential Γ_σ moment-growth triangle inequality.

theorem HCPolySupport.IndependentSums.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 belong to the stretched-exponential class with the natural logarithmic scale from the Chapter 4 notes.

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

Event indicators also satisfy the symmetric O_{Γ_σ} relation, since the indicator is already nonnegative.

theorem HCPolySupport.IndependentSums.isBigOWith_gammaSigma_finset_sup' {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ι : Type u_2} (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 bound in the stretched-exponential class. This is the finite-family version of the Chapter 4 maximum lemma with the note-facing constant (3 log N)^{1/σ}.

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

Finite-maximum bound with nonuniform witness scales: the common scale is the supremum of the individual witnesses.

theorem HCPolySupport.IndependentSums.isBigOWith_gammaSigma_finset_sup'_abs_of_scales {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ι : Type u_2} (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)) : IsBigOWith μ (gammaSigma σ) (fun (ω : Ω) => s.sup' hs fun (i : ι) => |X i ω|) ((3 * Real.log ↑s.card) ^ σ⁻¹ * s.sup' hs a)

Absolute finite-maximum bound with nonuniform witness scales.

theorem HCPolySupport.IndependentSums.isBigO_gammaSigma_finset_sup'_of_scales {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ι : Type u_2} (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)

Symmetric finite-maximum bound with nonuniform witness scales.

theorem HCPolySupport.IndependentSums.hasGammaMomentGrowthWith_finset_sup'_of_scales {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ι : Type u_2} (s : Finset ι) (hs : s.Nonempty) {X : ι → Ω → ℝ} {a : ι → ℝ} {σ : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hs_card : 2 ≤ s.card) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, HasGammaMomentGrowthWith μ σ (X i) (a i)) (hXm : ∀ i ∈ s, Measurable (X i)) : HasGammaMomentGrowthWith μ σ (fun (ω : Ω) => s.sup' hs fun (i : ι) => X i ω) (gammaMomentConst σ * ((3 * Real.log ↑s.card) ^ σ⁻¹ * (Real.exp 1 * s.sup' hs a)))

Finite-maximum bound in witness-level Γ_σ moment-growth form.

theorem HCPolySupport.IndependentSums.hasGammaMomentGrowth_finset_sup' {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ι : Type u_2} (s : Finset ι) (hs : s.Nonempty) {X : ι → Ω → ℝ} {σ : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hσ : 0 < σ) (hs_card : 2 ≤ s.card) (hX : ∀ i ∈ s, HasGammaMomentGrowth μ σ (X i)) (hXm : ∀ i ∈ s, Measurable (X i)) : HasGammaMomentGrowth μ σ fun (ω : Ω) => s.sup' hs fun (i : ι) => X i ω

Existential finite-maximum bound for the Γ_σ moment-growth class.