posPart_toSimpleFunc — Mathlib

English

The negative part of a simple function maps (via toSimpleFunc) to the corresponding negative part almost everywhere.

Русский

Отрицательная часть простой функции отображается через toSimpleFunc к соответствующей отрицательной части почти повсеместно.

LaTeX

$$$\toSimpleFunc(\mathrm{negPart}\, f) =^\mu (\mathrm{toSimpleFunc}\, f)^{-}$$$

Lean4

theorem posPart_toSimpleFunc (f : α →₁ₛ[μ] ℝ) : toSimpleFunc (posPart f) =ᵐ[μ] (toSimpleFunc f).posPart :=
  by
  have eq : ∀ a, (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0 := fun a => rfl
  have ae_eq : ∀ᵐ a ∂μ, toSimpleFunc (posPart f) a = max ((toSimpleFunc f) a) 0 :=
    by
    filter_upwards [toSimpleFunc_eq_toFun (posPart f), Lp.coeFn_posPart (f : α →₁[μ] ℝ), toSimpleFunc_eq_toFun f] with _
      _ h₂ h₃
    convert h₂ using 1
    rw [h₃]
  refine ae_eq.mono fun a h => ?_
  rw [h, eq]

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