integrable_comp_emb — Mathlib

English

If f is measure-preserving and a measurable embedding, then integrability under μ maps to integrability under ν via composition with f.

Русский

Если f сохраняет меру и есть внедрение, то интегрируемость транспонируется через композицию с f.

LaTeX

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

Lean4

theorem integrable_comp_emb {f : α → δ} {ν} (h₁ : MeasurePreserving f μ ν) (h₂ : MeasurableEmbedding f) {g : δ → ε} :
    Integrable (g ∘ f) μ ↔ Integrable g ν :=
  h₁.map_eq ▸ Iff.symm h₂.integrable_map_iff

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