integrable_map_iff — Mathlib

English

If f is a measure-preserving equivalence, then g is integrable w.r.t. μ.map f iff g ∘ f is integrable w.r.t μ.

Русский

Если f — эквивалент по мере, сохраняющий меру, то интегрируемость g по μ.map f эквивалентна интегрируемости g ∘ f по μ.

LaTeX

$$$\\mathrm{Integrable}(g, \\mathrm{map}\, f\, μ) \\iff \\mathrm{Integrable}(g\\circ f, μ)$ for a measure-preserving equivalence f.$$

Lean4

theorem _root_.MeasurableEmbedding.integrable_map_iff {f : α → δ} (hf : MeasurableEmbedding f) {g : δ → ε} :
    Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ :=
  by
  simp_rw [← memLp_one_iff_integrable]
  exact hf.memLp_map_measure_iff

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