Source indexedtheorem · leanprover/lean4:v4.32.0

Function.Periodic.setIntegral_Ioc_add_eq

Carleson.ToMathlib.MeasureTheory.Integral.IntervalIntegral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean:24 to 31

Source documentation

If f is a periodic function with period T, then its integral over [t, t + T] does not depend on t.

Exact Lean statement

theorem setIntegral_Ioc_add_eq (hf : Periodic f T) (t s : ℝ) :
    ∫ x in Ioc t (t + T), f x = ∫ x in Ioc s (s + T), f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem setIntegral_Ioc_add_eq (hf : Periodic f T) (t s : ℝ) :    ∫ x in Ioc t (t + T), f x = ∫ x in Ioc s (s + T), f x := by  wlog! hT : 0 < T  · rw [Ioc_eq_empty (by simpa), Ioc_eq_empty (by simpa)]  haveI : VAddInvariantMeasure (AddSubgroup.zmultiples T) ℝ volume :=    ⟨fun c s _ => measure_preimage_add _ _ _⟩  apply IsAddFundamentalDomain.setIntegral_eq (G := AddSubgroup.zmultiples T)  exacts [isAddFundamentalDomain_Ioc hT t, isAddFundamentalDomain_Ioc hT s, hf.map_vadd_zmultiples]