lintegral_map — Mathlib

English

If you have a simple function g on β and a measurable map f : α → β, then g.lintegral with the pushforward measure μ via f equals (g ∘ f) lintegral with μ.

Русский

Если есть простая функция g на β и измеримое отображение f : α → β, то g.lintegral по мере map f μ равен (g ∘ f) линеграль по μ.

LaTeX

$$$g.lintegral(\\mathrm{Measure.map} f μ) = (g \\circ f \\;\\text{with } hf).lintegral μ$$$

Lean4

theorem lintegral_map {β} [MeasurableSpace β] (g : β →ₛ ℝ≥0∞) {f : α → β} (hf : Measurable f) :
    g.lintegral (Measure.map f μ) = (g.comp f hf).lintegral μ :=
  Eq.symm <| lintegral_map' _ _ f (fun _ => rfl) fun _s hs => Measure.map_apply hf hs

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