compMeasurePreserving_mem_Lp — Mathlib

English

If g belongs to Lp on β with respect to μb, and f is measure-preserving from α to β, then g∘f belongs to Lp on α with respect to μ.

Русский

Если g принадлежит Lp на β по отношению к μb, и f измеримо сохраняет меры, то g∘f принадлежит Lp на α по отношению к μ.

LaTeX

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

Lean4

theorem compMeasurePreserving_mem_Lp {β : Type*} [MeasurableSpace β] {μb : MeasureTheory.Measure β} {g : β →ₘ[μb] E}
    (hg : g ∈ Lp E p μb) {f : α → β} (hf : MeasurePreserving f μ μb) : g.compMeasurePreserving f hf ∈ Lp E p μ :=
  by
  rw [Lp.mem_Lp_iff_eLpNorm_lt_top] at hg ⊢
  rwa [eLpNorm_compMeasurePreserving]

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