Coarse-graining support: Support.Probability.IndependentSums.PsiCalculus

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

The first abstract calculus for Chapter 4 weak-Orlicz tails.

This file begins the formalization of the growth-condition arguments from the notes. The immediate goal is Step 1 of the O_Ψ calculus: polynomial factors can be absorbed into a dilation of the argument of Ψ.

def HCPolySupport.IndependentSums.HasPsiGrowth (Ψ : ℝ → ℝ) (K : ℝ) : Prop

The Chapter 4 growth hypothesis t Ψ(t) ≤ Ψ(K t) for t ≥ 1.

Equations

• HCPolySupport.IndependentSums.HasPsiGrowth Ψ K = ∀ ⦃t : ℝ⦄, 1 ≤ t → t * Ψ t ≤ Ψ (K * t)

def HCPolySupport.IndependentSums.HasPsiAbstractDoubling (Ψ : ℝ → ℝ) (q C₀ : ℝ) : Prop

The abstract doubling condition used in Step 5 of the Chapter 4 generalized triangle inequality argument.

Equations

• HCPolySupport.IndependentSums.HasPsiAbstractDoubling Ψ q C₀ = ∀ ⦃t s : ℝ⦄, 1 ≤ t → 1 ≤ s → s ^ q ≤ C₀ * (Ψ (t * s) / Ψ t)

def HCPolySupport.IndependentSums.natTriangular : ℕ → ℕ

The recursive triangular-number exponent that appears in the inductive polynomial-absorption estimate.

Equations

• HCPolySupport.IndependentSums.natTriangular 0 = 0
• HCPolySupport.IndependentSums.natTriangular n.succ = HCPolySupport.IndependentSums.natTriangular n + n

@[simp]

theorem HCPolySupport.IndependentSums.natTriangular_zero : natTriangular 0 = 0

@[simp]

theorem HCPolySupport.IndependentSums.natTriangular_succ (n : ℕ) : natTriangular (n + 1) = natTriangular n + n

theorem HCPolySupport.IndependentSums.one_le_pow_of_one_le_real {x : ℝ} (hx : 1 ≤ x) (n : ℕ) : 1 ≤ x ^ n

theorem HCPolySupport.IndependentSums.hasPsiGrowth_nat_polyAbsorptionPre {Ψ : ℝ → ℝ} {K : ℝ} (hK : 1 ≤ K) (hΨ : HasPsiGrowth Ψ K) (n : ℕ) ⦃t : ℝ⦄ : 1 ≤ t → t ^ n * Ψ t ≤ (K ^ natTriangular n)⁻¹ * Ψ (K ^ n * t)

theorem HCPolySupport.IndependentSums.hasPsiGrowth_nat_polyAbsorption {Ψ : ℝ → ℝ} {K : ℝ} (hK : 1 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (n : ℕ) ⦃t : ℝ⦄ : 1 ≤ t → t ^ n * Ψ t ≤ Ψ (K ^ n * t)

A weaker but convenient corollary of the pre-absorption estimate: natural polynomial factors can be absorbed into the argument of Ψ without tracking the sharpening prefactor from the notes.

theorem HCPolySupport.IndependentSums.admissiblePsi_lowerBound_pow_natTriangular {Ψ : ℝ → ℝ} {K : ℝ} (hK : 1 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (n : ℕ) : K ^ natTriangular n ≤ Ψ (K ^ n)

theorem HCPolySupport.IndependentSums.hasPsiGrowth_rpow_absorption {Ψ : ℝ → ℝ} {K p t : ℝ} (hK : 1 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (ht : 1 ≤ t) : t ^ p * Ψ t ≤ Ψ (K ^ ⌈p⌉₊ * t)

Note-facing Step 1: polynomial powers with a real exponent can be absorbed by replacing the exponent with its ceiling.

theorem HCPolySupport.IndependentSums.admissiblePsi_minimalGrowthPre {Ψ : ℝ → ℝ} {K : ℝ} (hK : 1 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (m : ℕ) {t : ℝ} (ht : K ^ m ≤ t) : K ^ natTriangular m ≤ Ψ t

Step 2 pre-estimate from the notes: once t dominates a power of K, the discrete lower bound for Ψ(K^m) propagates to Ψ(t) by monotonicity.

theorem HCPolySupport.IndependentSums.two_mul_natTriangular (n : ℕ) : 2 * natTriangular n = n * (n - 1)

theorem HCPolySupport.IndependentSums.natTriangular_real_eq (n : ℕ) : ↑(natTriangular n) = ↑n * ↑(n - 1) / 2

theorem HCPolySupport.IndependentSums.admissiblePsi_minimalGrowth {Ψ : ℝ → ℝ} {K t : ℝ} (hK : 2 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (ht : K ^ 2 ≤ t) : Real.exp (Real.log t ^ 2 / (9 * Real.log K)) ≤ Ψ t

Step 2 of the Chapter 4 O_Ψ calculus: the growth hypothesis forces at least log-squared growth of Ψ.

theorem HCPolySupport.IndependentSums.admissiblePsi_ratioLowerBound_pow_natTriangular {Ψ : ℝ → ℝ} {K t : ℝ} (hK : 1 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (ht : 1 ≤ t) (m : ℕ) : K ^ natTriangular m ≤ Ψ (t * K ^ m) / Ψ t

Discrete lower bounds for the normalized ratio Ψ(t K^m) / Ψ(t).

theorem HCPolySupport.IndependentSums.admissiblePsi_ratioMinimalGrowthPre {Ψ : ℝ → ℝ} {K t : ℝ} (hK : 1 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (ht : 1 ≤ t) (m : ℕ) {s : ℝ} (hs : K ^ m ≤ s) : K ^ natTriangular m ≤ Ψ (t * s) / Ψ t

The discrete ratio lower bound extends from K^m to every larger s by monotonicity of Ψ.

theorem HCPolySupport.IndependentSums.admissiblePsi_ratioMinimalGrowth {Ψ : ℝ → ℝ} {K t s : ℝ} (hK : 2 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (ht : 1 ≤ t) (hs : K ^ 2 ≤ s) : Real.exp (Real.log s ^ 2 / (9 * Real.log K)) ≤ Ψ (t * s) / Ψ t

The log-squared minimal-growth bound for the normalized ratio Ψ(ts) / Ψ(t).

theorem HCPolySupport.IndependentSums.admissiblePsi_doubling {Ψ : ℝ → ℝ} {K q t s : ℝ} (hK : 2 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (hq : 2 ≤ q) (ht : 1 ≤ t) (hs : 1 ≤ s) : s ^ q ≤ K ^ (3 * q ^ 2) * (Ψ (t * s) / Ψ t)

Step 4 in the Chapter 4 proof: the growth condition implies a doubling estimate for Ψ.

theorem HCPolySupport.IndependentSums.admissiblePsi_hasPsiAbstractDoubling {Ψ : ℝ → ℝ} {K q : ℝ} (hK : 2 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) (hq : 2 ≤ q) : HasPsiAbstractDoubling Ψ q (K ^ (3 * q ^ 2))

theorem HCPolySupport.IndependentSums.admissiblePsi_hasPsiAbstractDoubling_two {Ψ : ℝ → ℝ} {K : ℝ} (hK : 2 ≤ K) (hΨ : HasPsiGrowth Ψ K) (hAdmissible : AdmissiblePsi Ψ) : HasPsiAbstractDoubling Ψ 2 (K ^ 12)

theorem HCPolySupport.IndependentSums.hasPsiAbstractDoubling_one_le_const {Ψ : ℝ → ℝ} {q C₀ : ℝ} (hD : HasPsiAbstractDoubling Ψ q C₀) (hAdmissible : AdmissiblePsi Ψ) : 1 ≤ C₀

Under the abstract doubling hypothesis, the doubling constant is at least 1.

theorem HCPolySupport.IndependentSums.hasPsiAbstractDoubling_inv_mul_le {Ψ : ℝ → ℝ} {q C₀ u v : ℝ} (hD : HasPsiAbstractDoubling Ψ q C₀) (hAdmissible : AdmissiblePsi Ψ) (hu : 1 ≤ u) (hv : 1 ≤ v) : (Ψ (u * v))⁻¹ ≤ C₀ * v ^ (-q) * (Ψ u)⁻¹

Step 5 helper: the abstract doubling estimate can be rewritten as an upper bound on the inverse tail profile.

theorem HCPolySupport.IndependentSums.hasPsiAbstractDoubling_scaledInvTail {Ψ : ℝ → ℝ} {q C₀ a t s : ℝ} (hD : HasPsiAbstractDoubling Ψ q C₀) (hAdmissible : AdmissiblePsi Ψ) (ha : 0 < a) (ht : 2 ≤ t) (hs : t * a / 2 ≤ s) : (Ψ (s / a))⁻¹ ≤ C₀ * (Ψ (t / 2))⁻¹ * (2 * s / (a * t)) ^ (-q)

Note-facing Step 5 helper: specialize abstract doubling to the tail profile s ↦ Ψ (s / a)⁻¹ on the half-line s ≥ ta / 2.

theorem HCPolySupport.IndependentSums.integral_Ioi_div_rpow_neg {q c : ℝ} (hq : 1 < q) (hc : 0 < c) : ∫ (s : ℝ) in Set.Ioi c, (s / c) ^ (-q) = c / (q - 1)

The power-tail integral appearing in Step 5 of the Chapter 4 generalized triangle inequality proof.

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

A concrete growth constant for the stretched-exponential model class Γ_σ, chosen so that the Chapter 4 growth hypothesis holds for every σ > 0.

Equations

• HCPolySupport.IndependentSums.gammaGrowthConst σ = max 2 ((1 + σ⁻¹) ^ σ⁻¹)

theorem HCPolySupport.IndependentSums.two_le_gammaGrowthConst (σ : ℝ) : 2 ≤ gammaGrowthConst σ

theorem HCPolySupport.IndependentSums.hasPsiGrowth_gammaSigma {σ : ℝ} (hσ : 0 < σ) : HasPsiGrowth (gammaSigma σ) (gammaGrowthConst σ)

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

The explicit Chapter 4 growth constant for the log-normal model class Ψ_σ.

Equations

• HCPolySupport.IndependentSums.psiGrowthConst σ = 2 * Real.exp (2 * σ ^ 2)

theorem HCPolySupport.IndependentSums.two_le_psiGrowthConst (σ : ℝ) : 2 ≤ psiGrowthConst σ

theorem HCPolySupport.IndependentSums.hasPsiGrowth_psiSigma {σ : ℝ} (hσ : 1 ≤ σ) : HasPsiGrowth (psiSigma σ) (psiGrowthConst σ)