Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-07 16:01 5f2a6ac6

View on Github →

feat(measure_theory/integral/periodic): further properties of periodic integrals (#12488) Formalized as part of the Sphere Eversion project.

Estimated changes

Modified src/algebra/order/floor.lean

added theorem int.fract_div_mul_self_add_zsmul_eq

added theorem int.fract_div_mul_self_mem_Ico

Modified src/measure_theory/integral/periodic.lean

added theorem function.periodic.Inf_add_zsmul_le_integral_of_pos

modified theorem function.periodic.interval_integral_add_eq

added theorem function.periodic.interval_integral_add_eq_add

modified theorem function.periodic.interval_integral_add_eq_of_pos

added theorem function.periodic.interval_integral_add_zsmul_eq

added theorem function.periodic.tendsto_at_top_interval_integral_of_pos'

added theorem function.periodic.tendsto_at_top_interval_integral_of_pos

modified theorem is_add_fundamental_domain_Ioc

Modified src/topology/algebra/order/compact.lean

added theorem continuous_on.Inf_image_Icc_le

modified theorem continuous_on.image_Icc

modified theorem continuous_on.image_interval

modified theorem continuous_on.image_interval_eq_Icc

added theorem continuous_on.le_Sup_image_Icc