Coarse-graining support: Support.Book.Ch04.Theorems.ConcentrationAEMeasurable

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

A.e.-measurable concentration bridges

The public independent-sum concentration theorems are stated for measurable summands. Chapter 4 local-test observables are naturally only a.e.-measurable under a law carrier. This file provides the small bridge used by completed-local partition arguments: replace each summand by its measurable representative, use a.e. congruence to preserve independence, and transfer the tail conclusion back.

theorem HCPolySupport.Book.Ch04.measureReal_mono_ae {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s t : Set Ω} (hst : s ≤ᵐ[μ] t) : μ.real s ≤ μ.real t

theorem HCPolySupport.Book.Ch04.isBigOWith_of_ae_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X Y : Ω → ℝ} {A : ℝ} (hX : IsBigOWith μ Ψ X A) (hYX : ∀ᵐ (ω : Ω) ∂μ, Y ω ≤ X ω) : IsBigOWith μ Ψ Y A

theorem HCPolySupport.Book.Ch04.isBigO_congr_ae {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ψ : ℝ → ℝ} {X Y : Ω → ℝ} {A : ℝ} (hXY : X =ᵐ[μ] Y) : IsBigO μ Ψ X A ↔ IsBigO μ Ψ Y A

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_iff_of_map_eq_map {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {σ A : ℝ} {X Y : Ω → ℝ} (hX_meas : Measurable X) (hY_meas : Measurable Y) (hmap : MeasureTheory.Measure.map X μ = MeasureTheory.Measure.map Y μ) : IsBigO μ (gammaSigma σ) X A ↔ IsBigO μ (gammaSigma σ) Y A

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_iff_of_map_eq_map_aemeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {σ A : ℝ} {X Y : Ω → ℝ} (hX_aemeas : AEMeasurable X μ) (hY_aemeas : AEMeasurable Y μ) (hmap : MeasureTheory.Measure.map X μ = MeasureTheory.Measure.map Y μ) : IsBigO μ (gammaSigma σ) X A ↔ IsBigO μ (gammaSigma σ) Y A

theorem HCPolySupport.Book.Ch04.isBigOWith_gammaSigma_iff_of_map_eq_map {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {σ A : ℝ} {X Y : Ω → ℝ} (hX_meas : Measurable X) (hY_meas : Measurable Y) (hmap : MeasureTheory.Measure.map X μ = MeasureTheory.Measure.map Y μ) : IsBigOWith μ (gammaSigma σ) X A ↔ IsBigOWith μ (gammaSigma σ) Y A

theorem HCPolySupport.Book.Ch04.isBigOWith_gammaSigma_iff_of_map_eq_map_aemeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {σ A : ℝ} {X Y : Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hX_aemeas : AEMeasurable X μ) (hY_aemeas : AEMeasurable Y μ) (hmap : MeasureTheory.Measure.map X μ = MeasureTheory.Measure.map Y μ) : IsBigOWith μ (gammaSigma σ) X A ↔ IsBigOWith μ (gammaSigma σ) Y A

theorem HCPolySupport.Book.Ch04.isBigO_finset_sum_of_isBigO_gammaSigma_aemeasurable {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {σ : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hσ : 0 < σ) (hs : s.Nonempty) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) (a i)) (hXm : ∀ (i : ι), AEMeasurable (X i) μ) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (gammaTriangleConst σ * s.sum a)

theorem HCPolySupport.Book.Ch04.isBigO_finsetAverage_of_isBigO_gammaSigma_aemeasurable {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) {X : ι → Ω → ℝ} {a : ι → ℝ} {σ : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hσ : 0 < σ) (hs : s.Nonempty) (ha : ∀ i ∈ s, 0 < a i) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) (a i)) (hXm : ∀ (i : ι), AEMeasurable (X i) μ) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (gammaTriangleConst σ * ((↑s.card)⁻¹ * s.sum a))

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_finset_sum_of_iIndepFun_of_isBigO_of_integral_eq_zero_aemeasurable {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_aemeas : ∀ (i : ι), AEMeasurable (X i) μ) (hs : s.Nonempty) (hσ₀ : 0 < σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K) (h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (gammaSigmaIndependentSumConst σ * √↑s.card * K)

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_const_of_abs_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {σ A c : ℝ} (hA : 0 ≤ A) (hc : |c| ≤ A) : IsBigO μ (gammaSigma σ) (fun (_ω : Ω) => c) A

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_sub_const_of_abs_const_le_aemeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {σ K M c : ℝ} {X : Ω → ℝ} (hσ : 0 < σ) (hK : 0 < K) (hM : 0 < M) (hX : IsBigO μ (gammaSigma σ) X K) (hXm : AEMeasurable X μ) (hc : |c| ≤ M) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => X ω - c) (gammaTriangleConst σ * (K + M))