English
Let F: X → α → G, bound: α → ℝ, and s ⊆ X. Suppose F(x) is AES-almost everywhere measurable and ‖F(x, a)‖ ≤ bound(a) for x ∈ s (a.e. in μ), bound is integrable, and for almost all a the restriction of x ↦ F(x, a) is continuous on s. Then the map x ↦ ∫_α F(x, a) dμ is continuously dependent on x on the set s, i.e., ContinuousOn(⋯) on s.
Русский
Пусть F: X → α → G, bound: α → ℝ и s ⊆ X. Пусть F(x) измеримо а.е., и ‖F(x, a)‖ ≤ bound(a) при x ∈ s (а.е. по μ), bound интегрируем, и для а почти всюду а. непрерывность функции x ↦ F(x, a) на s. Тогда x ↦ ∫_α F(x, a) dμ непрерывно зависит от x на s.
LaTeX
$$$\\text{Let }F:X\\to\\alpha\\to G,\\ bound:\\alpha\\to\\mathbb{R},\\ s\\subseteq X.\\; (i)\\ \\forall x\\in s:\\ AEStronglyMeasurable(F(x),\\mu),\\; (ii)\\ \\forall x\\in s:\\ \\forall^* a:\\|F(x,a)\\|\\le bound(a),\\; (iii)\\ Integrable\\ bound\\mu,\\ (iv)\\ \\forall^*a:\\ ContinuousOn(F(\\cdot,a),s). \\\\ \\text{Then }\\text{ContinuousOn}(x\\mapsto\\int_{\\alpha} F(x,a)\\,d\\mu, s).$$
Lean4
theorem continuousOn_of_dominated {F : X → α → G} {bound : α → ℝ} {s : Set X}
(hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ) (h_bound : ∀ x ∈ s, ∀ᵐ a ∂μ, ‖F x a‖ ≤ bound a)
(bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ a ∂μ, ContinuousOn (fun x => F x a) s) :
ContinuousOn (fun x => ∫ a, F x a ∂μ) s :=
by
by_cases hG : CompleteSpace G
· simp only [integral, hG, L1.integral]
exact
continuousOn_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ) hF_meas h_bound bound_integrable
h_cont
· simp [integral, hG, continuousOn_const]
