English
Let F: X → α → G be such that for every x, a is in μ-measurable, ‖F(x,a)‖ is bounded by some integrable bound, and for almost every a the map x ↦ F(x,a) is continuous. Then the Bochner integral x ↦ ∫_α F(x,a) dμ is continuous as a function of x.
Русский
Пусть F: X → α → G так, что для каждого x, a функция измерима, и ‖F(x,a)‖ ограничена интегрируемым bound; а по a почти всюду F(x,a) непрерывно по x. Тогда x ↦ ∫_α F(x,a) dμ непрерывно в x.
LaTeX
$$$\\text{Let }F:X\\to\\alpha\\to G,\\bound:\\alpha\\to\\mathbb{R},\\text{ and assume }(i)\\ AEStronglyMeasurable(F(x),\\mu)\\ \\forall x,\\ (ii)\\ bound\\in L^1(μ),\\ (iii)\\ For a.e. a, x\\mapsto F(x,a) \\\\text{ is Continuous}. \\Rightarrow\\ x\\mapsto \\int_α F(x,a) dμ\\text{ is Continuous.}$$$
Lean4
theorem continuous_of_dominated {F : X → α → G} {bound : α → ℝ} (hF_meas : ∀ x, AEStronglyMeasurable (F x) μ)
(h_bound : ∀ x, ∀ᵐ a ∂μ, ‖F x a‖ ≤ bound a) (bound_integrable : Integrable bound μ)
(h_cont : ∀ᵐ a ∂μ, Continuous fun x => F x a) : Continuous fun x => ∫ a, F x a ∂μ :=
by
by_cases hG : CompleteSpace G
· simp only [integral, hG, L1.integral]
exact
continuous_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ) hF_meas h_bound bound_integrable h_cont
· simp [integral, hG, continuous_const]
