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

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

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

Explicit upper bound for the Chapter 4 tail integral ∫_1^∞ t e^{-t^σ} dt. We use the full (0, ∞) Gamma-integral value because it is simpler to package and still sufficient for the generic heavy-tail backend.

Equations

• HCPolySupport.IndependentSums.gammaSigmaTailIntegralConst σ = 1 / σ * Real.Gamma (2 / σ)

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

Explicit logarithmic-control constant for the Γ_σ specialization.

Equations

• HCPolySupport.IndependentSums.gammaSigmaLogControlConst σ = Real.exp (32 / σ ^ 2)

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

Rounded scalar constant appearing in the specialized Γ_σ heavy-tail mgf bound after feeding gammaSigmaTailIntegralConst and gammaSigmaLogControlConst into the generic rounded backend.

Equations

• HCPolySupport.IndependentSums.gammaSigmaHeavyTailRoundedConst σ = 3 + HCPolySupport.IndependentSums.gammaSigmaLogControlConst σ + HCPolySupport.IndependentSums.gammaSigmaTailIntegralConst σ

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

Auxiliary union-term constant for the corrected small-σ Chapter 4 concentration split.

Equations

• HCPolySupport.IndependentSums.gammaSigmaHeavyTailUnionConst σ = (2 * √(HCPolySupport.IndependentSums.gammaSigmaHeavyTailRoundedConst σ)) ^ (σ / (1 - σ))

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

Explicit one-sided sqrt(card) scale for the heavy-tail Γ_σ concentration theorem on the range σ ∈ (0, 1).

Equations

• HCPolySupport.IndependentSums.gammaSigmaHeavyTailConst σ = 16 * √(HCPolySupport.IndependentSums.gammaSigmaHeavyTailRoundedConst σ)

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

Symmetric sqrt(card) scale for the heavy-tail Γ_σ concentration theorem on the range σ ∈ (0, 1). The factor 2^(1/σ) absorbs the two-sided tail union.

Equations

• HCPolySupport.IndependentSums.gammaSigmaHeavyTailEndpointConst σ = 2 ^ (1 / σ) * HCPolySupport.IndependentSums.gammaSigmaHeavyTailConst σ

theorem HCPolySupport.IndependentSums.gammaSigmaTailIntegralConst_nonneg {σ : ℝ} (hσ : 0 < σ) : 0 ≤ gammaSigmaTailIntegralConst σ

theorem HCPolySupport.IndependentSums.gammaSigmaHeavyTailRoundedConst_pos {σ : ℝ} (hσ : 0 < σ) : 0 < gammaSigmaHeavyTailRoundedConst σ

theorem HCPolySupport.IndependentSums.one_le_gammaSigmaLogControlConst (σ : ℝ) : 1 ≤ gammaSigmaLogControlConst σ

theorem HCPolySupport.IndependentSums.two_add_two_div_le_gammaSigmaHeavyTailUnionConst {σ : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) : 2 + 2 / σ ≤ gammaSigmaHeavyTailUnionConst σ

theorem HCPolySupport.IndependentSums.four_mul_log_le_half_rpow_add_log_gammaSigmaLogControlConst {σ t : ℝ} (hσ : 0 < σ) (ht : 1 ≤ t) : 4 * Real.log t ≤ 1 / 2 * t ^ σ + Real.log (gammaSigmaLogControlConst σ)

The concrete logarithmic control from the Chapter 4 notes, with an explicit choice of constant that is convenient in Lean.

theorem HCPolySupport.IndependentSums.lintegral_Ioi_one_gammaSigma_le_gammaSigmaTailIntegralConst {σ : ℝ} (hσ : 0 < σ) : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / gammaSigma σ t) ≤ ENNReal.ofReal (gammaSigmaTailIntegralConst σ)

The Γ_σ tail integral on (1, ∞) is controlled by the explicit Gamma constant gammaSigmaTailIntegralConst σ.

theorem HCPolySupport.IndependentSums.gammaSigma_log_constraint {σ l L t : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hlL : l ≤ 1 / 2 * L ^ (σ - 1)) (ht : t ∈ Set.Icc 1 L) : l * t ≤ Real.log (gammaSigma σ t) - 4 * Real.log t + Real.log (gammaSigmaLogControlConst σ)

If λ ≤ (1/2) L^(σ - 1) and 1 ≤ t ≤ L, then the deterministic part of the Γ_σ logarithmic kernel constraint holds.

theorem HCPolySupport.IndependentSums.smallRegime_sq_le_gammaSigmaTailPower {σ R t : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hR_pos : 0 < R) (ht_pos : 0 < t) (hsmall : t ≤ R ^ (σ / (2 * (2 - σ)))) : t ^ 2 ≤ (√R / t) ^ (σ / (1 - σ))

theorem HCPolySupport.IndependentSums.smallRegime_cardPow_le_gammaSigmaTailPower {σ R t : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hR_pos : 0 < R) (ht_pos : 0 < t) (hsmall : t ≤ R ^ (σ / (2 * (2 - σ)))) : R ^ (σ / (2 - σ)) ≤ (√R / t) ^ (σ / (1 - σ))

theorem HCPolySupport.IndependentSums.largeRegime_cardPow_le_gammaSigmaScale {σ R t : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hR_pos : 0 < R) (ht_pos : 0 < t) (hlarge : R ^ (σ / (2 * (2 - σ))) ≤ t) : R ^ (σ / (2 - σ)) ≤ R ^ (σ / 2) * t ^ σ

theorem HCPolySupport.IndependentSums.largeRegime_correction_le_gammaSigmaScale {σ R t : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hR_pos : 0 < R) (ht_pos : 0 < t) (hlarge : R ^ (σ / (2 * (2 - σ))) ≤ t) : R ^ σ * t ^ (2 * σ - 2) ≤ R ^ (σ / 2) * t ^ σ