Theorems · Theorem · measure theory
Function.Periodic.intervalIntegrable
∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ},
Function.Periodic f T →
T ≠ 0 →
IntervalIntegrable f MeasureTheory.volume t (t + T) →
∀ (a₁ a₂ : ℝ), IntervalIntegrable f MeasureTheory.volume a₁ a₂A periodic function is interval integrable over every interval if it is interval integrable over one period.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 247 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedAddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites32
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- TopologicalSpaceproof · cited by 24,529
- NormedAddCommGroupstatement and proof · cited by 15,752
- MeasureTheory.Measureproof · cited by 10,939
- Nat.cast_oneproof · cited by 2,501
- Nat.cast_zeroproof · cited by 1,870
- LT.lt.ne'proof · cited by 1,417
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- Nat.cast_addproof · cited by 586
- le_of_not_gtproof · cited by 430
- Set.uIccproof · cited by 393
- Int.cast_natCastproof · cited by 393
Cited by2
Results whose statement or proof uses this declaration.
- Function.Periodic.intervalIntegrable₀proof · cited by 2
- Function.Periodic.intervalIntegrable_iffproof · cited by 1