compMeasurePreservingₗ — Mathlib

English

Composition with a measure-preserving map preserves membership in Lp for function-valued maps; the Lp-norm is preserved under this composition.

Русский

Композиция с отображением, сохраняющим меру, сохраняет принадлежность функции к Lp; норма Lp сохраняется при композиции.

LaTeX

$$$g\in Lp(E,p,μb)\land f: α→β \Rightarrow g∘f \in Lp(E,p,μ)$$$

Lean4

/-- `MeasureTheory.Lp.compMeasurePreserving` as a linear map. -/
@[simps]
def compMeasurePreservingₗ (f : α → β) (hf : MeasurePreserving f μ μb) : Lp E p μb →ₗ[𝕜] Lp E p μ
    where
  __ := compMeasurePreserving f hf
  map_smul' c g := by rcases g with ⟨⟨_⟩, _⟩; rfl

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