Theorems · Definition · measure theory

MeasureTheory.SimpleFunc.integral

{α : Type u_1} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup F] →
      [NormedSpace ℝ F] → {x : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.SimpleFunc α F → F

Bochner integral of simple functions whose codomain is a real NormedSpace. This is equal to ∑ x ∈ f.range, μ.real (f ⁻¹' {x}) • x (see integral_eq).

Defined in

Mathlib.MeasureTheory.Integral.Bochner.L1

Cited by

35 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace