norm_toLp — Mathlib

English

For a Schwartz map f, the Lp-norm of f equals the real part of its eLp-norm, i.e., ‖f.toLp p μ‖ = ENNReal.toReal (eLpNorm f p μ).

Русский

Для отображения Шварца f нормa Lp равна реальной части eLp-нормы: ‖f.toLp p μ‖ = ENNReal.toReal (eLpNorm f p μ).

LaTeX

$$$$ \\|f^{\\mathrm{toLp}} p \\mu\\| = \\operatorname{ENNReal}.toReal\\big( eLpNorm(f, p, \\mu) \\big). $$$$

Lean4

theorem norm_toLp {f : 𝓢(E, F)} {p : ℝ≥0∞} {μ : Measure E} [hμ : μ.HasTemperateGrowth] :
    ‖f.toLp p μ‖ = ENNReal.toReal (eLpNorm f p μ) := by rw [Lp.norm_def, eLpNorm_congr_ae (coeFn_toLp f p μ)]

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