Commit 2022-10-12 04:37 f1138dc3

feat(measure_theory/integral/periodic): relate integrals over add_circle with integrals upstairs in ℝ (#16836) Prove that the covering map from ℝ to add_circle is measure-preserving, with respect to Lebesgue measure restricted to an interval (upstairs) and Haar measure (downstairs). As corollaries, lemmas relating the various integrals upstairs and downstairs.