English
For a real-valued integrable function f, the Bochner integral equals the difference between the integrals of its positive part and its negative part, i.e., ∫ f = ∫ f⁺ − ∫ f⁻, where f⁺ and f⁻ are the positive and negative parts of f.
Русский
Для интегрируемой по Лоне вещественной функции f интеграл равен разности интегралов частей: ∫ f = ∫ f⁺ − ∫ f⁻, где f⁺ и f⁻ — положительная и отрицательная части f.
LaTeX
$$$\\int a, f(a)\\,d\\mu = \\operatorname{toReal}\\left(\\int^- a, \\mathbf{ofReal}(f(a))\\,d\\mu\\right) - \\operatorname{toReal}\\left(\\int^- a, \\mathbf{ofReal}(-f(a))\\,d\\mu\\right)$$$
Lean4
/-- The Bochner integral of a real-valued function `f : α → ℝ` is the difference between the
integral of the positive part of `f` and the integral of the negative part of `f`. -/
theorem integral_eq_lintegral_pos_part_sub_lintegral_neg_part {f : α → ℝ} (hf : Integrable f μ) :
∫ a, f a ∂μ = ENNReal.toReal (∫⁻ a, .ofReal (f a) ∂μ) - ENNReal.toReal (∫⁻ a, .ofReal (-f a) ∂μ) :=
by
let f₁ := hf.toL1 f
have eq₁ : ENNReal.toReal (∫⁻ a, ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖ :=
by
rw [L1.norm_def]
congr 1
apply lintegral_congr_ae
filter_upwards [Lp.coeFn_posPart f₁, hf.coeFn_toL1] with _ h₁ h₂
rw [h₁, h₂, ENNReal.ofReal]
congr 1
apply NNReal.eq
rw [Real.nnnorm_of_nonneg (le_max_right _ _)]
rw [Real.coe_toNNReal', NNReal.coe_mk]
-- Go to the `L¹` space
have eq₂ : ENNReal.toReal (∫⁻ a, ENNReal.ofReal (-f a) ∂μ) = ‖Lp.negPart f₁‖ :=
by
rw [L1.norm_def]
congr 1
apply lintegral_congr_ae
filter_upwards [Lp.coeFn_negPart f₁, hf.coeFn_toL1] with _ h₁ h₂
rw [h₁, h₂, ENNReal.ofReal]
congr 1
apply NNReal.eq
simp only [Real.coe_toNNReal', coe_nnnorm, nnnorm_neg]
rw [Real.norm_of_nonpos (min_le_right _ _), ← max_neg_neg, neg_zero]
rw [eq₁, eq₂, integral, dif_pos, dif_pos]
exact L1.integral_eq_norm_posPart_sub _
