Commit 2023-06-19 04:09 10d33483

View on Github →

feat: port MeasureTheory.Integral.Periodic (#4815)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/Periodic.lean

added theorem AddCircle.volume_closedBall

added theorem Function.Periodic.integral_le_sSup_add_zsmul_of_pos

added theorem Function.Periodic.intervalIntegral_add_eq

added theorem Function.Periodic.intervalIntegral_add_eq_add

added theorem Function.Periodic.intervalIntegral_add_eq_of_pos

added theorem Function.Periodic.intervalIntegral_add_zsmul_eq

added theorem Function.Periodic.sInf_add_zsmul_le_integral_of_pos

added theorem Function.Periodic.tendsto_atBot_intervalIntegral_of_pos'

added theorem Function.Periodic.tendsto_atBot_intervalIntegral_of_pos

added theorem Function.Periodic.tendsto_atTop_intervalIntegral_of_pos'

added theorem Function.Periodic.tendsto_atTop_intervalIntegral_of_pos

added theorem isAddFundamentalDomain_Ioc'

added theorem isAddFundamentalDomain_Ioc