Theorems · Theorem · real analysis

BoxIntegral.integrable_of_bounded_and_ae_continuousWithinAt

∀ {ι : Type u} {E : Type v} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : Fintype ι]
  (l : BoxIntegral.IntegrationParams) [CompleteSpace E] {I : BoxIntegral.Box ι} {f : (ι → ℝ) → E},
  (∃ C, ∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ C) →
    ∀ (μ : MeasureTheory.Measure (ι → ℝ)) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ],
      (∀ᵐ (x : ι → ℝ) ∂μ.restrict (BoxIntegral.Box.Icc I), ContinuousWithinAt f (BoxIntegral.Box.Icc I) x) →
        BoxIntegral.Integrable I l f μ.toBoxAdditive.toSMul

A function that is bounded and a.e. continuous on a box I is integrable on I.

Defined in

Mathlib.Analysis.BoxIntegral.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFintypeCompleteSpaceMeasureTheory.IsLocallyFiniteMeasure