English
Let F: X × ℝ → E be ae-measurable and dominated on a neighborhood of a point; if F(x, t) converges to f(t) for a.e. t in interval and F satisfies uniform bounds, then the parametric interval integral is continuous in the parameter at that point.
Русский
Пусть F: X × ℝ → E измерима почти всюду и ограничена на окрестности точки; если F сходится к f по почти всем t, и выполнено ограничение, то интеграл по интервалу зависит непрерывно от параметра в данной точке.
LaTeX
$$$\\text{ContinuousWithinAt}\\bigl(\\lambda x, \\int_{a}^{b} F(x, t)\,dt\\bigr) = \\text{dc-continuity-form}$$$
Lean4
/-- Continuity of interval integral with respect to a parameter at a point.
Given `F : X → ℝ → E`, assume `F x` is ae-measurable on `[a, b]` for `x` in a
neighborhood of `x₀`, and assume it is bounded by a function integrable on
`[a, b]` independent of `x` in a neighborhood of `x₀`. If `(fun x ↦ F x t)`
is continuous at `x₀` for almost every `t` in `[a, b]`
then the same holds for `(fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀`. -/
theorem continuousAt_of_dominated_interval {F : X → ℝ → E} {x₀ : X} {bound : ℝ → ℝ} {a b : ℝ}
(hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict <| Ι a b))
(h_bound : ∀ᶠ x in 𝓝 x₀, ∀ᵐ t ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b)
(h_cont : ∀ᵐ t ∂μ, t ∈ Ι a b → ContinuousAt (fun x => F x t) x₀) :
ContinuousAt (fun x => ∫ t in a..b, F x t ∂μ) x₀ :=
tendsto_integral_filter_of_dominated_convergence bound hF_meas h_bound bound_integrable h_cont
