Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.map_lintegral

∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (g : β → ENNReal)
  (f : MeasureTheory.SimpleFunc α β),
  (MeasureTheory.SimpleFunc.map g f).lintegral μ = ∑ x ∈ f.range, g x * μ (⇑f ⁻¹' {x})

Calculate the integral of (g ∘ f), where g : β → ℝ≥0∞ and f : α →ₛ β.

Defined in

Mathlib.MeasureTheory.Function.SimpleFunc

Cited by

7 results in Mathlib

Foundations

Depth 191 from the axioms · uses propext, Classical.choice, Quot.sound