English
If e is a measurable embedding and μ, ν are measures with MeasurePreserving e, then integrability under composition with e equals integrability under restriction with preimage.
Русский
Если e — измеримое вложение и μ, ν — меры, причём e сохраняет меру, то інтегрируемость через композицию с e равна через предобраз.
LaTeX
$$IntegrableOn (f ∘ e) (e^{-1} s) μ ⇔ IntegrableOn f s ν$$
Lean4
theorem integrableOn_image [MeasurableSpace β] {e : α → β} {ν} (h₁ : MeasurePreserving e μ ν)
(h₂ : MeasurableEmbedding e) {f : β → ε} {s : Set α} : IntegrableOn f (e '' s) ν ↔ IntegrableOn (f ∘ e) s μ :=
((h₁.restrict_image_emb h₂ s).integrable_comp_emb h₂).symm