posPart — Mathlib

English

In L1, the norm of a simple function’s integral equals the integral of the norm of the function via a compatibility with the mapping to SimpleFunc.

Русский

В пространстве L1 норма интеграла простой функции равна интегралу нормы функции через соответствие с отображением в SimpleFunc.

LaTeX

$$$$ \\|f\\| = \\big( (toSimpleFunc f).map \\|\\cdot\\| \\big)_{\\\\text{integral}} μ $$$$

Lean4

/-- Positive part of a simple function in L1 space. -/
nonrec def posPart (f : α →₁ₛ[μ] ℝ) : α →₁ₛ[μ] ℝ :=
  ⟨Lp.posPart (f : α →₁[μ] ℝ), by
    rcases f with ⟨f, s, hsf⟩
    use s.posPart
    simp only [SimpleFunc.posPart, SimpleFunc.coe_map, Function.comp_def, coe_posPart, ← hsf, posPart_mk]⟩

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