coeFn_compMeasurePreserving — Mathlib

English

The operator that composes with a measure-preserving map between Lp spaces is an isometry; it preserves the Lp-norm exactly.

Русский

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

LaTeX

$$$Isometry\ (compMeasurePreserving\ f\ hf: Lp(E,p,μb) \to Lp(E,p,μ))$$$

Lean4

theorem coeFn_compMeasurePreserving (g : Lp E p μb) (hf : MeasurePreserving f μ μb) :
    compMeasurePreserving f hf g =ᵐ[μ] g ∘ f :=
  g.1.coeFn_compMeasurePreserving hf

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