Theorems · Theorem · real analysis

MeasureTheory.SimpleFunc.box_integral_eq_integral

∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  (f : MeasureTheory.SimpleFunc (ι → ℝ) E) (μ : MeasureTheory.Measure (ι → ℝ))
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] (I : BoxIntegral.Box ι) (l : BoxIntegral.IntegrationParams),
  l.bRiemann = false →
    BoxIntegral.integral I l (⇑f) μ.toBoxAdditive.toSMul = MeasureTheory.SimpleFunc.integral (μ.restrict ↑I) f

For a simple function, its McShane (or Henstock, or ⊥) box integral is equal to its integral in the sense of MeasureTheory.SimpleFunc.integral.

Defined in

Mathlib.Analysis.BoxIntegral.Integrability

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeNormedAddCommGroupNormedSpaceMeasureTheory.IsLocallyFiniteMeasure