setLIntegral_subtype — Mathlib

English

If g is a measurable embedding, then for any function f the equality ∫ f d(map g μ) = ∫ f ∘ g dμ holds, even without assuming f is measurable.

Русский

Если g — измеримое вложение, то для любой функции f выполняется равенство ∫ f d(map g μ) = ∫ f ∘ g dμ даже без предположения о measurability f.

LaTeX

$$$$ \int f\, d(map\ g\ μ) = \int (f\circ g)\, dμ, $$$$

Lean4

theorem setLIntegral_subtype {s : Set α} (hs : MeasurableSet s) (t : Set s) (f : α → ℝ≥0∞) :
    ∫⁻ x in t, f x ∂(μ.comap (↑)) = ∫⁻ x in (↑) '' t, f x ∂μ := by
  rw [(MeasurableEmbedding.subtype_coe hs).restrict_comap, lintegral_subtype_comap hs, restrict_restrict hs,
    inter_eq_right.2 (Subtype.coe_image_subset _ _)]

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