Coarse-graining support: Support.Probability.IndependentSums.GammaSigmaExpRegime.OneVariable

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

theorem HCPolySupport.IndependentSums.mgf_le_one_add_tsum_geometric_of_gammaMomentGrowth_small_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ M l : ℝ} (hXm : AEMeasurable X μ) (hσ : 1 ≤ σ) (hM : 0 ≤ M) (hl : 0 ≤ l) (hl_small : l ≤ (2 * Real.exp 1 * M)⁻¹) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) (hXmom : HasGammaMomentGrowthWith μ σ X M) : ProbabilityTheory.mgf X μ l ≤ 1 + ∑' (n : ℕ), (Real.exp 1 * M * l) ^ (n + 2)

Small-λ mgf bound for a centered Γ_σ random variable, in the raw geometric-tail form that comes directly from the exponential power series.

theorem HCPolySupport.IndependentSums.mgf_le_one_add_linear_add_tsum_geometric_of_gammaMomentGrowth_small {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ M l : ℝ} (hXm : AEMeasurable X μ) (hσ : 1 ≤ σ) (hM : 0 ≤ M) (hl : 0 ≤ l) (hl_small : l ≤ (2 * Real.exp 1 * M)⁻¹) (hXmom : HasGammaMomentGrowthWith μ σ X M) : ProbabilityTheory.mgf X μ l ≤ 1 + l * M + ∑' (n : ℕ), (Real.exp 1 * M * l) ^ (n + 2)

Small-λ mgf bound without the centering hypothesis. The linear term is controlled by the first absolute moment.

theorem HCPolySupport.IndependentSums.mgf_le_one_add_two_mul_sq_of_gammaMomentGrowth_small_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ M l : ℝ} (hXm : AEMeasurable X μ) (hσ : 1 ≤ σ) (hM : 0 ≤ M) (hl : 0 ≤ l) (hl_small : l ≤ (2 * Real.exp 1 * M)⁻¹) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) (hXmom : HasGammaMomentGrowthWith μ σ X M) : ProbabilityTheory.mgf X μ l ≤ 1 + 2 * (Real.exp 1 * M * l) ^ 2

Clean small-λ mgf estimate for centered Γ_σ random variables in the exponential regime σ ≥ 1.

theorem HCPolySupport.IndependentSums.mgf_le_exp_two_mul_sq_of_gammaMomentGrowth_small_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ M l : ℝ} (hXm : AEMeasurable X μ) (hσ : 1 ≤ σ) (hM : 0 ≤ M) (hl : 0 ≤ l) (hl_small : l ≤ (2 * Real.exp 1 * M)⁻¹) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) (hXmom : HasGammaMomentGrowthWith μ σ X M) : ProbabilityTheory.mgf X μ l ≤ Real.exp (2 * (Real.exp 1 * M * l) ^ 2)

Exponential small-λ mgf estimate for centered Γ_σ random variables in the regime σ ≥ 1.

theorem HCPolySupport.IndependentSums.mgf_le_two_of_gammaMomentGrowth_quarter_small {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ M l : ℝ} (hXm : AEMeasurable X μ) (hσ : 1 ≤ σ) (hM : 0 < M) (hl : 0 ≤ l) (hl_quarter : l ≤ (4 * Real.exp 1 * M)⁻¹) (hXmom : HasGammaMomentGrowthWith μ σ X M) : ProbabilityTheory.mgf X μ l ≤ 2

Under the stronger quarter-scale hypothesis e M λ ≤ 1/4, the small-λ mgf is universally bounded by 2.

theorem HCPolySupport.IndependentSums.mgf_le_two_mul_exp_of_gammaMomentGrowth_of_one_lt {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ M l : ℝ} (hXm : AEMeasurable X μ) (hσ : 1 < σ) (hM : 0 < M) (hl : 0 ≤ l) (hXmom : HasGammaMomentGrowthWith μ σ X M) : ProbabilityTheory.mgf X μ l ≤ 2 * Real.exp (gammaExpLargeLambdaConst σ * (Real.exp 1 * M * l) ^ gammaExpConjExponent σ)

One-variable exponential mgf bound in the Chapter 4 regime σ > 1. The proof reduces |X|^σ to a unit-scale Γ₁ random variable and feeds it through the small-parameter Γ₁ mgf estimate.

theorem HCPolySupport.IndependentSums.integrable_exp_mul_of_gammaMomentGrowth_of_one_lt {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ M l : ℝ} (hXm : AEMeasurable X μ) (hσ : 1 < σ) (hM : 0 < M) (hl : 0 ≤ l) (hXmom : HasGammaMomentGrowthWith μ σ X M) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * X ω)) μ

Exponential integrability in the Chapter 4 large-λ regime σ > 1.

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

Explicit coefficient after pushing the large-λ mgf estimate from moment-growth witnesses back to the note-facing O_{Γ_σ} scale.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.IndependentSums.mgf_le_two_mul_exp_of_isBigO_gammaSigma_of_one_lt {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ K l : ℝ} (hXm : AEMeasurable X μ) (hσ : 1 < σ) (hK : 0 < K) (hl : 0 ≤ l) (hX : IsBigO μ (gammaSigma σ) X K) : ProbabilityTheory.mgf X μ l ≤ 2 * Real.exp (gammaSigmaLargeMgfConst σ * (K * l) ^ gammaExpConjExponent σ)

Large-λ one-variable mgf bound stated directly for O_{Γ_σ} random variables with σ > 1.

theorem HCPolySupport.IndependentSums.integrable_exp_mul_of_isBigO_gammaSigma_of_one_lt {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ K l : ℝ} (hXm : AEMeasurable X μ) (hσ : 1 < σ) (hK : 0 < K) (hl : 0 ≤ l) (hX : IsBigO μ (gammaSigma σ) X K) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * X ω)) μ

Exponential integrability in the note-facing O_{Γ_σ} language for σ > 1.

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_le_exp_of_gammaMomentGrowth_small_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ M l a : ℝ} (hXm : AEMeasurable X μ) (hσ : 1 ≤ σ) (hM : 0 ≤ M) (hl : 0 ≤ l) (hl_small : l ≤ (2 * Real.exp 1 * M)⁻¹) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) (hXmom : HasGammaMomentGrowthWith μ σ X M) : μ.real (upperTailEvent X a) ≤ Real.exp (-l * a + 2 * (Real.exp 1 * M * l) ^ 2)

Chernoff upper-tail estimate coming from the small-λ Γ_σ mgf bound.

theorem HCPolySupport.IndependentSums.measureReal_absTailEvent_le_two_mul_exp_of_gammaMomentGrowth_small_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ M l a : ℝ} (hXm : AEMeasurable X μ) (hσ : 1 ≤ σ) (hM : 0 ≤ M) (hl : 0 ≤ l) (hl_small : l ≤ (2 * Real.exp 1 * M)⁻¹) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) (hXmom : HasGammaMomentGrowthWith μ σ X M) : μ.real (absTailEvent X a) ≤ 2 * Real.exp (-l * a + 2 * (Real.exp 1 * M * l) ^ 2)

Absolute-tail version of the small-λ Γ_σ Chernoff estimate.