Theorems · Theorem · measure theory

intervalIntegrable_iff

∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.uIoc a b) μ

A function is interval integrable with respect to a given measure μ on a..b if and only if it is integrable on uIoc a b with respect to μ. This is an equivalent definition of IntervalIntegrable.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

29 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceENormedAddMonoidTopologicalSpace.PseudoMetrizableSpace