compMeasurePreservingₗᵢ — Mathlib

English

The map sending a function to its composition with a measure-preserving map is an isometry with respect to the Lp-norm.

Русский

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

LaTeX

$$Isometry (compMeasurePreserving f hf) on Lp$$

Lean4

/-- `MeasureTheory.Lp.compMeasurePreserving` as a linear isometry. -/
@[simps!]
def compMeasurePreservingₗᵢ [Fact (1 ≤ p)] (f : α → β) (hf : MeasurePreserving f μ μb) : Lp E p μb →ₗᵢ[𝕜] Lp E p μ
    where
  toLinearMap := compMeasurePreservingₗ 𝕜 f hf
  norm_map' := (norm_compMeasurePreserving · hf)

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