English
If Fi → f in L1, then ∫ x in s Fi x → ∫ x in s f x for each set s.
Русский
Если Fi → f в L1, то интеграл по s Fi → интеграл по s f для каждого множества s.
LaTeX
$$$\text{Tendsto } i \mapsto \int x \in s_i, F_i(x) \partial μ \; \to \; \int x \in s, f(x) \partial μ$$$
Lean4
theorem continuousWithinAt_of_dominated {F : X → α → G} {x₀ : X} {bound : α → ℝ} {s : Set X}
(hF_meas : ∀ᶠ x in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ) (h_bound : ∀ᶠ x in 𝓝[s] x₀, ∀ᵐ a ∂μ, ‖F x a‖ ≤ bound a)
(bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ a ∂μ, ContinuousWithinAt (fun x => F x a) s x₀) :
ContinuousWithinAt (fun x => ∫ a, F x a ∂μ) s x₀ :=
by
by_cases hG : CompleteSpace G
· simp only [integral, hG, L1.integral]
exact
continuousWithinAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ) hF_meas h_bound
bound_integrable h_cont
· simp [integral, hG, continuousWithinAt_const]
