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

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

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

The Hölder-conjugate exponent σ / (σ - 1) used in the large-λ exponential regime when 1 < σ.

Equations

• HCPolySupport.IndependentSums.gammaExpConjExponent σ = σ / (σ - 1)

theorem HCPolySupport.IndependentSums.gammaExpConjExponent_pos {σ : ℝ} (hσ : 1 < σ) : 0 < gammaExpConjExponent σ

theorem HCPolySupport.IndependentSums.gammaExpConjExponent_holderConjugate {σ : ℝ} (hσ : 1 < σ) : σ.HolderConjugate (gammaExpConjExponent σ)

theorem HCPolySupport.IndependentSums.inv_gammaExpConjExponent {σ : ℝ} (hσ : 1 < σ) : (gammaExpConjExponent σ)⁻¹ = (σ - 1) / σ

theorem HCPolySupport.IndependentSums.gammaExp_young {σ l t : ℝ} (hσ : 1 < σ) (hl : 0 ≤ l) (ht : 0 ≤ t) : l * t ≤ t ^ σ / σ + (σ - 1) / σ * l ^ gammaExpConjExponent σ

Young's inequality in the Chapter 4 large-λ shape.

theorem HCPolySupport.IndependentSums.gammaExp_young_scale {σ B l t : ℝ} (hσ : 1 < σ) (hB : 0 ≤ B) (hl : 0 ≤ l) (ht : 0 ≤ t) : l * (B * t) ≤ t ^ σ / σ + (σ - 1) / σ * (B * l) ^ gammaExpConjExponent σ

Scaled Young inequality matching the tail parameterization x = B t.

theorem HCPolySupport.IndependentSums.gammaExp_largeLambda_exponent_le {σ l t : ℝ} (hσ : 1 < σ) (hl : 0 ≤ l) (ht : 0 ≤ t) : l * t - t ^ σ ≤ (σ - 1) / σ * l ^ gammaExpConjExponent σ - (σ - 1) / σ * t ^ σ

Exponent comparison extracted from gammaExp_young. This is the basic kernel estimate behind the large-λ regime.

theorem HCPolySupport.IndependentSums.exp_gammaExp_largeLambda_exponent_le {σ l t : ℝ} (hσ : 1 < σ) (hl : 0 ≤ l) (ht : 0 ≤ t) : Real.exp (l * t - t ^ σ) ≤ Real.exp ((σ - 1) / σ * l ^ gammaExpConjExponent σ) * Real.exp (-((σ - 1) / σ) * t ^ σ)

Exponential form of the Chapter 4 large-λ kernel comparison.

theorem HCPolySupport.IndependentSums.gammaExpSlope_pos {σ : ℝ} (hσ : 1 < σ) : 0 < (σ - 1) / σ

theorem HCPolySupport.IndependentSums.summable_nat_sq_mul_exp_gammaExpKernel {σ α : ℝ} (hσ : 1 < σ) (hα : 0 ≤ α) : Summable fun (n : ℕ) => ↑n ^ 2 * Real.exp (α * ↑n - ↑n ^ σ)

The large-λ shell kernel is summable after comparison with an exponentially decaying sequence.

noncomputable def HCPolySupport.IndependentSums.gammaExpYoungScaleConst (σ δ : ℝ) : ℝ

The scaling constant produced by the δ-version of Young's inequality in the exponential regime σ > 1.

Equations

• HCPolySupport.IndependentSums.gammaExpYoungScaleConst σ δ = (σ - 1) / σ * ((σ * δ) ^ σ⁻¹)⁻¹ ^ HCPolySupport.IndependentSums.gammaExpConjExponent σ

theorem HCPolySupport.IndependentSums.gammaExpYoungScaleConst_pos {σ δ : ℝ} (hσ : 1 < σ) (hδ : 0 < δ) : 0 < gammaExpYoungScaleConst σ δ

theorem HCPolySupport.IndependentSums.gammaExp_young_scale_delta {σ B l t δ : ℝ} (hσ : 1 < σ) (hB : 0 ≤ B) (hl : 0 ≤ l) (ht : 0 ≤ t) (hδ : 0 < δ) : l * (B * t) ≤ δ * t ^ σ + gammaExpYoungScaleConst σ δ * (B * l) ^ gammaExpConjExponent σ

δ-scaled Young inequality in the Chapter 4 exponential regime.

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

Fixed coefficient appearing in the one-variable large-λ mgf estimate for the Chapter 4 exponential regime σ > 1.

Equations

• HCPolySupport.IndependentSums.gammaExpLargeLambdaConst σ = HCPolySupport.IndependentSums.gammaExpYoungScaleConst σ (4 * Real.exp 1 * HCPolySupport.IndependentSums.gammaMomentConst 1)⁻¹

noncomputable def HCPolySupport.IndependentSums.gammaExpTaylorTail {Ω : Type u_1} (l : ℝ) (X : Ω → ℝ) (n : ℕ) : Ω → ℝ

The Taylor tail used in the small-λ mgf expansion.

Equations

• HCPolySupport.IndependentSums.gammaExpTaylorTail l X n ω = (l * X ω) ^ (n + 2) / ↑(n + 2).factorial

noncomputable def HCPolySupport.IndependentSums.gammaExpSeriesTerm {Ω : Type u_1} (l : ℝ) (X : Ω → ℝ) (n : ℕ) : Ω → ℝ

The full exponential-series term attached to l * X.

Equations

• HCPolySupport.IndependentSums.gammaExpSeriesTerm l X n ω = (l * X ω) ^ n / ↑n.factorial

theorem HCPolySupport.IndependentSums.gammaExpTaylorTail_eq_gammaExpSeriesTerm_add_two {Ω : Type u_1} (l : ℝ) (X : Ω → ℝ) (n : ℕ) : gammaExpTaylorTail l X n = gammaExpSeriesTerm l X (n + 2)

theorem HCPolySupport.IndependentSums.nat_div_exp_pow_le_factorial (n : ℕ) : (↑n / Real.exp 1) ^ n ≤ ↑n.factorial

theorem HCPolySupport.IndependentSums.nat_pow_div_factorial_le_exp_nat (n : ℕ) : ↑n ^ n / ↑n.factorial ≤ Real.exp ↑n

theorem HCPolySupport.IndependentSums.gammaMomentGrowth_natCast_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {σ M : ℝ} {X : Ω → ℝ} {n : ℕ} (hn : 1 ≤ n) (hXmom : HasGammaMomentGrowthWith μ σ X M) : MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ n) μ ∧ ∫ (ω : Ω), |X ω| ^ n ∂μ ≤ (M * ↑n ^ σ⁻¹) ^ n

theorem HCPolySupport.IndependentSums.gammaMomentGrowth_natCast_term_le {σ M l : ℝ} {n : ℕ} (hn : 1 ≤ n) (hσ : 1 ≤ σ) (hM_nonneg : 0 ≤ M) (hl_nonneg : 0 ≤ l) : (M * l * ↑n ^ σ⁻¹) ^ n / ↑n.factorial ≤ (Real.exp 1 * M * l) ^ n

theorem HCPolySupport.IndependentSums.integral_norm_gammaExpTaylorTail_le_geometric {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {σ M l : ℝ} (n : ℕ) (hσ : 1 ≤ σ) (hM : 0 ≤ M) (hl : 0 ≤ l) (hXmom : HasGammaMomentGrowthWith μ σ X M) : ∫ (ω : Ω), ‖gammaExpTaylorTail l X n ω‖ ∂μ ≤ (Real.exp 1 * M * l) ^ (n + 2)

The normed Taylor tail is controlled by the geometric scale (e M λ)^(n+2) once Γ_σ moment growth is available with σ ≥ 1.

theorem HCPolySupport.IndependentSums.summable_integral_norm_gammaExpTaylorTail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {σ M l : ℝ} (hσ : 1 ≤ σ) (hM : 0 ≤ M) (hl : 0 ≤ l) (hl_small : l ≤ (2 * Real.exp 1 * M)⁻¹) (hXmom : HasGammaMomentGrowthWith μ σ X M) : Summable fun (n : ℕ) => ∫ (ω : Ω), ‖gammaExpTaylorTail l X n ω‖ ∂μ

Under the Chapter 4 small-λ hypothesis e M λ ≤ 1/2, the Taylor tails form a summable family in L¹. This is the summability input needed to interchange the mgf integral with the exponential power series.

theorem HCPolySupport.IndependentSums.integrable_gammaExpSeriesTerm_of_one_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {σ M l : ℝ} {n : ℕ} (hn : 1 ≤ n) (hXm : AEMeasurable X μ) (hl : 0 ≤ l) (hXmom : HasGammaMomentGrowthWith μ σ X M) : MeasureTheory.Integrable (gammaExpSeriesTerm l X n) μ

theorem HCPolySupport.IndependentSums.integrable_gammaExpSeriesTerm {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ M l : ℝ} (n : ℕ) (hXm : AEMeasurable X μ) (hl : 0 ≤ l) (hXmom : HasGammaMomentGrowthWith μ σ X M) : MeasureTheory.Integrable (gammaExpSeriesTerm l X n) μ

theorem HCPolySupport.IndependentSums.summable_integral_norm_gammaExpSeriesTerm {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {σ M l : ℝ} (hσ : 1 ≤ σ) (hM : 0 ≤ M) (hl : 0 ≤ l) (hl_small : l ≤ (2 * Real.exp 1 * M)⁻¹) (hXmom : HasGammaMomentGrowthWith μ σ X M) : Summable fun (n : ℕ) => ∫ (ω : Ω), ‖gammaExpSeriesTerm l X n ω‖ ∂μ

theorem HCPolySupport.IndependentSums.ae_summable_norm_gammaExpSeriesTerm {Ω : 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) : ∀ᵐ (ω : Ω) ∂μ, Summable fun (n : ℕ) => ‖gammaExpSeriesTerm l X n ω‖

theorem HCPolySupport.IndependentSums.integrable_tsum_norm_gammaExpSeriesTerm {Ω : 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) : MeasureTheory.Integrable (fun (ω : Ω) => ∑' (n : ℕ), ‖gammaExpSeriesTerm l X n ω‖) μ

theorem HCPolySupport.IndependentSums.integrable_exp_mul_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) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * X ω)) μ

theorem HCPolySupport.IndependentSums.mgf_pos_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) : 0 < ProbabilityTheory.mgf X μ l