Comparing test integrals through localized reconstruction

The comparison uses equality on a finite-prefix event and full-sequence convergence on a large good event. All error terms are bounded by measurable indicators.

theorem BGW.StableTrees.PathTail.eventually_abs_integral_sub_le_of_reconstruction_ae {Ω : Type u_1} {Γ : Type u_2} {S : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Γ] [MeasurableSpace S] (P₀ : MeasureTheory.ProbabilityMeasure Ω) (P : MeasureTheory.ProbabilityMeasure Γ) (a : ℕ → Ω → ℝ) (b : ℕ → S → ℝ) (o : ℕ → Ω → S) (Y : ℕ → Γ → S) (z : Γ → ℝ) (ha : ∀ (n : ℕ), Measurable (a n)) (hb : ∀ (n : ℕ), Measurable (b n)) (ho : ∀ (n : ℕ), Measurable (o n)) (hY : ∀ (n : ℕ), Measurable (Y n)) (hz : MeasureTheory.AEStronglyMeasurable z ↑P) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (Y n) ↑P = MeasureTheory.Measure.map (o n) ↑P₀) (E : ℕ → Set S) (hE : ∀ (n : ℕ), MeasurableSet (E n)) (hexact : ∀ (n : ℕ), ∀ᵐ (ω : Ω) ∂↑P₀, o n ω ∈ E n → a n ω = b n (o n ω)) (G : Set Γ) (hG : MeasurableSet G) {C : ℝ} (hC : 0 ≤ C) (haC : ∀ (n : ℕ) (ω : Ω), |a n ω| ≤ C) (hbC : ∀ (n : ℕ) (y : S), |b n y| ≤ C) (hzC : ∀ (p : Γ), |z p| ≤ C) (hconv : ∀ᵐ (p : Γ) ∂↑P, p ∈ G → Filter.Tendsto (fun (n : ℕ) => b n (Y n p)) Filter.atTop (nhds (z p)) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, Y n p ∈ E n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, |∫ (ω : Ω), a n ω ∂↑P₀ - ∫ (p : Γ), z p ∂↑P| < 4 * C * (↑P).real Gᶜ + ε

Scalar integral comparison when reconstruction is almost everywhere exact on observable events and converges on a large good event. The estimate pays four times the test bound on the bad limiting event.

theorem BGW.StableTrees.PathTail.eventually_abs_integral_sub_le_of_reconstruction {Ω : Type u_1} {Γ : Type u_2} {S : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Γ] [MeasurableSpace S] (P₀ : MeasureTheory.ProbabilityMeasure Ω) (P : MeasureTheory.ProbabilityMeasure Γ) (a : ℕ → Ω → ℝ) (b : ℕ → S → ℝ) (o : ℕ → Ω → S) (Y : ℕ → Γ → S) (z : Γ → ℝ) (ha : ∀ (n : ℕ), Measurable (a n)) (hb : ∀ (n : ℕ), Measurable (b n)) (ho : ∀ (n : ℕ), Measurable (o n)) (hY : ∀ (n : ℕ), Measurable (Y n)) (hz : MeasureTheory.AEStronglyMeasurable z ↑P) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (Y n) ↑P = MeasureTheory.Measure.map (o n) ↑P₀) (E : ℕ → Set S) (hE : ∀ (n : ℕ), MeasurableSet (E n)) (hexact : ∀ (n : ℕ) (ω : Ω), o n ω ∈ E n → a n ω = b n (o n ω)) (G : Set Γ) (hG : MeasurableSet G) {C : ℝ} (hC : 0 ≤ C) (haC : ∀ (n : ℕ) (ω : Ω), |a n ω| ≤ C) (hbC : ∀ (n : ℕ) (y : S), |b n y| ≤ C) (hzC : ∀ (p : Γ), |z p| ≤ C) (hconv : ∀ᵐ (p : Γ) ∂↑P, p ∈ G → Filter.Tendsto (fun (n : ℕ) => b n (Y n p)) Filter.atTop (nhds (z p)) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, Y n p ∈ E n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, |∫ (ω : Ω), a n ω ∂↑P₀ - ∫ (p : Γ), z p ∂↑P| < 4 * C * (↑P).real Gᶜ + ε

Scalar integral comparison when reconstruction is exact on observable events and converges on a large good event. The estimate pays four times the test bound on the bad limiting event.