mathlib

f1138dc3 - feat(measure_theory/integral/periodic): relate integrals over `add_circle` with integrals upstairs in `ℝ` (#16836)

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. Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>