English
For a real-valued integrable function, the integral of the norm equals a subtraction of two integrals over positive and non-positive sets.
Русский
Для вещественно-значимого интегрируемого функции интеграл нормы то же самое разложение на множества положительных и неотрицательных значений.
LaTeX
$$$$ \int \|f\| \, d\mu = \int_{\{f \ge 0\}} f \, d\mu - \int_{\{f < 0\}} f \, d\mu $$$$
Lean4
theorem integral_norm_eq_pos_sub_neg {f : X → ℝ} (hfi : Integrable f μ) :
∫ x, ‖f x‖ ∂μ = ∫ x in {x | 0 ≤ f x}, f x ∂μ - ∫ x in {x | f x ≤ 0}, f x ∂μ :=
have h_meas : NullMeasurableSet {x | 0 ≤ f x} μ := aestronglyMeasurable_const.nullMeasurableSet_le hfi.1
calc
∫ x, ‖f x‖ ∂μ = ∫ x in {x | 0 ≤ f x}, ‖f x‖ ∂μ + ∫ x in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ := by
rw [← integral_add_compl₀ h_meas hfi.norm]
_ = ∫ x in {x | 0 ≤ f x}, f x ∂μ + ∫ x in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ :=
by
congr 1
refine setIntegral_congr_fun₀ h_meas fun x hx => ?_
dsimp only
rw [Real.norm_eq_abs, abs_eq_self.mpr _]
exact hx
_ = ∫ x in {x | 0 ≤ f x}, f x ∂μ - ∫ x in {x | 0 ≤ f x}ᶜ, f x ∂μ :=
by
congr 1
rw [← integral_neg]
refine setIntegral_congr_fun₀ h_meas.compl fun x hx => ?_
dsimp only
rw [Real.norm_eq_abs, abs_eq_neg_self.mpr _]
rw [Set.mem_compl_iff, Set.notMem_setOf_iff] at hx
linarith
_ = ∫ x in {x | 0 ≤ f x}, f x ∂μ - ∫ x in {x | f x ≤ 0}, f x ∂μ := by
rw [← setIntegral_neg_eq_setIntegral_nonpos hfi.1, compl_setOf]; simp only [not_le]
