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

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

theorem HCPolySupport.IndependentSums.integral_sq_exp_weight (l s : ℝ) : ∫ (t : ℝ) in 0..s, (2 * t + l * t ^ 2) * Real.exp (l * t) = s ^ 2 * Real.exp (l * s)

Primitive used in the weighted layer-cake estimate for t ↦ t² e^{λt}.

theorem HCPolySupport.IndependentSums.upperTruncation_posPart_tailSet_eq {Ω : Type u_1} {X : Ω → ℝ} {t L : ℝ} (ht : 0 < t) (htL : t ≤ L) : {ω : Ω | t ≤ max (upperTruncation X L ω) 0} = {ω : Ω | t ≤ X ω}

On the positive slice 0 < t ≤ L, the event {t ≤ max(min(X, L), 0)} agrees exactly with {t ≤ X}.

theorem HCPolySupport.IndependentSums.upperTruncation_posPart_le {Ω : Type u_1} {X : Ω → ℝ} {L : ℝ} {ω : Ω} (hL : 0 ≤ L) : max (upperTruncation X L ω) 0 ≤ L

theorem HCPolySupport.IndependentSums.abs_upperTruncation_le_abs_self {Ω : Type u_1} {X : Ω → ℝ} {L : ℝ} {ω : Ω} (hL : 0 ≤ L) : |upperTruncation X L ω| ≤ |X ω|

theorem HCPolySupport.IndependentSums.upperTruncation_sq_mul_exp_max_le_abs_sq_add_posPart_sq_mul_exp {Ω : Type u_1} {X : Ω → ℝ} {l L : ℝ} {ω : Ω} (hL : 0 ≤ L) : upperTruncation X L ω ^ 2 * Real.exp (l * max (upperTruncation X L ω) 0) ≤ |X ω| ^ 2 + max (upperTruncation X L ω) 0 ^ 2 * Real.exp (l * max (upperTruncation X L ω) 0)

theorem HCPolySupport.IndependentSums.integral_upperTruncation_posPart_sq_mul_exp_eq_integral_Ioc_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {l L : ℝ} (hXm : Measurable X) (hl : 0 ≤ l) (hL : 0 ≤ L) : ∫ (ω : Ω), max (upperTruncation X L ω) 0 ^ 2 * Real.exp (l * max (upperTruncation X L ω) 0) ∂μ = ∫ (t : ℝ) in Set.Ioc 0 L, (2 * t + l * t ^ 2) * Real.exp (l * t) * μ.real {ω : Ω | t ≤ X ω}

Layer-cake identity for the weighted positive part of the upper truncation max(min(X, L), 0). This is the natural Set.Ioc 0 L version that precedes the note-facing [1, L] estimate.

theorem HCPolySupport.IndependentSums.integrable_upperTruncation_posPart_sq_mul_exp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {l L : ℝ} (hXm : Measurable X) (hl : 0 ≤ l) (hL : 0 ≤ L) : MeasureTheory.Integrable (fun (ω : Ω) => max (upperTruncation X L ω) 0 ^ 2 * Real.exp (l * max (upperTruncation X L ω) 0)) μ

The weighted positive-part term in the heavy-tail Taylor remainder is integrable on a finite measure space because max(min(X, L), 0) is bounded by L.

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

The weighted truncation term is controlled by the square moment of X plus the weighted positive-part term, hence by the natural Set.Ioc 0 L tail integral from the layer-cake formula.

theorem HCPolySupport.IndependentSums.integrable_upperTruncation_sq_mul_exp_max_of_integrable_abs_sq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {l L : ℝ} (hXm : Measurable X) (hXsq : MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ 2) μ) (hl : 0 ≤ l) (hL : 0 ≤ L) : MeasureTheory.Integrable (fun (ω : Ω) => upperTruncation X L ω ^ 2 * Real.exp (l * max (upperTruncation X L ω) 0)) μ

The full weighted truncation term is integrable once |X|² is integrable, because it is pointwise dominated by |X|² plus the bounded positive-part weight.