norm_indicatorConstLp_top — Mathlib

English

If p corresponds to ∞ and μ(s) is finite and nonzero, then the L∞-norm of indicatorConstLp(p, s, hμs, c) equals ||c||.

Русский

Если p = ∞ и μ(s) ≠ 0, то L∞-норма indicatorConstLp(p, s, hμs, c) равна ||c||.

LaTeX

$$$\|indicatorConstLp(p, hs, hμs, c)\| = \|c\|$ when p = \infty$ and μ(s) ≠ 0.$$

Lean4

theorem norm_indicatorConstLp_top (hμs_ne_zero : μ s ≠ 0) : ‖indicatorConstLp ∞ hs hμs c‖ = ‖c‖ := by
  rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn, eLpNorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero,
    ENNReal.toReal_top, _root_.div_zero, ENNReal.rpow_zero, mul_one, toReal_enorm]

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