feat(measure_theory/integral/periodic): relate integrals over `add_ci…

…rcle` 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>

src/group_theory/subgroup/basic.lean

@@ -2683,6 +2683,9 @@ lemma exists_mem_zpowers {x : G} {p : G → Prop} :
   (∃ g ∈ zpowers x, p g) ↔ ∃ m : ℤ, p (x ^ m) :=
 set.exists_range_iff
 
+instance (a : G) : countable (zpowers a) :=
+((zpowers_hom G a).range_restrict_surjective.comp multiplicative.of_add.surjective).countable
+
 end subgroup
 
 namespace add_subgroup
@@ -2705,6 +2708,9 @@ attribute [to_additive add_subgroup.forall_mem_zmultiples] subgroup.forall_mem_z
 attribute [to_additive add_subgroup.exists_zmultiples] subgroup.exists_zpowers
 attribute [to_additive add_subgroup.exists_mem_zmultiples] subgroup.exists_mem_zpowers
 
+instance (a : A) : countable (zmultiples a) :=
+(zmultiples_hom A a).range_restrict_surjective.countable
+
 section ring
 
 variables {R : Type*} [ring R] (r : R) (k : ℤ)

src/measure_theory/constructions/borel_space.lean

@@ -11,6 +11,7 @@ import measure_theory.lattice
 import measure_theory.measure.open_pos
 import topology.algebra.order.liminf_limsup
 import topology.continuous_function.basic
+import topology.instances.add_circle
 import topology.instances.ereal
 import topology.G_delta
 import topology.order.lattice
@@ -1343,6 +1344,15 @@ instance ereal.borel_space : borel_space ereal := ⟨rfl⟩
 instance complex.measurable_space : measurable_space ℂ := borel ℂ
 instance complex.borel_space : borel_space ℂ := ⟨rfl⟩
 
+instance add_circle.measurable_space {a : ℝ} : measurable_space (add_circle a) :=
+borel (add_circle a)
+
+instance add_circle.borel_space {a : ℝ} : borel_space (add_circle a) := ⟨rfl⟩
+
+@[measurability] protected lemma add_circle.measurable_mk' {a : ℝ} :
+  measurable (coe : ℝ → add_circle a) :=
+continuous.measurable $ add_circle.continuous_mk' a
+
 /-- One can cut out `ℝ≥0∞` into the sets `{0}`, `Ico (t^n) (t^(n+1))` for `n : ℤ` and `{∞}`. This
 gives a way to compute the measure of a set in terms of sets on which a given function `f` does not
 fluctuate by more than `t`. -/

src/measure_theory/integral/periodic.lean

@@ -1,21 +1,33 @@
 /-
 Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yury Kudryashov
+Authors: Yury Kudryashov, Alex Kontorovich, Heather Macbeth
 -/
-import measure_theory.group.fundamental_domain
+import measure_theory.measure.haar_quotient
 import measure_theory.integral.interval_integral
 import topology.algebra.order.floor
 
 /-!
 # Integrals of periodic functions
 
-In this file we prove that `∫ x in t..t + T, f x = ∫ x in s..s + T, f x` for any (not necessarily
-measurable) function periodic function with period `T`.
+In this file we prove that the half-open interval `Ioc t (t + T)` in `ℝ` is a fundamental domain of
+the action of the subgroup `ℤ ∙ T` on `ℝ`.
+
+A consequence is `add_circle.measure_preserving_mk`: the covering map from `ℝ` to the "additive
+circle" `ℝ ⧸ (ℤ ∙ T)` is measure-preserving, with respect to the restriction of Lebesgue measure to
+`Ioc t (t + T)` (upstairs) and with respect to Haar measure (downstairs).
+
+Another consequence (`function.periodic.interval_integral_add_eq` and related declarations) is that
+`∫ x in t..t + T, f x = ∫ x in s..s + T, f x` for any (not necessarily measurable) function with
+period `T`.
 -/
 
-open set function measure_theory measure_theory.measure topological_space
-open_locale measure_theory
+open set function measure_theory measure_theory.measure topological_space add_subgroup
+  interval_integral
+
+open_locale measure_theory nnreal ennreal
+
+local attribute [-instance] quotient_add_group.measurable_space quotient.measurable_space
 
 lemma is_add_fundamental_domain_Ioc {T : ℝ} (hT : 0 < T) (t : ℝ) (μ : measure ℝ . volume_tac) :
   is_add_fundamental_domain (add_subgroup.zmultiples T) (Ioc t (t + T)) μ :=
@@ -27,21 +39,135 @@ begin
   simpa only [add_comm x] using exists_unique_add_zsmul_mem_Ioc hT x t
 end
 
+lemma is_add_fundamental_domain_Ioc' {T : ℝ} (hT : 0 < T) (t : ℝ) (μ : measure ℝ . volume_tac) :
+  is_add_fundamental_domain (add_subgroup.zmultiples T).opposite (Ioc t (t + T)) μ :=
+begin
+  refine is_add_fundamental_domain.mk' measurable_set_Ioc.null_measurable_set (λ x, _),
+  have : bijective (cod_restrict (λ n : ℤ, n • T) (add_subgroup.zmultiples T) _),
+    from (equiv.of_injective (λ n : ℤ, n • T) (zsmul_strict_mono_left hT).injective).bijective,
+  refine this.exists_unique_iff.2 _,
+  simpa using exists_unique_add_zsmul_mem_Ioc hT x t,
+end
+
+namespace add_circle
+variables (T : ℝ) [hT : fact (0 < T)]
+include hT
+
+/-- Equip the "additive circle" `ℝ ⧸ (ℤ ∙ T)` with, as a standard measure, the Haar measure of total
+mass `T` -/
+noncomputable instance measure_space : measure_space (add_circle T) :=
+{ volume := (ennreal.of_real T) • add_haar_measure ⊤,
+  .. add_circle.measurable_space }
+
+@[simp] protected lemma measure_univ : volume (set.univ : set (add_circle T)) = ennreal.of_real T :=
+begin
+  dsimp [(volume)],
+  rw ← positive_compacts.coe_top,
+  simp [add_haar_measure_self, -positive_compacts.coe_top],
+end
+
+instance is_finite_measure : is_finite_measure (volume : measure (add_circle T)) :=
+{ measure_univ_lt_top := by simp }
+
+/-- The covering map from `ℝ` to the "additive circle" `ℝ ⧸ (ℤ ∙ T)` is measure-preserving,
+considered with respect to the standard measure (defined to be the Haar measure of total mass `T`)
+on the additive circle, and with respect to the restriction of Lebsegue measure on `ℝ` to an
+interval (t, t + T]. -/
+protected lemma measure_preserving_mk (t : ℝ) :
+  measure_preserving (coe : ℝ → add_circle T) (volume.restrict (Ioc t (t + T))) :=
+measure_preserving_quotient_add_group.mk'
+  (is_add_fundamental_domain_Ioc' hT.out t)
+  (⊤ : positive_compacts (add_circle T))
+  (by simp)
+  T.to_nnreal
+  (by simp [← ennreal.of_real_coe_nnreal, real.coe_to_nnreal T hT.out.le])
+
+/-- The integral of a measurable function over `add_circle T` is equal to the integral over an
+interval (t, t + T] in `ℝ` of its lift to `ℝ`. -/
+protected lemma lintegral_preimage (t : ℝ) {f : add_circle T → ℝ≥0∞} (hf : measurable f) :
+  ∫⁻ a in Ioc t (t + T), f a = ∫⁻ b : add_circle T, f b :=
+by rw [← lintegral_map hf add_circle.measurable_mk',
+  (add_circle.measure_preserving_mk T t).map_eq]
+
+variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E]
+
+/-- The integral of an almost-everywhere strongly measurable function over `add_circle T` is equal
+to the integral over an interval (t, t + T] in `ℝ` of its lift to `ℝ`. -/
+protected lemma integral_preimage (t : ℝ) {f : add_circle T → E}
+  (hf : ae_strongly_measurable f volume) :
+  ∫ a in Ioc t (t + T), f a = ∫ b : add_circle T, f b :=
+begin
+  rw ← (add_circle.measure_preserving_mk T t).map_eq at ⊢ hf,
+  rw integral_map add_circle.measurable_mk'.ae_measurable hf,
+end
+
+/-- The integral of an almost-everywhere strongly measurable function over `add_circle T` is equal
+to the integral over an interval (t, t + T] in `ℝ` of its lift to `ℝ`. -/
+protected lemma interval_integral_preimage (t : ℝ) {f : add_circle T → E}
+  (hf : ae_strongly_measurable f volume) :
+  ∫ a in t..(t + T), f a = ∫ b : add_circle T, f b :=
+begin
+  rw [integral_of_le, add_circle.integral_preimage T t hf],
+  linarith [hT.out],
+end
+
+end add_circle
+
+namespace unit_add_circle
+private lemma fact_zero_lt_one : fact ((0:ℝ) < 1) := ⟨zero_lt_one⟩
+local attribute [instance] fact_zero_lt_one
+
+noncomputable instance measure_space : measure_space unit_add_circle := add_circle.measure_space 1
+
+@[simp] protected lemma measure_univ : volume (set.univ : set unit_add_circle) = 1 := by simp
+
+instance is_finite_measure : is_finite_measure (volume : measure unit_add_circle) :=
+add_circle.is_finite_measure 1
+
+/-- The covering map from `ℝ` to the "unit additive circle" `ℝ ⧸ ℤ` is measure-preserving,
+considered with respect to the standard measure (defined to be the Haar measure of total mass 1)
+on the additive circle, and with respect to the restriction of Lebsegue measure on `ℝ` to an
+interval (t, t + 1]. -/
+protected lemma measure_preserving_mk (t : ℝ) :
+  measure_preserving (coe : ℝ → unit_add_circle) (volume.restrict (Ioc t (t + 1))) :=
+add_circle.measure_preserving_mk 1 t
+
+/-- The integral of a measurable function over `unit_add_circle` is equal to the integral over an
+interval (t, t + 1] in `ℝ` of its lift to `ℝ`. -/
+protected lemma lintegral_preimage (t : ℝ) {f : unit_add_circle → ℝ≥0∞} (hf : measurable f) :
+  ∫⁻ a in Ioc t (t + 1), f a = ∫⁻ b : unit_add_circle, f b :=
+add_circle.lintegral_preimage 1 t hf
+
+variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E]
+
+/-- The integral of an almost-everywhere strongly measurable function over `unit_add_circle` is
+equal to the integral over an interval (t, t + 1] in `ℝ` of its lift to `ℝ`. -/
+protected lemma integral_preimage (t : ℝ) {f : unit_add_circle → E}
+  (hf : ae_strongly_measurable f volume) :
+  ∫ a in Ioc t (t + 1), f a = ∫ b : unit_add_circle, f b :=
+add_circle.integral_preimage 1 t hf
+
+/-- The integral of an almost-everywhere strongly measurable function over `unit_add_circle` is
+equal to the integral over an interval (t, t + 1] in `ℝ` of its lift to `ℝ`. -/
+protected lemma interval_integral_preimage (t : ℝ) {f : unit_add_circle → E}
+  (hf : ae_strongly_measurable f volume) :
+  ∫ a in t..(t + 1), f a = ∫ b : unit_add_circle, f b :=
+add_circle.interval_integral_preimage 1 t hf
+
+end unit_add_circle
+
 variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E]
 
 namespace function
 
 namespace periodic
 
-open interval_integral
-
 variables {f : ℝ → E} {T : ℝ}
 
 /-- An auxiliary lemma for a more general `function.periodic.interval_integral_add_eq`. -/
 lemma interval_integral_add_eq_of_pos (hf : periodic f T)
   (hT : 0 < T) (t s : ℝ) : ∫ x in t..t + T, f x = ∫ x in s..s + T, f x :=
 begin
-  haveI : encodable (add_subgroup.zmultiples T) := (countable_range _).to_encodable,
   simp only [integral_of_le, hT.le, le_add_iff_nonneg_right],
   haveI : vadd_invariant_measure (add_subgroup.zmultiples T) ℝ volume :=
     ⟨λ c s hs, measure_preimage_add _ _ _⟩,

src/measure_theory/measure/haar_quotient.lean

@@ -32,7 +32,7 @@ Note that a group `G` with Haar measure that is both left and right invariant is
 -/
 
 open set measure_theory topological_space measure_theory.measure
-open_locale pointwise
+open_locale pointwise nnreal
 
 variables {G : Type*} [group G] [measurable_space G] [topological_space G]
   [topological_group G] [borel_space G]
@@ -158,3 +158,20 @@ begin
     measure.map_apply meas_π, measure.restrict_apply₀' 𝓕meas, inter_comm],
   exact K.compact.measurable_set,
 end
+
+/-- Given a normal subgroup `Γ` of a topological group `G` with Haar measure `μ`, which is also
+  right-invariant, and a finite volume fundamental domain `𝓕`, the quotient map to `G ⧸ Γ` is
+  measure-preserving between appropriate multiples of Haar measure on `G` and `G ⧸ Γ`. -/
+@[to_additive measure_preserving_quotient_add_group.mk' "Given a normal subgroup `Γ` of an additive
+  topological group `G` with Haar measure `μ`, which is also right-invariant, and a finite volume
+  fundamental domain `𝓕`, the quotient map to `G ⧸ Γ` is measure-preserving between appropriate
+  multiples of Haar measure on `G` and `G ⧸ Γ`."]
+lemma measure_preserving_quotient_group.mk' [subgroup.normal Γ]
+  [measure_theory.measure.is_haar_measure μ] [μ.is_mul_right_invariant]
+  (h𝓕_finite : μ 𝓕 < ⊤) (c : ℝ≥0) (h : μ (𝓕 ∩ (quotient_group.mk' Γ) ⁻¹' K) = c) :
+  measure_preserving
+    (quotient_group.mk' Γ)
+    (μ.restrict 𝓕)
+    (c • (measure_theory.measure.haar_measure K)) :=
+{ measurable := continuous_quotient_mk.measurable,
+  map_eq := by rw [h𝓕.map_restrict_quotient K h𝓕_finite, h]; refl }

src/topology/instances/add_circle.lean

@@ -30,7 +30,6 @@ the rational circle `add_circle (1 : ℚ)`, and so we set things up more general
 ## TODO
 
  * Link with periodicity
- * Measure space structure
  * Lie group structure
  * Exponential equivalence to `circle`