Coarse-graining support: Support.Probability.IndependentSums.PsiConcentration.Concentration

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

theorem HCPolySupport.IndependentSums.mgf_upperTruncation_le_one_add_half_mul_sq_mul_absoluteMoment_add_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {l L : ℝ} (hXm : Measurable X) (hXint : MeasureTheory.Integrable X μ) (hXsq : MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ 2) μ) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) (hl : 0 ≤ l) (hL : 0 ≤ L) : ProbabilityTheory.mgf (upperTruncation X L) μ l ≤ 1 + l ^ 2 / 2 * (∫ (ω : Ω), |X ω| ^ 2 ∂μ + ∫ (t : ℝ) in Set.Ioc 0 L, (2 * t + l * t ^ 2) * Real.exp (l * t) * μ.real {ω : Ω | t ≤ X ω})

Taylor plus the nonpositive mean of the truncation gives the one-variable mgf bound in the natural 1 + A form before the note-facing tail estimates are inserted.

theorem HCPolySupport.IndependentSums.mgf_upperTruncation_le_exp_of_integral_abs_sq_add_integral_Ioc_tail_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {l L : ℝ} (hXm : Measurable X) (hXint : MeasureTheory.Integrable X μ) (hXsq : MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ 2) μ) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) (hl : 0 ≤ l) (hL : 0 ≤ L) : ProbabilityTheory.mgf (upperTruncation X L) μ l ≤ Real.exp (l ^ 2 / 2 * (∫ (ω : Ω), |X ω| ^ 2 ∂μ + ∫ (t : ℝ) in Set.Ioc 0 L, (2 * t + l * t ^ 2) * Real.exp (l * t) * μ.real {ω : Ω | t ≤ X ω}))

Exponential form of the one-variable truncated mgf bound. This is the direct input used by the generic Chernoff reduction for sums of truncated variables.

theorem HCPolySupport.IndependentSums.lintegral_abs_sq_le_two_add_two_mul_of_isBigO_of_lintegral_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {CΨ : ℝ} (hXm : Measurable X) (hAdmissible : AdmissiblePsi Ψ) (hCΨ_nonneg : 0 ≤ CΨ) (hCΨ : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / Ψ t) ≤ ENNReal.ofReal CΨ) (hX : IsBigO μ Ψ X 1) : ∫⁻ (ω : Ω), ENNReal.ofReal (|X ω| ^ 2) ∂μ ≤ ENNReal.ofReal (2 + 2 * CΨ)

A symmetric O_Ψ(1) tail bound together with the integrability of t / Ψ(t) controls the second moment. This is the scalar moment estimate used later in the heavy-tail Chernoff argument.

theorem HCPolySupport.IndependentSums.integral_abs_sq_le_two_add_two_mul_of_isBigO_of_lintegral_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {CΨ : ℝ} (hXm : Measurable X) (hAdmissible : AdmissiblePsi Ψ) (hCΨ_nonneg : 0 ≤ CΨ) (hCΨ : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / Ψ t) ≤ ENNReal.ofReal CΨ) (hX : IsBigO μ Ψ X 1) : ∫ (ω : Ω), |X ω| ^ 2 ∂μ ≤ 2 + 2 * CΨ

Real-integral version of lintegral_abs_sq_le_two_add_two_mul_of_isBigO_of_lintegral_tail.

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_finset_sum_le_exp_of_iIndepFun_of_mgf_le_exp {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : ι → Ω → ℝ} {v : ι → ℝ} {s : Finset ι} {a l : ℝ} (h_indep : ProbabilityTheory.iIndepFun Y μ) (h_meas : ∀ (i : ι), Measurable (Y i)) (hl : 0 ≤ l) (h_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * Y i ω)) μ) (hmgf : ∀ i ∈ s, ProbabilityTheory.mgf (Y i) μ l ≤ Real.exp (v i)) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, Y i ω) a) ≤ Real.exp (-l * a + ∑ i ∈ s, v i)

Generic Chernoff reduction for a finite independent family once each one-variable mgf is bounded by exp (vᵢ).

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_finset_sum_upperTruncation_le_exp_of_iIndepFun_of_mgf_le_exp {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {v : ι → ℝ} {s : Finset ι} {a l L : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hl : 0 ≤ l) (hmgf : ∀ i ∈ s, ProbabilityTheory.mgf (upperTruncation (X i) L) μ l ≤ Real.exp (v i)) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, upperTruncation (X i) L ω) a) ≤ Real.exp (-l * a + ∑ i ∈ s, v i)

Chernoff reduction specialized to the one-sided upper truncation min (Xᵢ, L).

theorem HCPolySupport.IndependentSums.upperTruncation_tail_le_exp_of_independent_momentGeneratingFunction {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {a l L v : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hl : 0 ≤ l) (hmgf : ∀ i ∈ s, ProbabilityTheory.mgf (upperTruncation (X i) L) μ l ≤ Real.exp v) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, upperTruncation (X i) L ω) a) ≤ Real.exp (-l * a + ↑s.card * v)

Uniform one-variable mgf bounds produce the expected card(s) factor in the exponent for the truncated sum.

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_le_inv_of_isBigO {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {t : ℝ} (hX : IsBigO μ Ψ X 1) (ht : 1 ≤ t) : μ.real (upperTailEvent X t) ≤ (Ψ t)⁻¹

The symmetric O_Ψ(1) hypothesis immediately controls the one-sided upper tail needed by the truncation split.

theorem HCPolySupport.IndependentSums.integrableOn_integrand_Ioc_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {l L : ℝ} (hl : 0 ≤ l) (hL : 0 ≤ L) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (2 * t + l * t ^ 2) * Real.exp (l * t) * μ.real {ω : Ω | t ≤ X ω}) (Set.Ioc 0 L) MeasureTheory.volume

The natural Set.Ioc 0 L tail integrand is integrable on finite intervals, because the tail factor is bounded by 1 and the polynomial-exponential weight is bounded on [0, L].

theorem HCPolySupport.IndependentSums.integral_Ioc_zero_one_tail_le_exp_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {l : ℝ} (hXm : Measurable X) (hl : 0 ≤ l) (hl1 : l ≤ 1) : ∫ (t : ℝ) in Set.Ioc 0 1, (2 * t + l * t ^ 2) * Real.exp (l * t) * μ.real {ω : Ω | t ≤ X ω} ≤ Real.exp 1

The small interval (0, 1] contributes a universal bounded term to the truncated mgf exponent.

theorem HCPolySupport.IndependentSums.exp_mul_div_psi_le_mul_rpow_neg_four_of_log_constraint {Ψ : ℝ → ℝ} {l L M t : ℝ} (hAdmissible : AdmissiblePsi Ψ) (hM : 1 ≤ M) (ht : t ∈ Set.Icc 1 L) (hconstraint : l * t ≤ Real.log (Ψ t) - 4 * Real.log t + Real.log M) : Real.exp (l * t) / Ψ t ≤ M * t ^ (-4)

The Chapter 4 logarithmic constraint implies the deterministic kernel bound exp (λ t) / Ψ(t) ≤ M t^{-4} on [1, L].

theorem HCPolySupport.IndependentSums.integral_Ioc_one_L_tail_le_two_mul_M_of_isBigO_of_log_constraint {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {l L M : ℝ} (hAdmissible : AdmissiblePsi Ψ) (hX : IsBigO μ Ψ X 1) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hM : 1 ≤ M) (hconstraint : ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 1 L → l * t ≤ Real.log (Ψ t) - 4 * Real.log t + Real.log M) : ∫ (t : ℝ) in Set.Ioc 1 L, (2 * t + l * t ^ 2) * Real.exp (l * t) * μ.real {ω : Ω | t ≤ X ω} ≤ 2 * M

The large interval [1, L] tail contribution is controlled by the deterministic kernel coming from the Chapter 4 logarithmic constraint.

theorem HCPolySupport.IndependentSums.mgf_upperTruncation_le_exp_of_isBigO_of_lintegral_tail_of_log_constraint {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {CΨ l L M : ℝ} (hXm : Measurable X) (hXint : MeasureTheory.Integrable X μ) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) (hAdmissible : AdmissiblePsi Ψ) (hCΨ_nonneg : 0 ≤ CΨ) (hCΨ : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / Ψ t) ≤ ENNReal.ofReal CΨ) (hX : IsBigO μ Ψ X 1) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hL : 1 ≤ L) (hM : 1 ≤ M) (hconstraint : ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 1 L → l * t ≤ Real.log (Ψ t) - 4 * Real.log t + Real.log M) : ProbabilityTheory.mgf (upperTruncation X L) μ l ≤ Real.exp (l ^ 2 * (1 + Real.exp 1 / 2 + M + CΨ))

Exact one-variable truncated mgf estimate under the Chapter 4 admissible weak-Orlicz hypotheses. The constant reflects the currently formalized Set.Ioc 0 1 cleanup term.

theorem HCPolySupport.IndependentSums.mgf_upperTruncation_le_exp_of_isBigO_of_lintegral_tail_of_log_constraint_rounded {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {CΨ l L M : ℝ} (hXm : Measurable X) (hXint : MeasureTheory.Integrable X μ) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) (hAdmissible : AdmissiblePsi Ψ) (hCΨ_nonneg : 0 ≤ CΨ) (hCΨ : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / Ψ t) ≤ ENNReal.ofReal CΨ) (hX : IsBigO μ Ψ X 1) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hL : 1 ≤ L) (hM : 1 ≤ M) (hconstraint : ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 1 L → l * t ≤ Real.log (Ψ t) - 4 * Real.log t + Real.log M) : ProbabilityTheory.mgf (upperTruncation X L) μ l ≤ Real.exp (l ^ 2 * (3 + M + CΨ))

Rounded one-variable truncated mgf estimate with the cleaner constant 3 + M + C_Ψ.

theorem HCPolySupport.IndependentSums.upperTailProbability_finiteSum_le_exp_card_mul_add_card_mul_invPsi {Ω : 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) (hAdmissible : AdmissiblePsi Ψ) (hCΨ_nonneg : 0 ≤ CΨ) (hCΨ : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / Ψ t) ≤ ENNReal.ofReal CΨ) (hX : ∀ i ∈ s, IsBigO μ Ψ (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 (Ψ t) - 4 * Real.log t + Real.log M) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a) ≤ Real.exp (-l * a + ↑s.card * (l ^ 2 * (1 + Real.exp 1 / 2 + M + CΨ))) + ↑s.card * (Ψ L)⁻¹

Generic heavy-tail concentration estimate for centered finite independent families under the Chapter 4 admissibility and logarithmic-kernel hypotheses.

theorem HCPolySupport.IndependentSums.upperTailProbability_finiteSum_le_exp_card_mul_add_card_mul_invPsi_of_invPsi {Ω : 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) (hAdmissible : AdmissiblePsi Ψ) (hCΨ_nonneg : 0 ≤ CΨ) (hCΨ : ∫⁻ (t : ℝ) in Set.Ioi 1, ENNReal.ofReal (t / Ψ t) ≤ ENNReal.ofReal CΨ) (hX : ∀ i ∈ s, IsBigO μ Ψ (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 (Ψ 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 * (Ψ L)⁻¹

Rounded generic heavy-tail concentration estimate with the cleaner constant 3 + M + C_Ψ.