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

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

theorem HCPolySupport.IndependentSums.psiSigma_log_constraint_of_le {σ l L t : ℝ} (hl : 0 ≤ l) (ht : t ∈ Set.Icc 1 L) : l * t ≤ Real.log (psiSigma σ t) - 4 * Real.log t + Real.log (psiSigmaLogControlConst l L)

The simple logarithmic-control constant satisfies the generic raw truncation-Chernoff log constraint for Ψ_σ on [1, L].

theorem HCPolySupport.IndependentSums.upperTailProbability_finiteSum_le_exp_card_mul_add_card_mul_invPsi_psiSigma {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ a l L CΨ M : ℝ} (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σ : 1 ≤ σ) (hCΨ_nonneg : 0 ≤ CΨ) (hCΨ : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / psiSigma σ t) ≤ ENNReal.ofReal CΨ) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) 1) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hL : 1 ≤ L) (hM : 1 ≤ M) (hconstraint : ∀ i ∈ s, ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 1 L → l * t ≤ Real.log (psiSigma σ t) - 4 * Real.log t + Real.log M) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a) ≤ Real.exp (-l * a + ↑s.card * (l ^ 2 * (3 + M + CΨ))) + ↑s.card * (psiSigma σ L)⁻¹

Raw truncation-Chernoff concentration for independent centered O_{Ψ_σ}(1) summands, with the analytic Ψ_σ tail-integral and logarithmic constraint hypotheses left explicit.

This is the specialization point for the log-normal independent-sum endpoint. The remaining endpoint proof will choose l, L, M, and CΨ as functions of σ, the family size, and the tail parameter, then optimize this raw bound to obtain the clean sqrt(card) weak-Ψ_σ scale.

theorem HCPolySupport.IndependentSums.upperTailProbability_finiteSum_le_exp_card_mul_add_card_mul_invPsi_of_iIndepFun {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K a l L CΨ M : ℝ} (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σ : 1 ≤ σ) (hK : 0 < K) (hCΨ_nonneg : 0 ≤ CΨ) (hCΨ : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / psiSigma σ t) ≤ ENNReal.ofReal CΨ) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hL : 1 ≤ L) (hM : 1 ≤ M) (hconstraint : ∀ i ∈ s, ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 1 L → l * t ≤ Real.log (psiSigma σ t) - 4 * Real.log t + Real.log M) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) (K * a)) ≤ Real.exp (-l * a + ↑s.card * (l ^ 2 * (3 + M + CΨ))) + ↑s.card * (psiSigma σ L)⁻¹

Scaled raw truncation-Chernoff concentration for independent centered O_{Ψ_σ}(K) summands. The conclusion is written at threshold K * a, so the right-hand side is exactly the unit-scale raw bound.

theorem HCPolySupport.IndependentSums.absoluteTailProbability_finiteSum_le_twoExp_add_twoCardInvPsiPsiSigma {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K a l L CΨ M : ℝ} (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σ : 1 ≤ σ) (hK : 0 < K) (hCΨ_nonneg : 0 ≤ CΨ) (hCΨ : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / psiSigma σ t) ≤ ENNReal.ofReal CΨ) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hL : 1 ≤ L) (hM : 1 ≤ M) (hconstraint : ∀ i ∈ s, ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 1 L → l * t ≤ Real.log (psiSigma σ t) - 4 * Real.log t + Real.log M) : μ.real (absTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) (K * a)) ≤ 2 * Real.exp (-l * a + ↑s.card * (l ^ 2 * (3 + M + CΨ))) + 2 * (↑s.card * (psiSigma σ L)⁻¹)

Symmetric raw truncation-Chernoff concentration for independent centered O_{Ψ_σ}(K) summands. This is just the scaled upper-tail estimate applied to X and -X, before the final log-normal absorption step.

theorem HCPolySupport.IndependentSums.absolutePsiSigmaTailProbability_finiteSum_le_expBound_of_logConstraint {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K a l L M : ℝ} (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σ : 1 ≤ σ) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hL : 1 ≤ L) (hM : 1 ≤ M) (hconstraint : ∀ i ∈ s, ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 1 L → l * t ≤ Real.log (psiSigma σ t) - 4 * Real.log t + Real.log M) : μ.real (absTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) (K * a)) ≤ 2 * Real.exp (-l * a + ↑s.card * (l ^ 2 * (3 + M + psiSigmaTailIntegralConst σ))) + 2 * (↑s.card * (psiSigma σ L)⁻¹)

Symmetric raw Ψ_σ concentration with the scalar tail-integral input discharged, but with an arbitrary logarithmic-control constant M. This is the preferred backend for the final optimized log-normal endpoint: the deterministic optimizer can choose M sharply instead of using the simple fallback exp(l L + 4 log L).

theorem HCPolySupport.IndependentSums.absolutePsiSigmaTailProbability_finiteSum_le_expBound_of_simpleLogControl {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K a l L CΨ : ℝ} (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σ : 1 ≤ σ) (hK : 0 < K) (hCΨ_nonneg : 0 ≤ CΨ) (hCΨ : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / psiSigma σ t) ≤ ENNReal.ofReal CΨ) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hL : 1 ≤ L) : μ.real (absTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) (K * a)) ≤ 2 * Real.exp (-l * a + ↑s.card * (l ^ 2 * (3 + psiSigmaLogControlConst l L + CΨ))) + 2 * (↑s.card * (psiSigma σ L)⁻¹)

Symmetric raw Ψ_σ concentration with the simple log-control constant already plugged into the generic log-constraint slot. The only analytic input still explicit is the tail-integral bound for t / Ψ_σ(t).

theorem HCPolySupport.IndependentSums.absolutePsiSigmaTailProbability_finiteSum_le_expBound_of_packagedConstants {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K 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σ : 1 ≤ σ) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hL : 1 ≤ L) : μ.real (absTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) (K * a)) ≤ 2 * Real.exp (-l * a + ↑s.card * (l ^ 2 * (3 + psiSigmaLogControlConst l L + psiSigmaTailIntegralConst σ))) + 2 * (↑s.card * (psiSigma σ L)⁻¹)

Symmetric raw Ψ_σ concentration with both scalar analytic inputs discharged by the packaged log-control and tail-integral constants.

theorem HCPolySupport.IndependentSums.isBigO_finiteSum_psiSigma_of_simpleLogControlAbsorption {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K B : ℝ} (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σ : 1 ≤ σ) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) (h_absorb : ∀ ⦃t : ℝ⦄, 1 ≤ t → ∃ (l : ℝ) (L : ℝ), 0 ≤ l ∧ l ≤ 1 ∧ 1 ≤ L ∧ 2 * Real.exp (-l * (B * t) + ↑s.card * (l ^ 2 * (3 + psiSigmaLogControlConst l L + psiSigmaTailIntegralConst σ))) + 2 * (↑s.card * (psiSigma σ L)⁻¹) ≤ Real.exp (-((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2))) : IsBigO μ (psiSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (B * K)

Scalar independent-sum Ψ_σ endpoint reduced to the remaining deterministic choice of truncation/Chernoff parameters. This isolates the probability part of the log-normal endpoint: after this theorem, the only missing input is the optimization/absorption inequality for the raw bound.

theorem HCPolySupport.IndependentSums.isBigO_finiteSum_psiSigma_of_logConstraintAbsorption {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K B : ℝ} (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σ : 1 ≤ σ) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) (h_absorb : ∀ ⦃t : ℝ⦄, 1 ≤ t → ∃ (l : ℝ) (L : ℝ) (M : ℝ), 0 ≤ l ∧ l ≤ 1 ∧ 1 ≤ L ∧ 1 ≤ M ∧ (∀ i ∈ s, ∀ ⦃u : ℝ⦄, u ∈ Set.Icc 1 L → l * u ≤ Real.log (psiSigma σ u) - 4 * Real.log u + Real.log M) ∧ 2 * Real.exp (-l * (B * t) + ↑s.card * (l ^ 2 * (3 + M + psiSigmaTailIntegralConst σ))) + 2 * (↑s.card * (psiSigma σ L)⁻¹) ≤ Real.exp (-((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2))) : IsBigO μ (psiSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (B * K)

Scalar independent-sum Ψ_σ endpoint reduced to deterministic optimization with an arbitrary logarithmic-control constant. This is the general note-facing staging theorem for the final log-normal scalar endpoint: the probability and analytic tail-integral parts are fully discharged, while the remaining hypothesis is exactly the deterministic parameter choice (l, L, M) and absorption of the raw bound.

theorem HCPolySupport.IndependentSums.isBigO_psiSigma_finset_sum_of_iIndepFun_of_isBigO_scale {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K B : ℝ} (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σ : 1 ≤ σ) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) (h_absorb : ∀ ⦃t : ℝ⦄, 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) ∧ 2 * Real.exp (-l * (B * t) + ↑s.card * (l ^ 2 * (3 + psiSigmaPolynomialLogControlConst σ C + psiSigmaTailIntegralConst σ))) + 2 * (↑s.card * (psiSigma σ L)⁻¹) ≤ Real.exp (-((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2))) : IsBigO μ (psiSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (B * K)

Scalar independent-sum Ψ_σ endpoint reduced to a linear-control parameter choice. The helper four_mul_log_le_half_log_psiSigma_add_const absorbs the polynomial factor in the raw theorem, so the deterministic optimizer only needs to find l, L, C such that l u ≤ (1/2) log Ψ_σ(u) + C on [1,L] and the resulting raw bound is absorbed by the target Ψ_σ tail.

theorem HCPolySupport.IndependentSums.isBigO_psiSigma_finset_sum_of_iIndepFun_of_isBigO_scale_of_iIndepFun {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K B : ℝ} (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) (hs : s.Nonempty) (hσ : 1 ≤ σ) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) (h_absorb : ∀ ⦃t : ℝ⦄, 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) + ↑s.card * (l ^ 2 * (3 + psiSigmaPolynomialLogControlConst σ C + psiSigmaTailIntegralConst σ)) ≤ l * (B * t) ∧ Real.log (2 * ↑s.card) + ((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2 + Real.log 2) ≤ (σ ^ 2)⁻¹ * Real.log (1 + σ * L) ^ 2) : IsBigO μ (psiSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (B * K)

Scalar independent-sum Ψ_σ endpoint reduced to three deterministic logarithmic inequalities: local linear control, mgf-term absorption, and union-term absorption. This is the preferred staging point for the final parameter-choice proof.

theorem HCPolySupport.IndependentSums.isBigO_psiSigma_finset_sum_of_iIndepFun_of_isBigO_scale_of_integral_eq_zero {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (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) (hs : s.Nonempty) (hσ : 1 ≤ σ) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) : IsBigO μ (psiSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (psiSigmaIndependentSumConst σ * √↑s.card * K)

Note-facing scalar independent-sum endpoint for the log-normal class Ψ_σ: centered independent summands with common O_{Ψ_σ} scale K concentrate at the square-root cardinality scale.

theorem HCPolySupport.IndependentSums.isBigO_psiSigma_finsetAverage_of_iIndepFun_of_isBigO_scale_of_integral_eq_zero {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (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) (hs : s.Nonempty) (hσ : 1 ≤ σ) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (psiSigma σ) (X i) K) : IsBigO μ (psiSigma σ) (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (psiSigmaIndependentSumConst σ * (√↑s.card / ↑s.card) * K)

Average version of the log-normal centered independent-sum endpoint.