smul_measure

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.MemLp.smul_measure

English

If f ∈ Lp(μ), then multiplying μ by a scalar c ≠ ∞ preserves MemLp membership.

Русский

Если f ∈ Lp(μ), то умножение меры на скаляр c ≠ ∞ сохраняет принадлежность к MemLp.

LaTeX

$$MemLp f p μ → Ne c top → MemLp f p (c • μ).$$

Lean4

theorem smul_measure {f : α → ε} {c : ℝ≥0∞} (hf : MemLp f p μ) (hc : c ≠ ∞) : MemLp f p (c • μ) :=
  hf.of_measure_le_smul hc le_rfl

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

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

Разделы

Аффилиация

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