negPart_toSimpleFunc — Mathlib

English

For f, the decomposition into positive and negative parts satisfies the Bochner integral identity: ∫ f = ∥posPart f∥ − ∥negPart f∥.

Русский

Разложение на положительную и отрицательную части удовлетворяет формуле: ∫ f = ∥posPart f∥ − ∥negPart f∥.

LaTeX

$$$\int f = \|\mathrm{posPart}\, f\| - \|\mathrm{negPart}\, f\|$$$

Lean4

theorem negPart_toSimpleFunc (f : α →₁ₛ[μ] ℝ) : toSimpleFunc (negPart f) =ᵐ[μ] (toSimpleFunc f).negPart :=
  by
  rw [SimpleFunc.negPart, MeasureTheory.SimpleFunc.negPart]
  filter_upwards [posPart_toSimpleFunc (-f), neg_toSimpleFunc f]
  intro a h₁ h₂
  rw [h₁]
  change max _ _ = max _ _
  rw [h₂]
  simp

Похожие утверждения