norm_indicatorConstLp — Mathlib

English

If 0 < p < ∞ and μ(s) is finite, then the Lp-norm of indicatorConstLp(p, s, hμs, c) equals ||c|| times μ(s)^(1/p).

Русский

Если 0 < p < ∞ и μ(s) < ∞, то||indicatorConstLp(p, s, hμs, c)||_p = ||c|| μ(s)^{1/p}.

LaTeX

$$$\|indicatorConstLp(p, hs, hμs, c)\| = \|c\| \cdot (\mu(s))^{1/p^{\mathrm{real}}}.$$$

Lean4

theorem norm_indicatorConstLp (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
    ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal) := by
  rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn, eLpNorm_indicator_const hs hp_ne_zero hp_ne_top,
    ENNReal.toReal_mul, measureReal_def, ENNReal.toReal_rpow, toReal_enorm]

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