feat(measure_theory/integral): `∫ x in b..b+a, f x = ∫ x in c..c + a,…

… f x` for a periodic `f` (#10477)

src/algebra/periodic.lean

@@ -7,6 +7,7 @@ import algebra.field.opposite
 import algebra.module.basic
 import algebra.order.archimedean
 import data.int.parity
+import group_theory.subgroup.basic
 
 /-!
 # Periodicity
@@ -277,6 +278,16 @@ lemma periodic_with_period_zero [add_zero_class α]
   periodic f 0 :=
 λ x, by rw add_zero
 
+lemma periodic.map_vadd_zmultiples [add_comm_group α] (hf : periodic f c)
+  (a : add_subgroup.zmultiples c) (x : α) :
+  f (a +ᵥ x) = f x :=
+by { rcases a with ⟨_, m, rfl⟩, simp [add_subgroup.vadd_def, add_comm _ x, hf.zsmul m x] }
+
+lemma periodic.map_vadd_multiples [add_comm_monoid α] (hf : periodic f c)
+  (a : add_submonoid.multiples c) (x : α) :
+  f (a +ᵥ x) = f x :=
+by { rcases a with ⟨_, m, rfl⟩, simp [add_submonoid.vadd_def, add_comm _ x, hf.nsmul m x] }
+
 /-! ### Antiperiodicity -/
 
 /-- A function `f` is said to be `antiperiodic` with antiperiod `c` if for all `x`,

src/group_theory/coset.lean

@@ -275,6 +275,10 @@ lemma induction_on' {C : α ⧸ s → Prop} (x : α ⧸ s)
   (H : ∀ z : α, C z) : C x :=
 quotient.induction_on' x H
 
+@[simp, to_additive]
+lemma quotient_lift_on_coe {β} (f : α → β) (h) (x : α) :
+  quotient.lift_on' (x : α ⧸ s) f h = f x := rfl
+
 @[to_additive]
 lemma forall_coe {C : α ⧸ s → Prop} :
   (∀ x : α ⧸ s, C x) ↔ ∀ x : α, C x :=

src/group_theory/quotient_group.lean

@@ -137,6 +137,10 @@ lemma coe_mul (a b : G) : ((a * b : G) : Q) = a * b := rfl
 @[simp, to_additive quotient_add_group.coe_neg]
 lemma coe_inv (a : G) : ((a⁻¹ : G) : Q) = a⁻¹ := rfl
 
+-- TODO: make it `rfl`
+@[simp, to_additive quotient_add_group.coe_sub]
+lemma coe_div (a b : G) : ((a / b : G) : Q) = a / b := by simp [div_eq_mul_inv]
+
 @[simp] lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n :=
 (mk' N).map_pow a n
 

src/measure_theory/group/arithmetic.lean

@@ -437,6 +437,17 @@ instance has_measurable_smul₂_of_mul (M : Type*) [has_mul M] [measurable_space
   has_measurable_smul₂ M M :=
 ⟨measurable_mul⟩
 
+@[to_additive] instance submonoid.has_measurable_smul {M α} [measurable_space M]
+  [measurable_space α] [monoid M] [mul_action M α] [has_measurable_smul M α] (s : submonoid M) :
+  has_measurable_smul s α :=
+⟨λ c, by simpa only using measurable_const_smul (c : M),
+  λ x, (measurable_smul_const x : measurable (λ c : M, c • x)).comp measurable_subtype_coe⟩
+
+@[to_additive] instance subgroup.has_measurable_smul {G α} [measurable_space G]
+  [measurable_space α] [group G] [mul_action G α] [has_measurable_smul G α] (s : subgroup G) :
+  has_measurable_smul s α :=
+s.to_submonoid.has_measurable_smul
+
 section smul
 
 variables {M β α : Type*} [measurable_space M] [measurable_space β] [has_scalar M β]

src/measure_theory/group/fundamental_domain.lean

@@ -28,7 +28,7 @@ We also generate additive versions of all theorems in this file using the `to_ad
 -/
 
 open_locale ennreal pointwise topological_space nnreal ennreal measure_theory
-open measure_theory measure_theory.measure set function topological_space
+open measure_theory measure_theory.measure set function topological_space filter
 
 namespace measure_theory
 
@@ -56,9 +56,25 @@ namespace is_fundamental_domain
 variables {G α E : Type*} [group G] [mul_action G α] [measurable_space α]
   [normed_group E] {s t : set α} {μ : measure α}
 
+/-- If for each `x : α`, exactly one of `g • x`, `g : G`, belongs to a measurable set `s`, then `s`
+is a fundamental domain for the action of `G` on `α`. -/
+@[to_additive "/- If for each `x : α`, exactly one of `g +ᵥ x`, `g : G`, belongs to a measurable set
+`s`, then `s` is a fundamental domain for the additive action of `G` on `α`. -/"]
+lemma mk' (h_meas : measurable_set s) (h_exists : ∀ x : α, ∃! g : G, g • x ∈ s) :
+  is_fundamental_domain G s μ :=
+{ measurable_set := h_meas,
+  ae_covers := eventually_of_forall $ λ x, (h_exists x).exists,
+  ae_disjoint := λ g hne,
+    begin
+      suffices : g • s ∩ s = ∅, by rw [this, measure_empty],
+      refine eq_empty_iff_forall_not_mem.2 _, rintro _ ⟨⟨x, hx, rfl⟩, hgx⟩,
+      rw ← one_smul G x at hx,
+      exact hne ((h_exists x).unique hgx hx)
+    end }
+
 @[to_additive] lemma Union_smul_ae_eq (h : is_fundamental_domain G s μ) :
   (⋃ g : G, g • s) =ᵐ[μ] univ :=
-filter.eventually_eq_univ.2 $ h.ae_covers.mono $
+eventually_eq_univ.2 $ h.ae_covers.mono $
   λ x ⟨g, hg⟩, mem_Union.2 ⟨g⁻¹, _, hg, inv_smul_smul _ _⟩
 
 @[to_additive] lemma mono (h : is_fundamental_domain G s μ) {ν : measure α} (hle : ν ≪ μ) :

src/measure_theory/integral/periodic.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import measure_theory.group.fundamental_domain
+import measure_theory.integral.interval_integral
+
+/-!
+# Integrals of periodic functions
+
+In this file we prove that `∫ x in b..b + a, f x = ∫ x in c..c + a, f x` for any (not necessarily
+measurable) function periodic function with period `a`.
+-/
+
+open set function measure_theory measure_theory.measure topological_space
+open_locale measure_theory
+
+lemma is_add_fundamental_domain_Ioc {a : ℝ} (ha : 0 < a) (b : ℝ) (μ : measure ℝ . volume_tac) :
+  is_add_fundamental_domain (add_subgroup.zmultiples a) (Ioc b (b + a)) μ :=
+begin
+  refine is_add_fundamental_domain.mk' measurable_set_Ioc (λ x, _),
+  have : bijective (cod_restrict (λ n : ℤ, n • a) (add_subgroup.zmultiples a) _),
+    from (equiv.of_injective (λ n : ℤ, n • a) (zsmul_strict_mono_left ha).injective).bijective,
+  refine this.exists_unique_iff.2 _,
+  simpa only [add_comm x] using exists_unique_add_zsmul_mem_Ioc ha x b
+end
+
+variables {E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [complete_space E] [second_countable_topology E]
+
+namespace function
+
+namespace periodic
+
+/-- An auxiliary lemma for a more general `function.periodic.interval_integral_add_eq`. -/
+lemma interval_integral_add_eq_of_pos {f : ℝ → E} {a : ℝ} (hf : periodic f a)
+  (ha : 0 < a) (b c : ℝ) : ∫ x in b..b + a, f x = ∫ x in c..c + a, f x :=
+begin
+  haveI : encodable (add_subgroup.zmultiples a) := (countable_range _).to_encodable,
+  simp only [interval_integral.integral_of_le, ha.le, le_add_iff_nonneg_right],
+  haveI : vadd_invariant_measure (add_subgroup.zmultiples a) ℝ volume :=
+    ⟨λ c s hs, real.volume_preimage_add_left _ _⟩,
+  exact (is_add_fundamental_domain_Ioc ha b).set_integral_eq
+    (is_add_fundamental_domain_Ioc ha c) hf.map_vadd_zmultiples
+end
+
+/-- If `f` is a periodic function with period `a`, then its integral over `[b, b + a]` does not
+depend on `b`. -/
+lemma interval_integral_add_eq {f : ℝ → E} {a : ℝ} (hf : periodic f a)
+  (b c : ℝ) : ∫ x in b..b + a, f x = ∫ x in c..c + a, f x :=
+begin
+  rcases lt_trichotomy 0 a with (ha|rfl|ha),
+  { exact hf.interval_integral_add_eq_of_pos ha b c },
+  { simp },
+  { rw [← neg_inj, ← interval_integral.integral_symm, ← interval_integral.integral_symm],
+    simpa only [← sub_eq_add_neg, add_sub_cancel]
+      using (hf.neg.interval_integral_add_eq_of_pos (neg_pos.2 ha) (b + a) (c + a)) }
+end
+
+end periodic
+
+end function