integrable_map_equiv — Mathlib

English

If f is a measurable equivalence, then the same integrability equivalence holds with simplifications.

Русский

Если f является измеримым эквивалентом, то та же эквивалентность интегрируемости сохраняется под упрощениями.

LaTeX

$$$\\mathrm{Integrable}(g,\\mathrm{map}\, f\, μ) \\iff \\mathrm{Integrable}(g\\circ f, μ)$ (simplified form for measurable equivalence).$$

Lean4

theorem integrable_map_equiv (f : α ≃ᵐ δ) (g : δ → ε) : Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ :=
  by
  simp_rw [← memLp_one_iff_integrable]
  exact f.memLp_map_measure_iff

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