lpMeasToLpTrim_smul — Mathlib

English

The trim-to-Lp map commutes with scalar multiplication: lpMeasToLpTrim of c·f equals c times the trim of f.

Русский

Обрезка через Lp-смежную пропорцию совместима с умножением на скаляр: map(c·f) = c·map(f).

LaTeX

$$$lpMeasToLpTrim\ F\ 𝕜\ p\ μ hm (c \cdot f) = c \cdot lpMeasToLpTrim\ F\ 𝕜\ p\ μ hm f$$$

Lean4

theorem lpMeasToLpTrim_smul (hm : m ≤ m0) (c : 𝕜) (f : lpMeas F 𝕜 m p μ) :
    lpMeasToLpTrim F 𝕜 p μ hm (c • f) = c • lpMeasToLpTrim F 𝕜 p μ hm f :=
  by
  ext1
  grw [Lp.coeFn_smul]
  refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm ?_ ?_
  · exact (Lp.stronglyMeasurable _).const_smul c
  grw [lpMeasToLpTrim_ae_eq]
  push_cast
  grw [Lp.coeFn_smul, lpMeasToLpTrim_ae_eq]

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