English
Let f be integrable; the norm of the difference between f and its approximation on a separable range tends to 0 in L1, i.e., Tendsto of ∥SimpleFunc.approxOn(...) − f∥ in L1 to 0.
Русский
Для интегрируемой f нормa разности между f и её аппроксимацией на сепарабельном диапазоне сходится к 0 в L1.
LaTeX
$$$\\lim_{n\\to\\infty} \\| f - \\text{approxOn}(f, s, 0, n) \\|_{L^1(μ)} = 0$.$$
Lean4
@[gcongr]
theorem integral_mono_measure {f : α → E} {ν : Measure α} (hle : μ ≤ ν) (hf : 0 ≤ᵐ[ν] f) (hfi : Integrable f ν) :
∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν := by
borelize E
obtain ⟨g, hg, hg_nonneg, hfg⟩ :=
hfi.1.exists_stronglyMeasurable_range_subset isClosed_Ici.measurableSet (Set.nonempty_Ici (a := 0)) hf
rw [integrable_congr hfg] at hfi
simp only [integral_congr_ae hfg, integral_congr_ae (ae_mono hle hfg)]
have _ := hg.separableSpace_range_union_singleton (b := 0)
have h₁ := tendsto_integral_approxOn_of_measurable_of_range_subset hg.measurable hfi _ le_rfl
have h₂ := tendsto_integral_approxOn_of_measurable_of_range_subset hg.measurable (hfi.mono_measure hle) _ le_rfl
apply le_of_tendsto_of_tendsto' h₂ h₁
exact fun n ↦
SimpleFunc.integral_mono_measure (Eventually.of_forall <| SimpleFunc.approxOn_range_nonneg hg_nonneg n) hle
(SimpleFunc.integrable_approxOn_range _ hfi n)
