English
If a family F(n) is ae-measurable and uniformly bounded in norm by a bound depending on the parameter, and F(n, x) tends to f(x) pointwise a.e., then the integral converges: ∫ F_n → ∫ f.
Русский
Если F(n) измерима почти всюду и ограничена по норме равномерно (зависит от параметра), и F_n(x) стремится к f(x) почти всюду, то интеграл сходится: ∫ F_n → ∫ f.
LaTeX
$$$\\lim_{n\\to\\infty} \\int_α F_n(a)\\,dμ(a) = \\int_α f(a)\\,dμ(a)$$$
Lean4
/-- Continuity of interval integral with respect to a parameter, at a point within a set.
Given `F : X → ℝ → E`, assume `F x` is ae-measurable on `[a, b]` for `x` in a
neighborhood of `x₀` within `s` and at `x₀`, and assume it is bounded by a function integrable
on `[a, b]` independent of `x` in a neighborhood of `x₀` within `s`. If `(fun x ↦ F x t)`
is continuous at `x₀` within `s` for almost every `t` in `[a, b]`
then the same holds for `(fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀`. -/
theorem continuousWithinAt_of_dominated_interval {F : X → ℝ → E} {x₀ : X} {bound : ℝ → ℝ} {a b : ℝ} {s : Set X}
(hF_meas : ∀ᶠ x in 𝓝[s] x₀, AEStronglyMeasurable (F x) (μ.restrict <| Ι a b))
(h_bound : ∀ᶠ x in 𝓝[s] x₀, ∀ᵐ t ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t)
(bound_integrable : IntervalIntegrable bound μ a b)
(h_cont : ∀ᵐ t ∂μ, t ∈ Ι a b → ContinuousWithinAt (fun x => F x t) s x₀) :
ContinuousWithinAt (fun x => ∫ t in a..b, F x t ∂μ) s x₀ :=
tendsto_integral_filter_of_dominated_convergence bound hF_meas h_bound bound_integrable h_cont
