eLpNorm_one_smul_measure

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.eLpNorm_one_smul_measure

← MathLib Explorer

English

For p = 1, scaling the measure by c ∈ ℝ≥0∞ scales the L1 norm by c.

Русский

При p = 1 масштабирование меры на c масштабирует норму L1 на c.

LaTeX

$$$\\mathrm{eLpNorm}(f,1,c\\cdot μ) = c \\cdot \\mathrm{eLpNorm}(f,1,μ).$$$

Lean4

theorem eLpNorm_one_smul_measure {f : α → ε} (c : ℝ≥0∞) : eLpNorm f 1 (c • μ) = c * eLpNorm f 1 μ := by
  rw [eLpNorm_smul_measure_of_ne_top] <;> simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru