English
Relates a functorial L1-representation to the standard integral; the L1 representative integrates to the same as the original.
Русский
Связано представление в L1 с обычным интегралом; интеграл по представлению совпадает с интегралом от функции.
LaTeX
$$$\text{MeasureTheory.L1.integral_of_fun_eq_integral} hf$$$
Lean4
/-- If `F i → f` in `L1`, then `∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ`. -/
theorem tendsto_setIntegral_of_L1 {ι} (f : α → G) (hfi : Integrable f μ) {F : ι → α → G} {l : Filter ι}
(hFi : ∀ᶠ i in l, Integrable (F i) μ) (hF : Tendsto (fun i ↦ ∫⁻ x, ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)) (s : Set α) :
Tendsto (fun i ↦ ∫ x in s, F i x ∂μ) l (𝓝 (∫ x in s, f x ∂μ)) :=
by
refine tendsto_integral_of_L1 f hfi.restrict ?_ ?_
· filter_upwards [hFi] with i hi using hi.restrict
· simp_rw [← eLpNorm_one_eq_lintegral_enorm] at hF ⊢
exact
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hF (fun _ ↦ zero_le')
(fun _ ↦ eLpNorm_mono_measure _ Measure.restrict_le_self)
