eLpNormEssSup_smul_measure — Mathlib

English

If c ≠ 0, then scaling the measure by c does not change the ess sup norm of f.

Русский

Если c ≠ 0, то масштабирование меры на c не изменяет ess sup нормы функции f.

LaTeX

$$$c \\neq 0 \\Rightarrow eLpNormEssSup f (c \\cdot μ) = eLpNormEssSup f μ.$$$

Lean4

@[simp]
theorem eLpNormEssSup_smul_measure (hc : c ≠ 0) (f : α → ε) : eLpNormEssSup f (c • μ) = eLpNormEssSup f μ :=
  by
  simp_rw [eLpNormEssSup]
  exact essSup_smul_measure hc _

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