norm_const — Mathlib

English

For finite μ, the norm of Lp-constant is exactly the formula involving μ.real univ and p, matching the previous norm statements.

Русский

Для конечной меры μ норма константы Лп равна формуле через μ.real и p.

LaTeX

$$norm of Lp.const p μ c equals ||c|| μ.real Set.univ^{1/p.toReal}.$$

Lean4

theorem norm_const [NeZero μ] (hp_zero : p ≠ 0) : ‖Lp.const p μ c‖ = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal) :=
  by
  have := NeZero.ne μ
  rw [← MemLp.toLp_const, Lp.norm_toLp, eLpNorm_const] <;> try assumption
  rw [measureReal_def, ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]

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