English
A bounded convergence theorem in the bounded-norm setting: if fs ≤ c and fs → f pointwise, then μ.testAgainstNN (fs) → μ.testAgainstNN f.
Русский
Сходимость в ограниченном нормировании: если fs ≤ c и fs сходится к f по точкам, то μ.testAgainstNN (fs) → μ.testAgainstNN f.
LaTeX
$$$ \text{tendsto}_{i} \; μ.testAgainstNN (fs_i) \; F \; (nhds (μ.testAgainstNN f)) $ under appropriate hypotheses.$$
Lean4
/-- A bounded convergence theorem for a finite measure:
If bounded continuous non-negative functions are uniformly bounded by a constant and tend to a
limit, then their integrals against the finite measure tend to the integral of the limit.
This formulation assumes:
* the functions tend to a limit along a countably generated filter;
* the limit is in the almost everywhere sense;
* boundedness holds almost everywhere;
* integration is the pairing against non-negative continuous test functions
(`MeasureTheory.FiniteMeasure.testAgainstNN`).
A related result using `MeasureTheory.lintegral` for integration is
`MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_filter_of_le_const`.
-/
theorem tendsto_testAgainstNN_filter_of_le_const {ι : Type*} {L : Filter ι} [L.IsCountablyGenerated]
{μ : FiniteMeasure Ω} {fs : ι → Ω →ᵇ ℝ≥0} {c : ℝ≥0} (fs_le_const : ∀ᶠ i in L, ∀ᵐ ω : Ω ∂(μ : Measure Ω), fs i ω ≤ c)
{f : Ω →ᵇ ℝ≥0} (fs_lim : ∀ᵐ ω : Ω ∂(μ : Measure Ω), Tendsto (fun i ↦ fs i ω) L (𝓝 (f ω))) :
Tendsto (fun i ↦ μ.testAgainstNN (fs i)) L (𝓝 (μ.testAgainstNN f)) :=
by
apply (ENNReal.tendsto_toNNReal (f.lintegral_lt_top_of_nnreal (μ : Measure Ω)).ne).comp
exact tendsto_lintegral_nn_filter_of_le_const (Ω := Ω) μ fs_le_const fs_lim
