norm_toSimpleFunc — Mathlib

English

For p ≥ 1, the norm of a simple Lp-function equals the real part of its eLp-norm after converting to a simple function.

Русский

Для p ≥ 1 норма простого Lp-функционала равна действительной части eLp-нормы после преобразования в простую функцию.

LaTeX

$$$ \\|f\\| = \\mathrm{toReal}\\left( eLpNorm\\left( toSimpleFunc\\,f\\right)\\ p\\, μ\\right) $$$

Lean4

theorem norm_toSimpleFunc [Fact (1 ≤ p)] (f : Lp.simpleFunc E p μ) :
    ‖f‖ = ENNReal.toReal (eLpNorm (toSimpleFunc f) p μ) := by
  simpa [toLp_toSimpleFunc] using norm_toLp (toSimpleFunc f) (simpleFunc.memLp f)

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