Source indexedtheorem · leanprover/lean4:v4.32.0

Function.Periodic.setLIntegral_Ioc_add_eq

Carleson.ToMathlib.MeasureTheory.Integral.IntervalIntegral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean:33 to 41

Mathematical statement

Exact Lean statement

theorem setLIntegral_Ioc_add_eq {f : ℝ → ℝ≥0∞} (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 setLIntegral_Ioc_add_eq {f : ℝ → ℝ≥0∞} (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.setLIntegral_eq (G := AddSubgroup.zmultiples T)  exacts [isAddFundamentalDomain_Ioc hT t, isAddFundamentalDomain_Ioc hT s,    (hf.comp enorm).map_vadd_zmultiples]