Theorems · Theorem · measure theory

MeasureTheory.Integrable.hasSum_intervalIntegral

∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E},
  MeasureTheory.Integrable f μ →
    ∀ (y : ℝ), HasSum (fun n => ∫ (x : ℝ) in y + ↑n..y + ↑n + 1, f x ∂μ) (∫ (x : ℝ), f x ∂μ)

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace