English
Continuity of a parametric interval integral: if F is a family of integrable functions on [a,b] depending continuously on a parameter, then the interval integral depends continuously on that parameter.
Русский
Непрерывность параметрического интеграла по интервалу: если F зависит непрерывно от параметра, то интеграл по интервалу зависит непрерывно от параметра.
LaTeX
$$$\\text{Continuous}\\bigl(\\lambda x, \\int_a^b F(x,t) dt\\bigr)$$$
Lean4
/-- Continuity of interval integral with respect to a parameter.
Given `F : X → ℝ → E`, assume each `F x` is ae-measurable on `[a, b]`,
and assume it is bounded by a function integrable on `[a, b]` independent of `x`.
If `(fun x ↦ F x t)` is continuous for almost every `t` in `[a, b]`
then the same holds for `(fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀`. -/
theorem continuous_of_dominated_interval {F : X → ℝ → E} {bound : ℝ → ℝ} {a b : ℝ}
(hF_meas : ∀ x, AEStronglyMeasurable (F x) <| μ.restrict <| Ι a b)
(h_bound : ∀ x, ∀ᵐ t ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b)
(h_cont : ∀ᵐ t ∂μ, t ∈ Ι a b → Continuous fun x => F x t) : Continuous fun x => ∫ t in a..b, F x t ∂μ :=
continuous_iff_continuousAt.mpr fun _ =>
continuousAt_of_dominated_interval (Eventually.of_forall hF_meas) (Eventually.of_forall h_bound) bound_integrable <|
h_cont.mono fun _ himp hx => (himp hx).continuousAt
