compMeasurePreserving — Mathlib

English

For g with Lp on β and a measure-preserving map f, the composed function g∘f is in Lp on α with respect to μ.

Русский

Для g в Lp на β и отображения, сохраняющего меру, f, композиция g∘f принадлежит Lp на α.

LaTeX

$$$g\in Lp\ E\ p\ μb \land f\text{ MeasurePreserving } μ\to μb \Rightarrow g\circ f ∈ Lp\ E\ p\ μ$$$

Lean4

/-- Composition of an `L^p` function with a measure-preserving function is an `L^p` function. -/
def compMeasurePreserving (f : α → β) (hf : MeasurePreserving f μ μb) : Lp E p μb →+ Lp E p μ
    where
  toFun g := ⟨g.1.compMeasurePreserving f hf, g.1.compMeasurePreserving_mem_Lp g.2 hf⟩
  map_zero' := rfl
  map_add' := by rintro ⟨⟨_⟩, _⟩ ⟨⟨_⟩, _⟩; rfl

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