Coarse-graining support: Support.Probability.IndependentSums.GammaSigmaConcentration.SmallRegime

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

theorem HCPolySupport.IndependentSums.upperTailProbability_finiteSum_le_exp_card_mul_add_card_mul_exp_neg {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ a l L : ℝ} (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) (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) 1) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hL : 1 ≤ L) (hlL : l ≤ 1 / 2 * L ^ (σ - 1)) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a) ≤ Real.exp (-l * a + ↑s.card * (l ^ 2 * gammaSigmaHeavyTailRoundedConst σ)) + ↑s.card * Real.exp (-L ^ σ)

Specialized rounded heavy-tail concentration estimate for Γ_σ on the range σ ∈ (0, 1). This is the concrete Γ_σ wrapper around the generic rounded truncation-Chernoff theorem from PsiConcentration.lean.

theorem HCPolySupport.IndependentSums.four_le_gammaSigmaHeavyTailRoundedConst {σ : ℝ} (hσ : 0 < σ) : 4 ≤ gammaSigmaHeavyTailRoundedConst σ

The rounded heavy-tail scale is uniformly at least 4, so its square root is at least 2.

theorem HCPolySupport.IndependentSums.two_le_sqrt_gammaSigmaHeavyTailRoundedConst {σ : ℝ} (hσ : 0 < σ) : 2 ≤ √(gammaSigmaHeavyTailRoundedConst σ)

theorem HCPolySupport.IndependentSums.gammaSigmaHeavyTailConst_pos {σ : ℝ} (hσ : 0 < σ) : 0 < gammaSigmaHeavyTailConst σ

theorem HCPolySupport.IndependentSums.heavyTail_rpow_choice_eq {σ l : ℝ} (hσ₁ : σ < 1) (hl : 0 < l) : have L := (2 * l) ^ (-(1 / (1 - σ))); 1 / 2 * L ^ (σ - 1) = l

theorem HCPolySupport.IndependentSums.one_le_heavyTail_rpow_choice {σ l : ℝ} (hσ₁ : σ < 1) (hl : 0 < l) (hl_half : l ≤ 1 / 2) : 1 ≤ (2 * l) ^ (-(1 / (1 - σ)))

theorem HCPolySupport.IndependentSums.card_mul_exp_neg_gammaSigmaHeavyTailUnionConst_mul_le_exp_neg_two_mul {σ R x : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hR_one : 1 ≤ R) (hx_nonneg : 0 ≤ x) (hcardPow : R ^ (σ / (2 - σ)) ≤ x) : R * Real.exp (-(gammaSigmaHeavyTailUnionConst σ * x)) ≤ Real.exp (-2 * x)

theorem HCPolySupport.IndependentSums.two_mul_exp_neg_two_mul_le_exp_neg {x : ℝ} (hx : 1 ≤ x) : 2 * Real.exp (-2 * x) ≤ Real.exp (-x)

theorem HCPolySupport.IndependentSums.smallRegime_heavyTail_mgf_le {σ R t : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hR_pos : 0 < R) (ht : 1 ≤ t) : have D := gammaSigmaHeavyTailRoundedConst σ; have B := gammaSigmaHeavyTailConst σ; have l := t / (4 * √D * √R); Real.exp (-l * (B * √R * t) + R * (l ^ 2 * D)) ≤ Real.exp (-2 * t ^ σ)

The small-regime heavy-tail choice gives the desired quadratic mgf decay.

theorem HCPolySupport.IndependentSums.smallRegime_heavyTail_union_le {σ R t : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hR_pos : 0 < R) (hR_one : 1 ≤ R) (ht : 1 ≤ t) (hsmall : t ≤ R ^ (σ / (2 * (2 - σ)))) : have D := gammaSigmaHeavyTailRoundedConst σ; have L := (2 * √D * (√R / t)) ^ (1 / (1 - σ)); R * Real.exp (-L ^ σ) ≤ Real.exp (-2 * t ^ σ)

The small-regime heavy-tail cutoff gives the desired tail decay for the union term.

theorem HCPolySupport.IndependentSums.upperTailProbability_finiteSum_le_exp_neg_of_iIndepFun_of_isBigO_of_iIndepFun {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ t : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) 1) (h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (ht : 1 ≤ t) (hsmall : t ≤ ↑s.card ^ (σ / (2 * (2 - σ)))) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) (gammaSigmaHeavyTailConst σ * √↑s.card * t)) ≤ Real.exp (-t ^ σ)

Small-regime one-sided heavy-tail concentration for centered independent unit-scale O_{Γ_σ} summands.