setLIntegral_comp_preimage — Mathlib

English

For a measurable g and measurable f, the preimage version of set L-integral satisfies the relation ∫ a in g^{-1} s f(g a) dμ = ∫ b in s f(b) dν.

Русский

Для измеримого g и измеримой f верно: ∫ a∈g^{-1}(s) f(g(a)) dμ = ∫ b∈s f(b) dν.

LaTeX

$$$$ \int⁻ a in g^{-1}' s, f(g a) \partial μ = \int⁻ b in s, f(b) \partial ν. $$$$

Lean4

theorem setLIntegral_comp_preimage {s : Set β} (hs : MeasurableSet s) {f : β → ℝ≥0∞} (hf : Measurable f) :
    ∫⁻ a in g ⁻¹' s, f (g a) ∂μ = ∫⁻ b in s, f b ∂ν := by rw [← hg.map_eq, setLIntegral_map hs hf hg.measurable]

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