memLp_map_measure_iff — Mathlib

English

If f is a measurable equivalence between spaces, then a function g has finite Lp-norm with respect to the pushforward measure map f μ if and only if the composition g ∘ f has finite Lp-norm with respect to μ.

Русский

Если f — измеримое эквивариантное отображение между пространствами, то функция g имеет конечную Lp-норму по мере map f μ тогда и только тогда, когда композиция g ∘ f имеет конечную Lp-норму по μ.

LaTeX

$$$\operatorname{MemLp}(g,p,\operatorname{Measure.map}(f,\mu)) \iff \operatorname{MemLp}(g\circ f,p,\mu)\quad( f \,\text{measurable equivalence})$$$

Lean4

theorem _root_.MeasurableEquiv.memLp_map_measure_iff (f : α ≃ᵐ β) : MemLp g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ :=
  f.measurableEmbedding.memLp_map_measure_iff

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