eLpNorm_eq_eLpNorm' — Mathlib

English

Let p be a positive finite ENNReal exponent (not zero, not infinity). Then the standard eLpNorm equals the prime variant with p.toReal.

Русский

Пусть p — положительный конечный показатель ENNReal; тогда eLpNorm(f,p,μ) = eLpNorm'(f,p.toReal,μ).

LaTeX

$$$eLpNorm\\,f\\,p\\,\\mu = eLpNorm'\\,f\\,p.toReal\\,\\mu$$

Lean4

theorem eLpNorm_eq_eLpNorm' (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) {f : α → ε} :
    eLpNorm f p μ = eLpNorm' f (ENNReal.toReal p) μ := by simp [eLpNorm, hp_ne_zero, hp_ne_top]

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