mathlib3

e409a904 - feat(measure_theory/integral/periodic.lean): add lemma `function.periodic.tendsto_at_bot_interval_integral_of_pos'` (#12500)

feat(measure_theory/integral/periodic.lean): add lemma `function.periodic.tendsto_at_bot_interval_integral_of_pos'` (#12500) Partner of `function.periodic.tendsto_at_top_interval_integral_of_pos'` (I probably should have included this in #12488) Formalized as part of the Sphere Eversion project.