setLIntegral_comp_emb — Mathlib

English

If g is a measurable embedding, then the pushforward integration over s equals the integration over the image set g''s with respect to ν: ∫ a in s f(g a) dμ = ∫ b in g''s f(b) dν.

Русский

Если g — измеримое вложение, то интеграл по предобразу равен интегралу по образу: ∫ a∈s f(g(a)) dμ = ∫ b∈g''s f(b) dν.

LaTeX

$$$$ \int⁻ a in s, f(g a) ∂μ = \int⁻ b in g '' s, f b ∂ν. $$$$

Lean4

theorem setLIntegral_comp_emb (hge : MeasurableEmbedding g) (f : β → ℝ≥0∞) (s : Set α) :
    ∫⁻ a in s, f (g a) ∂μ = ∫⁻ b in g '' s, f b ∂ν := by
  rw [← hg.setLIntegral_comp_preimage_emb hge, Set.preimage_image_eq _ hge.injective]

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