English
A bounded convergence theorem for FiniteMeasure: if fs ≤ c and fs ω → f ω pointwise, then ∫⁻ fs i ω → ∫⁻ f ω with respect to μ.
Русский
Сходимость по ограниченным линтегралу: если функции ограничены константой и сходятся по точкам, то интегралы сходятся.
LaTeX
$$$ \text{tendsto}_{i} \int⁻ ω, fs_i ω ∂(μ : \text{Measure } Ω) = \int⁻ ω, f ω ∂(μ : \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.lintegral`) against the finite
measure tend to the integral of the limit.
A related result with more general assumptions is
`MeasureTheory.tendsto_lintegral_nn_filter_of_le_const`.
-/
theorem tendsto_lintegral_nn_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 ↦ ∫⁻ ω, fs n ω ∂(μ : Measure Ω)) atTop (𝓝 (∫⁻ ω, f ω ∂(μ : Measure Ω))) :=
tendsto_lintegral_nn_filter_of_le_const μ (.of_forall fun n ↦ .of_forall (fs_le_const n)) (.of_forall fs_lim)
