High-contrast homogenization: Provider.Response.PreYoungProjectionFatou

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Passing uniform projected bounds to a limiting observable

Fatou's lemma transfers a common bound for measurable approximating observables to their almost-everywhere limit. An integrable real limit then has an expectation bounded by the same extended-nonnegative constant.

Finite normalized averages

theorem HCPolySupport.HighContrast.Response.integral_avsum_eq_avsum_integral {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (Z : Finset ι) (F : ι → α → ℝ) (hF : ∀ z ∈ Z, MeasureTheory.Integrable (F z) μ) : ∫ (a : α), avsum Z fun (z : ι) => F z a ∂μ = avsum Z fun (z : ι) => ∫ (a : α), F z a ∂μ

Integration commutes with a finite normalized average of integrable observables.

theorem HCPolySupport.HighContrast.Response.tendsto_avsum {ι : Type u_1} (Z : Finset ι) (F : ℕ → ι → ℝ) (f : ι → ℝ) (hF : ∀ z ∈ Z, Filter.Tendsto (fun (n : ℕ) => F n z) Filter.atTop (nhds (f z))) : Filter.Tendsto (fun (n : ℕ) => avsum Z fun (z : ι) => F n z) Filter.atTop (nhds (avsum Z f))

A finite normalized average preserves pointwise convergence.

theorem HCPolySupport.HighContrast.Response.aemeasurable_avsum {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (Z : Finset ι) (F : ι → α → ℝ) (hF : ∀ z ∈ Z, AEMeasurable (F z) μ) : AEMeasurable (fun (a : α) => avsum Z fun (z : ι) => F z a) μ

A finite normalized average of almost-everywhere measurable observables is almost-everywhere measurable.

Fatou passage

theorem HCPolySupport.HighContrast.Response.lintegral_ofReal_abs_le_of_tendsto_of_uniform_bound {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℕ → α → ℝ} {f : α → ℝ} {B : ENNReal} (hF : ∀ (n : ℕ), AEMeasurable (F n) μ) (hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a))) (hbound : ∀ (n : ℕ), ∫⁻ (a : α), ENNReal.ofReal |F n a| ∂μ ≤ B) : ∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ ≤ B

A uniform bound for the absolute lower integrals of a sequence passes to an almost-everywhere pointwise limit.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_integral_le_of_tendsto_of_uniform_bound {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℕ → α → ℝ} {f : α → ℝ} {B : ENNReal} (hF : ∀ (n : ℕ), AEMeasurable (F n) μ) (hf : MeasureTheory.Integrable f μ) (hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a))) (hbound : ∀ (n : ℕ), ∫⁻ (a : α), ENNReal.ofReal |F n a| ∂μ ≤ B) : ENNReal.ofReal |∫ (a : α), f a ∂μ| ≤ B

An integrable limiting observable inherits the common bound for the expectations of a pointwise convergent sequence.