eLpNorm'_const_smul_le

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.eLpNorm'_const_smul_le

← MathLib Explorer

English

If MemLp g p μ, then MemLp (c · g) p μ for any scalar c.

Русский

Если MemLp g p μ, то MemLp (c · g) p μ для любого скаляра c.

LaTeX

$$$\operatorname{MemLp}(g,p,μ) \Rightarrow \operatorname{MemLp}(c g,p,μ)$$$

Lean4

theorem eLpNorm'_const_smul_le (hq : 0 < q) : eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * eLpNorm' f q μ :=
  eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul (Eventually.of_forall fun _ => nnnorm_smul_le ..) hq

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

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

Разделы

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

Аффилиация

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