Theorems · Theorem · real analysis

BoxIntegral.integrable_of_bounded_and_ae_continuous

∀ {ι : 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 : ι → ℝ) ∂μ, ContinuousAt f x) → BoxIntegral.Integrable I l f μ.toBoxAdditive.toSMul

A function that is bounded on a box I and a.e. continuous is integrable on I. This is a version of integrable_of_bounded_and_ae_continuousWithinAt with a stronger continuity assumption so that the user does not need to specialize the continuity assumption to each box on which the theorem is to be applied.

Defined in

Mathlib.Analysis.BoxIntegral.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFintypeCompleteSpaceMeasureTheory.IsLocallyFiniteMeasure