English
Let f be integrable and bounded by C; then the norm of the difference between the full integral and the integral over a set s is bounded by μ.real(s^c)·C.
Русский
Пусть f интегрируема и ограничена константой C; тогда модуль разности между полным интегралом и интегралом по s ограничен μ.real(s^c)·C.
LaTeX
$$$$ \\left\\| \\int_X f \\, d\\mu - \\int_{x \\in s} f(x) \\, d\\mu(x) \\right\\| \\leq \\mu_{\\mathbb{R}}(s^c) \\; C $$$$
Lean4
theorem norm_integral_sub_setIntegral_le [IsFiniteMeasure μ] {C : ℝ} (hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C) {s : Set X}
(hs : MeasurableSet s) (hf1 : Integrable f μ) : ‖∫ (x : X), f x ∂μ - ∫ x in s, f x ∂μ‖ ≤ μ.real sᶜ * C :=
by
have h0 : ∫ (x : X), f x ∂μ - ∫ x in s, f x ∂μ = ∫ x in sᶜ, f x ∂μ := by
rw [sub_eq_iff_eq_add, add_comm, integral_add_compl hs hf1]
have h1 : ∫ x in sᶜ, ‖f x‖ ∂μ ≤ ∫ _ in sᶜ, C ∂μ :=
integral_mono_ae hf1.norm.restrict (integrable_const C) (ae_restrict_of_ae hf)
have h2 : ∫ _ in sᶜ, C ∂μ = μ.real sᶜ * C := by rw [setIntegral_const C, smul_eq_mul]
rw [h0, ← h2]
exact le_trans (norm_integral_le_integral_norm f) h1
