mk_smul_toLp — Mathlib

English

Precomposition by the action map matches the Lp construction under measure-preserving smoothing; the Lp realization commutes with the action.

Русский

Пре-композиция по отображению действия согласуется с построением Lp; реализация Lp коммутирует с действием.

LaTeX

$$mk c • hf.toLp f = (hf.comp_measurePreserving (measurePreserving_smul c μ)).toLp (f ∘ (c • ·))$$

Lean4

@[to_additive]
theorem mk_smul_toLp (c : M) {f : α → E} (hf : MemLp f p μ) :
    mk c • hf.toLp f = (hf.comp_measurePreserving <| measurePreserving_smul c μ).toLp (f <| c • ·) :=
  rfl

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