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

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

noncomputable def HCPolySupport.IndependentSums.centeredFinsetSum {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] (X : ι → Ω → ℝ) (μ : MeasureTheory.Measure Ω) (s : Finset ι) : Ω → ℝ

The centered finite sum ∑ (Xᵢ - E[Xᵢ]) attached to a family X.

Equations

• HCPolySupport.IndependentSums.centeredFinsetSum X μ s ω = ∑ i ∈ s, (X i ω - ∫ (x : Ω), X i x ∂μ)

def HCPolySupport.IndependentSums.symmetrizedFinsetSum {Ω : Type u_1} {ι : Type u_2} (X : ι → Ω → ℝ) (s : Finset ι) : Ω × Ω → ℝ

The symmetrized finite sum ∑ (Xᵢ(ω₁) - Xᵢ(ω₂)) on the product space.

Equations

• HCPolySupport.IndependentSums.symmetrizedFinsetSum X s ω = ∑ i ∈ s, (X i ω.1 - X i ω.2)

noncomputable def HCPolySupport.IndependentSums.absTailIndicator {Ω : Type u_1} (X : Ω → ℝ) (r : ℝ) : Ω → ℝ

The signed absolute-tail piece X 1_{|X| > r} used in the Rosenthal truncation argument.

Equations

• HCPolySupport.IndependentSums.absTailIndicator X r ω = if r < |X ω| then X ω else 0

noncomputable def HCPolySupport.IndependentSums.absTruncation {Ω : Type u_1} (X : Ω → ℝ) (r : ℝ) : Ω → ℝ

The bounded truncation X - X 1_{|X| > r}.

Equations

• HCPolySupport.IndependentSums.absTruncation X r ω = X ω - HCPolySupport.IndependentSums.absTailIndicator X r ω

@[simp]

theorem HCPolySupport.IndependentSums.absTailIndicator_apply {Ω : Type u_1} (X : Ω → ℝ) (r : ℝ) (ω : Ω) : absTailIndicator X r ω = if r < |X ω| then X ω else 0

@[simp]

theorem HCPolySupport.IndependentSums.absTruncation_apply {Ω : Type u_1} (X : Ω → ℝ) (r : ℝ) (ω : Ω) : absTruncation X r ω = X ω - absTailIndicator X r ω

theorem HCPolySupport.IndependentSums.absTailIndicator_of_lt_abs {Ω : Type u_1} {X : Ω → ℝ} {r : ℝ} {ω : Ω} (h : r < |X ω|) : absTailIndicator X r ω = X ω

theorem HCPolySupport.IndependentSums.absTailIndicator_of_not_lt_abs {Ω : Type u_1} {X : Ω → ℝ} {r : ℝ} {ω : Ω} (h : ¬r < |X ω|) : absTailIndicator X r ω = 0

theorem HCPolySupport.IndependentSums.absTruncation_add_absTailIndicator {Ω : Type u_1} (X : Ω → ℝ) (r : ℝ) : absTruncation X r + absTailIndicator X r = X

theorem HCPolySupport.IndependentSums.abs_absTailIndicator_le {Ω : Type u_1} {X : Ω → ℝ} {r : ℝ} (ω : Ω) : |absTailIndicator X r ω| ≤ |X ω|

theorem HCPolySupport.IndependentSums.absTruncation_of_abs_le {Ω : Type u_1} {X : Ω → ℝ} {r : ℝ} {ω : Ω} (h : |X ω| ≤ r) : absTruncation X r ω = X ω

theorem HCPolySupport.IndependentSums.absTruncation_of_lt_abs {Ω : Type u_1} {X : Ω → ℝ} {r : ℝ} {ω : Ω} (h : r < |X ω|) : absTruncation X r ω = 0

theorem HCPolySupport.IndependentSums.abs_absTruncation_le {Ω : Type u_1} {X : Ω → ℝ} {r : ℝ} (hr : 0 ≤ r) (ω : Ω) : |absTruncation X r ω| ≤ r

theorem HCPolySupport.IndependentSums.absTailIndicator_measurable {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {r : ℝ} (hX : Measurable X) : Measurable (absTailIndicator X r)

theorem HCPolySupport.IndependentSums.absTruncation_measurable {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {r : ℝ} (hX : Measurable X) : Measurable (absTruncation X r)

theorem HCPolySupport.IndependentSums.integrable_absTailIndicator_of_integrable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {r : ℝ} (hX_meas : Measurable X) (hX_int : MeasureTheory.Integrable X μ) : MeasureTheory.Integrable (absTailIndicator X r) μ

theorem HCPolySupport.IndependentSums.integrable_absTruncation_of_integrable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {r : ℝ} (hX_meas : Measurable X) (hX_int : MeasureTheory.Integrable X μ) : MeasureTheory.Integrable (absTruncation X r) μ

noncomputable def HCPolySupport.IndependentSums.absTailIndicatorFinsetSum {Ω : Type u_1} {ι : Type u_2} (X : ι → Ω → ℝ) (r : ι → ℝ) (s : Finset ι) : Ω → ℝ

The finite sum of signed absolute-tail pieces.

Equations

• HCPolySupport.IndependentSums.absTailIndicatorFinsetSum X r s ω = ∑ i ∈ s, HCPolySupport.IndependentSums.absTailIndicator (X i) (r i) ω

noncomputable def HCPolySupport.IndependentSums.absTruncationFinsetSum {Ω : Type u_1} {ι : Type u_2} (X : ι → Ω → ℝ) (r : ι → ℝ) (s : Finset ι) : Ω → ℝ

The finite sum of bounded absolute-truncation pieces.

Equations

• HCPolySupport.IndependentSums.absTruncationFinsetSum X r s ω = ∑ i ∈ s, HCPolySupport.IndependentSums.absTruncation (X i) (r i) ω

theorem HCPolySupport.IndependentSums.absTruncationFinsetSum_add_absTailIndicatorFinsetSum {Ω : Type u_1} {ι : Type u_2} (X : ι → Ω → ℝ) (r : ι → ℝ) (s : Finset ι) : absTruncationFinsetSum X r s + absTailIndicatorFinsetSum X r s = fun (ω : Ω) => ∑ i ∈ s, X i ω

theorem HCPolySupport.IndependentSums.abs_absTruncationFinsetSum_le_sum {Ω : Type u_1} {ι : Type u_2} {X : ι → Ω → ℝ} {r : ι → ℝ} {s : Finset ι} (hr : ∀ i ∈ s, 0 ≤ r i) (ω : Ω) : |absTruncationFinsetSum X r s ω| ≤ ∑ i ∈ s, r i

theorem HCPolySupport.IndependentSums.absTailIndicatorFinsetSum_measurable {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {X : ι → Ω → ℝ} {r : ι → ℝ} {s : Finset ι} (hX : ∀ i ∈ s, Measurable (X i)) : Measurable (absTailIndicatorFinsetSum X r s)

theorem HCPolySupport.IndependentSums.absTruncationFinsetSum_measurable {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {X : ι → Ω → ℝ} {r : ι → ℝ} {s : Finset ι} (hX : ∀ i ∈ s, Measurable (X i)) : Measurable (absTruncationFinsetSum X r s)

noncomputable def HCPolySupport.IndependentSums.centeredAbsTruncationFamily {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] (X : ι → Ω → ℝ) (r : ι → ℝ) (μ : MeasureTheory.Measure Ω) : ι → Ω → ℝ

The centered bounded-truncation family used in the Rosenthal proof.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.IndependentSums.centeredAbsTruncationFamily_apply {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] (X : ι → Ω → ℝ) (r : ι → ℝ) (μ : MeasureTheory.Measure Ω) (i : ι) (ω : Ω) : centeredAbsTruncationFamily X r μ i ω = absTruncation (X i) (r i) ω - ∫ (x : Ω), absTruncation (X i) (r i) x ∂μ

theorem HCPolySupport.IndependentSums.centeredAbsTruncationFamily_measurable {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {r : ι → ℝ} (hX : ∀ (i : ι), Measurable (X i)) (i : ι) : Measurable (centeredAbsTruncationFamily X r μ i)

theorem HCPolySupport.IndependentSums.centeredAbsTruncationFamily_iIndepFun {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {r : ι → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) : ProbabilityTheory.iIndepFun (centeredAbsTruncationFamily X r μ) μ

theorem HCPolySupport.IndependentSums.centeredAbsTruncationFamily_integral_eq_zero {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {r : ι → ℝ} {i : ι} (hXi_meas : Measurable (X i)) (hXi_int : MeasureTheory.Integrable (X i) μ) : ∫ (x : Ω), centeredAbsTruncationFamily X r μ i x ∂μ = 0

theorem HCPolySupport.IndependentSums.sum_centeredAbsTruncationFamily_eq_centeredFinsetSum_absTruncation {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {r : ι → ℝ} {s : Finset ι} : (fun (ω : Ω) => ∑ i ∈ s, centeredAbsTruncationFamily X r μ i ω) = centeredFinsetSum (fun (i : ι) => absTruncation (X i) (r i)) μ s

theorem HCPolySupport.IndependentSums.centeredFinsetSum_eq_absTruncationFinsetSum_add_absTailIndicatorFinsetSum {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {r : ι → ℝ} {s : Finset ι} (hTrunc_int : ∀ i ∈ s, MeasureTheory.Integrable (absTruncation (X i) (r i)) μ) (hTail_int : ∀ i ∈ s, MeasureTheory.Integrable (absTailIndicator (X i) (r i)) μ) : centeredFinsetSum X μ s = fun (ω : Ω) => centeredFinsetSum (fun (i : ι) => absTruncation (X i) (r i)) μ s ω + centeredFinsetSum (fun (i : ι) => absTailIndicator (X i) (r i)) μ s ω

theorem HCPolySupport.IndependentSums.upperTailEvent_add_subset_union {Ω : Type u_1} {X Y : Ω → ℝ} {a b : ℝ} : upperTailEvent (fun (ω : Ω) => X ω + Y ω) (a + b) ⊆ upperTailEvent X a ∪ upperTailEvent Y b

theorem HCPolySupport.IndependentSums.absTailEvent_add_subset_union {Ω : Type u_1} {X Y : Ω → ℝ} {a b : ℝ} : absTailEvent (fun (ω : Ω) => X ω + Y ω) (a + b) ⊆ absTailEvent X a ∪ absTailEvent Y b

theorem HCPolySupport.IndependentSums.absTailEvent_centeredFinsetSum_subset_union {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {r : ι → ℝ} {s : Finset ι} {a b : ℝ} (hTrunc_int : ∀ i ∈ s, MeasureTheory.Integrable (absTruncation (X i) (r i)) μ) (hTail_int : ∀ i ∈ s, MeasureTheory.Integrable (absTailIndicator (X i) (r i)) μ) : absTailEvent (centeredFinsetSum X μ s) (a + b) ⊆ absTailEvent (centeredFinsetSum (fun (i : ι) => absTruncation (X i) (r i)) μ s) a ∪ absTailEvent (centeredFinsetSum (fun (i : ι) => absTailIndicator (X i) (r i)) μ s) b

theorem HCPolySupport.IndependentSums.measureReal_absTailEvent_centeredFinsetSum_le_truncation_add_tail {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ} {r : ι → ℝ} {s : Finset ι} {a b : ℝ} (hTrunc_int : ∀ i ∈ s, MeasureTheory.Integrable (absTruncation (X i) (r i)) μ) (hTail_int : ∀ i ∈ s, MeasureTheory.Integrable (absTailIndicator (X i) (r i)) μ) : μ.real (absTailEvent (centeredFinsetSum X μ s) (a + b)) ≤ μ.real (absTailEvent (centeredFinsetSum (fun (i : ι) => absTruncation (X i) (r i)) μ s) a) + μ.real (absTailEvent (centeredFinsetSum (fun (i : ι) => absTailIndicator (X i) (r i)) μ s) b)

theorem HCPolySupport.IndependentSums.integral_abs_sub_integral_le_two_mul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → ℝ} (hY_int : MeasureTheory.Integrable Y μ) : ∫ (ω : Ω), |Y ω - ∫ (x : Ω), Y x ∂μ| ∂μ ≤ 2 * ∫ (ω : Ω), |Y ω| ∂μ

theorem HCPolySupport.IndependentSums.abs_integral_absTruncation_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {r : ℝ} (hX_meas : Measurable X) (hX_int : MeasureTheory.Integrable X μ) (hr : 0 ≤ r) : |∫ (x : Ω), absTruncation X r x ∂μ| ≤ r

theorem HCPolySupport.IndependentSums.abs_sub_integral_absTruncation_le_two_mul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {r : ℝ} (hX_meas : Measurable X) (hX_int : MeasureTheory.Integrable X μ) (hr : 0 ≤ r) (ω : Ω) : |absTruncation X r ω - ∫ (x : Ω), absTruncation X r x ∂μ| ≤ 2 * r

theorem HCPolySupport.IndependentSums.abs_centeredAbsTruncationFamily_le_two_mul {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {r : ι → ℝ} {i : ι} (hXi_meas : Measurable (X i)) (hXi_int : MeasureTheory.Integrable (X i) μ) (hri : 0 ≤ r i) (ω : Ω) : |centeredAbsTruncationFamily X r μ i ω| ≤ 2 * r i