English
Expressing the L1 integral of f through the norms of its positive and negative parts: ∫ f = ∥posPart f∥ − ∥negPart f∥.
Русский
Выражаем интеграл через нормы положительной и отрицательной частей: ∫ f = ∥posPart f∥ − ∥negPart f∥.
LaTeX
$$$\int f = \|\mathrm{posPart}\, f\| - \|\mathrm{negPart}\, f\|$$$
Lean4
theorem integral_eq_norm_posPart_sub (f : α →₁ₛ[μ] ℝ) : integral f = ‖posPart f‖ - ‖negPart f‖ := by
-- Convert things in `L¹` to their `SimpleFunc` counterpart
have ae_eq₁ : (toSimpleFunc f).posPart =ᵐ[μ] (toSimpleFunc (posPart f)).map norm :=
by
filter_upwards [posPart_toSimpleFunc f] with _ h
rw [SimpleFunc.map_apply, h]
conv_lhs =>
rw [← SimpleFunc.posPart_map_norm, SimpleFunc.map_apply]
-- Convert things in `L¹` to their `SimpleFunc` counterpart
have ae_eq₂ : (toSimpleFunc f).negPart =ᵐ[μ] (toSimpleFunc (negPart f)).map norm :=
by
filter_upwards [negPart_toSimpleFunc f] with _ h
rw [SimpleFunc.map_apply, h]
conv_lhs => rw [← SimpleFunc.negPart_map_norm, SimpleFunc.map_apply]
rw [integral, norm_eq_integral, norm_eq_integral, ← SimpleFunc.integral_sub]
· change
(toSimpleFunc f).integral μ =
((toSimpleFunc (posPart f)).map norm - (toSimpleFunc (negPart f)).map norm).integral μ
apply MeasureTheory.SimpleFunc.integral_congr (SimpleFunc.integrable f)
filter_upwards [ae_eq₁, ae_eq₂] with _ h₁ h₂
rw [SimpleFunc.sub_apply, ← h₁, ← h₂]
exact DFunLike.congr_fun (toSimpleFunc f).posPart_sub_negPart.symm _
· exact (SimpleFunc.integrable f).pos_part.congr ae_eq₁
· exact (SimpleFunc.integrable f).neg_part.congr ae_eq₂
