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

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

theorem HCPolySupport.IndependentSums.psiSigma_linear_control_of_le_half_log_sq_div {σ l L u : ℝ} (hσ : 1 ≤ σ) (hl_one : l ≤ 1) (hL : 1 ≤ L) (hl : l ≤ 1 / 2 * ((σ ^ 2)⁻¹ * Real.log (1 + σ * L) ^ 2 / L)) (hu : u ∈ Set.Icc 1 L) : l * u ≤ 1 / 2 * Real.log (psiSigma σ u) + Real.exp 2

A fixed-constant local-control lemma for the optimized log-normal parameter choice. The condition is the note-facing admissibility scale l ≲ log Ψ_σ(L) / L; the proof avoids differentiating log(1 + σ t)^2 / t by using Mathlib's monotonicity of log x / sqrt x on [exp 2, ∞), and handles the small range with the additive constant exp 2.

theorem HCPolySupport.IndependentSums.psiSigmaIndependentSumLambda_linear_control {σ R t u : ℝ} (hσ : 1 ≤ σ) (hR : 1 ≤ R) (ht : 1 ≤ t) (hu : u ∈ Set.Icc 1 (psiSigmaIndependentSumCutoff σ R t)) : psiSigmaIndependentSumLambda σ R t * u ≤ 1 / 2 * Real.log (psiSigma σ u) + Real.exp 2

theorem HCPolySupport.IndependentSums.psiSigma_independentSum_parameter_choice {σ R t : ℝ} (hσ : 1 ≤ σ) (hR : 1 ≤ R) (ht : 1 ≤ t) : ∃ (l : ℝ) (L : ℝ) (C : ℝ), 0 ≤ l ∧ l ≤ 1 ∧ 1 ≤ L ∧ 0 ≤ C ∧ (∀ ⦃u : ℝ⦄, u ∈ Set.Icc 1 L → l * u ≤ 1 / 2 * Real.log (psiSigma σ u) + C) ∧ Real.log 2 + ((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2 + Real.log 2) + R * (l ^ 2 * (3 + psiSigmaPolynomialLogControlConst σ C + psiSigmaTailIntegralConst σ)) ≤ l * (psiSigmaIndependentSumConst σ * √R * t) ∧ Real.log (2 * R) + ((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2 + Real.log 2) ≤ (σ ^ 2)⁻¹ * Real.log (1 + σ * L) ^ 2

theorem HCPolySupport.IndependentSums.psiSigma_log_constraint_of_mul_le_const {σ l L C u : ℝ} (hσ : 1 ≤ σ) (hl : 0 ≤ l) (hC : l * L ≤ C) (hu : u ∈ Set.Icc 1 L) : l * u ≤ Real.log (psiSigma σ u) - 4 * Real.log u + Real.log (psiSigmaPolynomialLogControlConst σ C)

theorem HCPolySupport.IndependentSums.two_mul_card_mul_inv_psiSigma_le_exp_neg_of_log_le {σ R L t : ℝ} (hR_pos : 0 < R) (hlog : Real.log (2 * R) + (σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2 ≤ (σ ^ 2)⁻¹ * Real.log (1 + σ * L) ^ 2) : 2 * (R * (psiSigma σ L)⁻¹) ≤ Real.exp (-((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2))

theorem HCPolySupport.IndependentSums.two_mul_card_mul_inv_psiSigma_le_exp_neg_of_log_add_le {σ R L q : ℝ} (hR_pos : 0 < R) (hlog : Real.log (2 * R) + q ≤ (σ ^ 2)⁻¹ * Real.log (1 + σ * L) ^ 2) : 2 * (R * (psiSigma σ L)⁻¹) ≤ Real.exp (-q)

theorem HCPolySupport.IndependentSums.two_mul_exp_neg_add_le_exp_neg_of_log_two_add_le {x y q : ℝ} (h : Real.log 2 + q + y ≤ x) : 2 * Real.exp (-x + y) ≤ Real.exp (-q)

theorem HCPolySupport.IndependentSums.psiSigma_raw_bound_le_exp_neg_of_mgf_and_union_log {σ R l B t D L : ℝ} (hR_pos : 0 < R) (hmgf : Real.log 2 + ((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2 + Real.log 2) + R * (l ^ 2 * D) ≤ l * (B * t)) (hunion : Real.log (2 * R) + ((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2 + Real.log 2) ≤ (σ ^ 2)⁻¹ * Real.log (1 + σ * L) ^ 2) : 2 * Real.exp (-l * (B * t) + R * (l ^ 2 * D)) + 2 * (R * (psiSigma σ L)⁻¹) ≤ Real.exp (-((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2))