integrableOn_image — Mathlib

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

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