English
Let F: X → α → G be such that for every x near x0 the function a ↦ F(x, a) is measurable, and there is an integrable bound bound(a) with ‖F(x, a)‖ ≤ bound(a) for x near x0. If bound is integrable and for almost every a the map x ↦ F(x, a) is continuous at x0, then the Bochner integral x ↦ ∫α F(x, a) dμ is continuous at x0.
Русский
Пусть F: X → α → G таково, что для ближайших x к x0 функция a ↦ F(x, a) измерима, существует интегрируемый предел bound(a) и ‖F(x, a)‖ ≤ bound(a) для x рядом с x0. Если bound интегрируем и для почти всех a отображение x ↦ F(x, a) непрерывно в x0, то интеграл Бо́хнера x ↦ ∫α F(x, a) dμ непрерывен в x0.
LaTeX
$$$\\text{Let }F:X\\to\\alpha\\to G,\\ x_0\\in X,\\ bound:\\alpha\\to\\mathbb{R}.\\quad\\forall^\\! x\\text{ near }x_0:\\ AEStronglyMeasurable(F(x),\\mu),\\; \\forall^\\! x:\\ near x_0,\\ \\forall a,\\; \\|F(x,a)\\|\\le bound(a),\\text{ with } bound\\in L^1(\\mu),\\\\\\forall^\\! a,\\ ContinuousAt(x\\mapsto F(x,a))\\text{ at }x_0.\\\\\\text{Then }\\text{ContinuousAt}\\left(x\\mapsto\\int_{\\alpha} F(x,a)\\,d\\mu\\right)\\text{ at }x_0.$$$
Lean4
theorem continuousAt_of_dominated {F : X → α → G} {x₀ : X} {bound : α → ℝ}
(hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ) (h_bound : ∀ᶠ x in 𝓝 x₀, ∀ᵐ a ∂μ, ‖F x a‖ ≤ bound a)
(bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ a ∂μ, ContinuousAt (fun x => F x a) x₀) :
ContinuousAt (fun x => ∫ a, F x a ∂μ) x₀ :=
by
by_cases hG : CompleteSpace G
· simp only [integral, hG, L1.integral]
exact
continuousAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ) hF_meas h_bound bound_integrable
h_cont
· simp [integral, hG, continuousAt_const]
