Theorems · Theorem · real analysis

BoxIntegral.HasIntegral.of_aeEq_zero

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

If f is a.e. equal to zero on a rectangular box, then it has McShane integral zero on this box.

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