Coarse-graining support: Support.Probability.IndependentSums.PsiSigma.TailAndLogControl

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

theorem HCPolySupport.IndependentSums.integrableOn_Ioi_one_psiSigma_tail_integrand {σ : ℝ} (hσ : 1 ≤ σ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t / psiSigma σ t) (Set.Ioi 1) MeasureTheory.volume

The log-normal tail-integral kernel is integrable on (1, ∞) for σ ≥ 1. The proof is intentionally non-sharp: after the cutoff exp(3 σ^2), Ψ_σ(t) dominates t^3, so the kernel is bounded by t⁻².

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

A non-sharp finite constant for the Ψ_σ analytic tail-integral input.

Equations

• HCPolySupport.IndependentSums.psiSigmaTailIntegralConst σ = (∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / HCPolySupport.IndependentSums.psiSigma σ t)).toReal

theorem HCPolySupport.IndependentSums.psiSigmaTailIntegralConst_nonneg (σ : ℝ) : 0 ≤ psiSigmaTailIntegralConst σ

theorem HCPolySupport.IndependentSums.lintegral_Ioi_one_psiSigma_le_psiSigmaTailIntegralConst {σ : ℝ} (hσ : 1 ≤ σ) : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / psiSigma σ t) ≤ ENNReal.ofReal (psiSigmaTailIntegralConst σ)

Note-facing discharge of the analytic Ψ_σ tail-integral hypothesis.

noncomputable def HCPolySupport.IndependentSums.psiSigmaLogControlConst (l L : ℝ) : ℝ

A simple non-sharp logarithmic-control constant for the raw Ψ_σ truncation-Chernoff theorem on the interval [1, L]. It is intentionally allowed to depend on the Chernoff parameter l and cutoff L; later endpoint optimization can replace this with a sharper σ-dependent package.

Equations

• HCPolySupport.IndependentSums.psiSigmaLogControlConst l L = Real.exp (l * L + 4 * Real.log L)

theorem HCPolySupport.IndependentSums.one_le_psiSigmaLogControlConst {l L : ℝ} (hl : 0 ≤ l) (hL : 1 ≤ L) : 1 ≤ psiSigmaLogControlConst l L

noncomputable def HCPolySupport.IndependentSums.psiSigmaPolynomialLogControlConst (σ C : ℝ) : ℝ

A sharper reusable logarithmic-control constant for the optimized Ψ_σ endpoint. If the optimizer can prove l t ≤ (1/2) log Ψ_σ(t) + C, this constant absorbs the remaining polynomial factor t^4 in the raw Chernoff theorem.

Equations

• HCPolySupport.IndependentSums.psiSigmaPolynomialLogControlConst σ C = Real.exp (C + 8 * σ ^ 2)

noncomputable def HCPolySupport.IndependentSums.psiSigmaLogExponent (σ t : ℝ) : ℝ

The logarithmic tail exponent log(1 + σ t)² / σ².

Equations

• HCPolySupport.IndependentSums.psiSigmaLogExponent σ t = (σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2

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

The raw independent-sum constant combining 3, the polynomial-log control at exp(2), and the tail-integral constant.

Equations

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

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

The independent-sum normalization constant 128 exp(σ² / 2) times the square root of the raw constant.

Equations

• HCPolySupport.IndependentSums.psiSigmaIndependentSumConst σ = 128 * Real.exp (σ ^ 2 / 2) * √(HCPolySupport.IndependentSums.psiSigmaIndependentSumRawConst σ)

noncomputable def HCPolySupport.IndependentSums.psiSigmaIndependentSumCutoff (σ R t : ℝ) : ℝ

The truncation threshold ((1 + σ t) exp(σ sqrt(log(4R))) - 1) / σ used for independent sums.

Equations

• HCPolySupport.IndependentSums.psiSigmaIndependentSumCutoff σ R t = ((1 + σ * t) * Real.exp (σ * √(Real.log (4 * R))) - 1) / σ

noncomputable def HCPolySupport.IndependentSums.psiSigmaIndependentSumLambda (σ R t : ℝ) : ℝ

The exponential-moment parameter 4(log(1 + σ t)² / σ² + log 2) divided by the sum constant times sqrt(R) t.

Equations

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

theorem HCPolySupport.IndependentSums.one_le_psiSigmaPolynomialLogControlConst {σ C : ℝ} (hC : 0 ≤ C) : 1 ≤ psiSigmaPolynomialLogControlConst σ C

theorem HCPolySupport.IndependentSums.one_le_psiSigmaIndependentSumRawConst (σ : ℝ) : 1 ≤ psiSigmaIndependentSumRawConst σ

theorem HCPolySupport.IndependentSums.psiSigmaIndependentSumRawConst_pos (σ : ℝ) : 0 < psiSigmaIndependentSumRawConst σ

theorem HCPolySupport.IndependentSums.psiSigmaIndependentSumConst_pos (σ : ℝ) : 0 < psiSigmaIndependentSumConst σ

theorem HCPolySupport.IndependentSums.one_add_mul_psiSigmaIndependentSumCutoff {σ R t : ℝ} (hσ : σ ≠ 0) : 1 + σ * psiSigmaIndependentSumCutoff σ R t = (1 + σ * t) * Real.exp (σ * √(Real.log (4 * R)))

theorem HCPolySupport.IndependentSums.one_le_psiSigmaIndependentSumCutoff {σ R t : ℝ} (hσ : 1 ≤ σ) (hR : 1 ≤ R) (ht : 1 ≤ t) : 1 ≤ psiSigmaIndependentSumCutoff σ R t

theorem HCPolySupport.IndependentSums.psiSigmaIndependentSumCutoff_union_log {σ R t : ℝ} (hσ : 1 ≤ σ) (hR : 1 ≤ R) (ht : 1 ≤ t) : Real.log (2 * R) + ((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2 + Real.log 2) ≤ (σ ^ 2)⁻¹ * Real.log (1 + σ * psiSigmaIndependentSumCutoff σ R t) ^ 2

theorem HCPolySupport.IndependentSums.exp_mul_sqrt_log_four_mul_le {σ R : ℝ} (hσ : 1 ≤ σ) (hR : 1 ≤ R) : Real.exp (σ * √(Real.log (4 * R))) ≤ 2 * Real.exp (σ ^ 2 / 2) * √R

theorem HCPolySupport.IndependentSums.psiSigmaIndependentSumCutoff_le_four_mul_exp_mul_sqrt_mul {σ R t : ℝ} (hσ : 1 ≤ σ) (hR : 1 ≤ R) (ht : 1 ≤ t) : psiSigmaIndependentSumCutoff σ R t ≤ 4 * Real.exp (σ ^ 2 / 2) * √R * t

theorem HCPolySupport.IndependentSums.eight_mul_psiSigmaIndependentSumCutoff_le_const_mul_sqrt_mul {σ R t : ℝ} (hσ : 1 ≤ σ) (hR : 1 ≤ R) (ht : 1 ≤ t) : 8 * psiSigmaIndependentSumCutoff σ R t ≤ psiSigmaIndependentSumConst σ * √R * t

theorem HCPolySupport.IndependentSums.four_mul_log_le_half_log_psiSigma_add_const {σ t : ℝ} (hσ : 1 ≤ σ) (ht : 1 ≤ t) : 4 * Real.log t ≤ 1 / 2 * Real.log (psiSigma σ t) + 8 * σ ^ 2

theorem HCPolySupport.IndependentSums.log_sq_le_four_mul_self_of_one_le {x : ℝ} (hx : 1 ≤ x) : Real.log x ^ 2 ≤ 4 * x

theorem HCPolySupport.IndependentSums.psiSigma_log_exponent_le_eight_mul_self {σ t : ℝ} (hσ : 1 ≤ σ) (ht : 1 ≤ t) : (σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2 ≤ 8 * t

theorem HCPolySupport.IndependentSums.psiSigma_log_exponent_add_log_two_le_nine_mul_self {σ t : ℝ} (hσ : 1 ≤ σ) (ht : 1 ≤ t) : (σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2 + Real.log 2 ≤ 9 * t

theorem HCPolySupport.IndependentSums.psiSigmaIndependentSumLambda_nonneg {σ R t : ℝ} (_hσ : 1 ≤ σ) (hR : 1 ≤ R) (ht : 1 ≤ t) : 0 ≤ psiSigmaIndependentSumLambda σ R t

theorem HCPolySupport.IndependentSums.psiSigmaIndependentSumLambda_le_one {σ R t : ℝ} (hσ : 1 ≤ σ) (hR : 1 ≤ R) (ht : 1 ≤ t) : psiSigmaIndependentSumLambda σ R t ≤ 1

theorem HCPolySupport.IndependentSums.psiSigmaIndependentSumLambda_le_half_cutoff_logExponent_div {σ R t : ℝ} (hσ : 1 ≤ σ) (hR : 1 ≤ R) (ht : 1 ≤ t) : psiSigmaIndependentSumLambda σ R t ≤ 1 / 2 * (psiSigmaLogExponent σ (psiSigmaIndependentSumCutoff σ R t) / psiSigmaIndependentSumCutoff σ R t)

theorem HCPolySupport.IndependentSums.psiSigmaIndependentSumLambda_mgf_log {σ R t : ℝ} (hσ : 1 ≤ σ) (hR : 1 ≤ R) (ht : 1 ≤ t) : Real.log 2 + (psiSigmaLogExponent σ t + Real.log 2) + R * (psiSigmaIndependentSumLambda σ R t ^ 2 * psiSigmaIndependentSumRawConst σ) ≤ psiSigmaIndependentSumLambda σ R t * (psiSigmaIndependentSumConst σ * √R * t)

theorem HCPolySupport.IndependentSums.psiSigma_log_constraint_of_linear_control {σ l L C u : ℝ} (hσ : 1 ≤ σ) (hu : u ∈ Set.Icc 1 L) (hlinear : ∀ ⦃v : ℝ⦄, v ∈ Set.Icc 1 L → l * v ≤ 1 / 2 * Real.log (psiSigma σ v) + C) : l * u ≤ Real.log (psiSigma σ u) - 4 * Real.log u + Real.log (psiSigmaPolynomialLogControlConst σ C)

Turn a local linear-control estimate into the generic logarithmic constraint needed by the raw Ψ_σ Chernoff theorem.

theorem HCPolySupport.IndependentSums.psiSigma_linear_control_of_mul_le_const {σ l L C u : ℝ} (hl : 0 ≤ l) (hC : l * L ≤ C) (hu : u ∈ Set.Icc 1 L) : l * u ≤ 1 / 2 * Real.log (psiSigma σ u) + C