Theorems · Theorem · measure theory

Real.integrable_of_summable_norm_Icc

∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : C(ℝ, E)},
  (Summable fun n => ‖ContinuousMap.restrict (Set.Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖) →
    MeasureTheory.Integrable (⇑f) MeasureTheory.volume

If the sequence with n-th term the sup norm of fun x ↦ f (x + n) on the interval Icc 0 1, for n ∈ ℤ, is summable, then f is integrable on ℝ.

Defined in

Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup