Theorems · Theorem · measure theory

AddCircle.integral_liftIoc_eq_intervalIntegral

∀ (T : ℝ) [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {t : ℝ}
  {f : ℝ → E}, ∫ (a : AddCircle T), AddCircle.liftIoc T t f a = ∫ (a : ℝ) in t..t + T, f a

The integral of a function lifted to AddCircle from an interval (t, t + T] to AddCircle T is equal to the intervalIntegral over the interval.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactNormedAddCommGroupNormedSpace