norm_compMeasurePreserving — Mathlib

English

The norm of the composition operator induced by a measure-preserving map equals the norm of the original Lp element after applying the map.

Русский

Норма оператора композиции, индуцированного отображением, сохраняющим меру, равна норме соответствующего элемента Lp после применения отображения.

LaTeX

$$$\|compMeasurePreserving\ f\ hf\ g\|=\|g\|$$$

Lean4

@[simp]
theorem norm_compMeasurePreserving (g : Lp E p μb) (hf : MeasurePreserving f μ μb) :
    ‖compMeasurePreserving f hf g‖ = ‖g‖ :=
  congr_arg ENNReal.toReal <| g.1.eLpNorm_compMeasurePreserving hf

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