English
There is a convergent behavior of lintegral under convergence of measures: Tendsto μs F (nhds μ) iff Tendsto (fun i => ∫⁻ f ∂ μs i) F (nhds (∫⁻ f ∂ μ)).
Русский
Сходимость мер эквивалентна сходимости интегралов по линтигралу.
LaTeX
$$$ \text{Tendsto } μ_s F (\mathsf{nhds} μ) \iff \forall f : Ω \to^{} ℝ_{\ge 0}, \; \text{Tendsto } (i \mapsto \int⁻ f x ∂(μ_s i : \text{Measure } Ω)) F (\mathsf{nhds} (\int⁻ f x ∂(μ : \text{Measure } Ω))). $$$
Lean4
/-- A bounded convergence theorem for a finite measure:
If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant and
tend pointwise to a limit, then their integrals (`MeasureTheory.FiniteMeasure.testAgainstNN`)
against the finite measure tend to the integral of the limit.
Related results:
* `MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_filter_of_le_const`:
more general assumptions
* `MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const`:
using `MeasureTheory.lintegral` for integration.
-/
theorem tendsto_testAgainstNN_of_le_const {μ : FiniteMeasure Ω} {fs : ℕ → Ω →ᵇ ℝ≥0} {c : ℝ≥0}
(fs_le_const : ∀ n ω, fs n ω ≤ c) {f : Ω →ᵇ ℝ≥0} (fs_lim : ∀ ω, Tendsto (fun n ↦ fs n ω) atTop (𝓝 (f ω))) :
Tendsto (fun n ↦ μ.testAgainstNN (fs n)) atTop (𝓝 (μ.testAgainstNN f)) :=
tendsto_testAgainstNN_filter_of_le_const (.of_forall fun n ↦ .of_forall (fs_le_const n)) (.of_forall fs_lim)
