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

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

def HCPolySupport.IndependentSums.upperTruncation {Ω : Type u_1} (X : Ω → ℝ) (L : ℝ) : Ω → ℝ

The one-sided bounded truncation min (X, L) used in the Chapter 4 heavy-tail concentration argument.

Equations

• HCPolySupport.IndependentSums.upperTruncation X L ω = min (X ω) L

@[simp]

theorem HCPolySupport.IndependentSums.upperTruncation_apply {Ω : Type u_1} (X : Ω → ℝ) (L : ℝ) (ω : Ω) : upperTruncation X L ω = min (X ω) L

theorem HCPolySupport.IndependentSums.upperTruncation_of_le {Ω : Type u_1} {X : Ω → ℝ} {L : ℝ} {ω : Ω} (h : X ω ≤ L) : upperTruncation X L ω = X ω

theorem HCPolySupport.IndependentSums.upperTruncation_of_lt {Ω : Type u_1} {X : Ω → ℝ} {L : ℝ} {ω : Ω} (h : L < X ω) : upperTruncation X L ω = L

theorem HCPolySupport.IndependentSums.upperTruncation_le_self {Ω : Type u_1} (X : Ω → ℝ) (L : ℝ) (ω : Ω) : upperTruncation X L ω ≤ X ω

theorem HCPolySupport.IndependentSums.upperTruncation_le {Ω : Type u_1} (X : Ω → ℝ) (L : ℝ) (ω : Ω) : upperTruncation X L ω ≤ L

theorem HCPolySupport.IndependentSums.upperTruncation_measurable {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {L : ℝ} (hX : Measurable X) : Measurable (upperTruncation X L)

theorem HCPolySupport.IndependentSums.iIndepFun_upperTruncation {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {L : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) : ProbabilityTheory.iIndepFun (fun (i : ι) (ω : Ω) => upperTruncation (X i) L ω) μ

theorem HCPolySupport.IndependentSums.upperTailEvent_finset_sum_subset_upperTailEvent_finset_sum_upperTruncation_union {Ω : Type u_1} {ι : Type u_2} (s : Finset ι) {X : ι → Ω → ℝ} {L a : ℝ} : upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a ⊆ upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, upperTruncation (X i) L ω) a ∪ ⋃ i ∈ s, upperTailEvent (X i) L

If a finite sum exceeds a, then either the corresponding upper-truncated sum still exceeds a, or one of the summands exceeded the truncation level.

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_finset_sum_le_upperTruncation_add {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (s : Finset ι) {X : ι → Ω → ℝ} {L a : ℝ} : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a) ≤ μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, upperTruncation (X i) L ω) a) + ∑ i ∈ s, μ.real (upperTailEvent (X i) L)

Measure-theoretic form of the basic truncation split used in the Chapter 4 heavy-tail concentration proof.

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_finset_sum_le_upperTruncation_add_card_mul_of_isBigOWith {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X : ι → Ω → ℝ} {s : Finset ι} {L a : ℝ} (hX : ∀ i ∈ s, IsBigOWith μ Ψ (X i) 1) (hL : 1 ≤ L) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a) ≤ μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, upperTruncation (X i) L ω) a) + ↑s.card * (Ψ L)⁻¹

If each summand satisfies the note-facing upper-tail bound with unit scale, the large-value part of the truncation split is bounded by card(s) / Ψ(L).

theorem HCPolySupport.IndependentSums.integrable_exp_mul_of_le_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Y : Ω → ℝ} {l B : ℝ} (hYm : Measurable Y) (hl : 0 ≤ l) (hYB : ∀ (ω : Ω), Y ω ≤ B) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * Y ω)) μ

A measurable random variable bounded above by B has finite exponential moment E[e^{λY}] for every λ ≥ 0 on a finite measure space.

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

The exponential moment of an upper-truncated variable is always defined for nonnegative λ.

theorem HCPolySupport.IndependentSums.exp_mul_le_one_add_mul_add_half_mul_sq_mul_exp_max_zero_of_nonneg {l x : ℝ} (hl : 0 ≤ l) : Real.exp (l * x) ≤ 1 + l * x + l ^ 2 / 2 * x ^ 2 * Real.exp (l * max x 0)

A scaled Taylor-remainder bound for exp (λx) with a global exponential weight on the positive part of x.

theorem HCPolySupport.IndependentSums.integrable_upperTruncation_of_integrable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {L : ℝ} (hXm : Measurable X) (hXint : MeasureTheory.Integrable X μ) : MeasureTheory.Integrable (upperTruncation X L) μ

The upper truncation min (X, L) is integrable whenever X is integrable on a finite measure space.

theorem HCPolySupport.IndependentSums.integral_upperTruncation_le_zero_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {L : ℝ} (hXm : Measurable X) (hXint : MeasureTheory.Integrable X μ) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) : ∫ (ω : Ω), upperTruncation X L ω ∂μ ≤ 0

If X is centered, then its upper truncation min (X, L) has nonpositive expectation.