Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.map_integral

∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E)
  (g : E → F),
  MeasureTheory.Integrable (⇑f) μ →
    g 0 = 0 →
      MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map g f) = ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • g x

Calculate the integral of g ∘ f : α →ₛ F, where f is an integrable function from α to E and g is a function from E to F. We require g 0 = 0 so that g ∘ f is integrable.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.L1

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupNormedSpace