Theorems · Theorem · real analysis

BoxIntegral.hasIntegralIndicatorConst

∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  (l : BoxIntegral.IntegrationParams),
  l.bRiemann = false →
    ∀ {s : Set (ι → ℝ)},
      MeasurableSet s →
        ∀ (I : BoxIntegral.Box ι) (y : E) (μ : MeasureTheory.Measure (ι → ℝ))
          [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ],
          BoxIntegral.HasIntegral I l (s.indicator fun x => y) μ.toBoxAdditive.toSMul (μ.real (s ∩ ↑I) • y)

The indicator function of a measurable set is McShane integrable with respect to any locally-finite measure.

Defined in

Mathlib.Analysis.BoxIntegral.Integrability

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeNormedAddCommGroupNormedSpaceMeasureTheory.IsLocallyFiniteMeasure