feat(dynamics/ergodic/add_circle): ergodicity of zsmul on the additiv…

…e circle (#17544)

src/algebra/hom/iterate.lean

@@ -164,8 +164,34 @@ smul_iterate (mul_opposite.op a) n
 lemma mul_right_iterate_apply_one : (* a)^[n] 1 = a ^ n :=
 by simp [mul_right_iterate]
 
+@[simp, to_additive]
+lemma pow_iterate (n : ℕ) (j : ℕ) : ((λ (x : G), x^n)^[j]) = λ x, x^(n^j) :=
+begin
+  letI : mul_action ℕ G :=
+  { smul := λ n g, g^n,
+    one_smul := pow_one,
+    mul_smul := λ m n g, pow_mul' g m n },
+  exact smul_iterate n j,
+end
+
 end monoid
 
+section group
+
+variables [group G]
+
+@[simp, to_additive]
+lemma zpow_iterate (n : ℤ) (j : ℕ) : ((λ (x : G), x^n)^[j]) = λ x, x^(n^j) :=
+begin
+  letI : mul_action ℤ G :=
+  { smul := λ n g, g^n,
+    one_smul := zpow_one,
+    mul_smul := λ m n g, zpow_mul' g m n },
+  exact smul_iterate n j,
+end
+
+end group
+
 section semigroup
 
 variables [semigroup G] {a b c : G}

src/data/real/ennreal.lean

@@ -1285,6 +1285,9 @@ begin
   rw [← eq_div_iff hb hb', mul_div_assoc, eq_comm],
 end
 
+lemma div_eq_one_iff {a b : ℝ≥0∞} (hb₀ : b ≠ 0) (hb₁ : b ≠ ∞) : a / b = 1 ↔ a = b :=
+⟨λ h, by rw [← (eq_div_iff hb₀ hb₁).mp h.symm, mul_one], λ h, h.symm ▸ div_self hb₀ hb₁⟩
+
 lemma inv_two_add_inv_two : (2:ℝ≥0∞)⁻¹ + 2⁻¹ = 1 :=
 by rw [← two_mul, ← div_eq_mul_inv, div_self two_ne_zero two_ne_top]
 

src/data/set/pointwise/iterate.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2022 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import data.set.pointwise.smul
+import algebra.hom.iterate
+import dynamics.fixed_points.basic
+
+/-!
+# Results about pointwise operations on sets with iteration.
+-/
+
+open_locale pointwise
+open set function
+
+/-- Let `n : ℤ` and `s` a subset of a commutative group `G` that is invariant under preimage for
+the map `x ↦ x^n`. Then `s` is invariant under the pointwise action of the subgroup of elements
+`g : G` such that `g^(n^j) = 1` for some `j : ℕ`. (This subgroup is called the Prüfer subgroup when
+ `G` is the `circle` and `n` is prime.) -/
+@[to_additive "Let `n : ℤ` and `s` a subset of an additive commutative group `G` that is invariant
+under preimage for the map `x ↦ n • x`. Then `s` is invariant under the pointwise action of the
+additive subgroup of elements `g : G` such that `(n^j) • g = 0` for some `j : ℕ`. (This additive
+subgroup is called the Prüfer subgroup when `G` is the `add_circle` and `n` is prime.)"]
+lemma smul_eq_self_of_preimage_zpow_eq_self {G : Type*} [comm_group G]
+  {n : ℤ} {s : set G} (hs : (λ x, x^n)⁻¹' s = s)
+  {g : G} {j : ℕ} (hg : g^(n^j) = 1) : g • s = s :=
+begin
+  suffices : ∀ {g' : G} (hg' : g'^(n^j) = 1), g' • s ⊆ s,
+  { refine le_antisymm (this hg) _,
+    conv_lhs { rw ← smul_inv_smul g s, },
+    replace hg : (g⁻¹)^(n^j) = 1, { rw [inv_zpow, hg, inv_one], },
+    simpa only [le_eq_subset, set_smul_subset_set_smul_iff] using this hg, },
+  rw (is_fixed_pt.preimage_iterate hs j : ((zpow_group_hom n)^[j])⁻¹' s = s).symm,
+  rintros g' hg' - ⟨y, hy, rfl⟩,
+  change ((zpow_group_hom n)^[j]) (g' * y) ∈ s,
+  replace hg' : ((zpow_group_hom n)^[j]) g' = 1, { simpa [zpow_group_hom], },
+  rwa [monoid_hom.iterate_map_mul, hg', one_mul],
+end

src/dynamics/ergodic/add_circle.lean

@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2022 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import measure_theory.group.add_circle
+import dynamics.ergodic.ergodic
+import measure_theory.covering.density_theorem
+import data.set.pointwise.iterate
+
+/-!
+# Ergodic maps of the additive circle
+
+This file contains proofs of ergodicity for maps of the additive circle.
+
+# Main definitions:
+
+ * `add_circle.ergodic_zsmul`: given `n : ℤ` such that `1 < |n|`, the self map `y ↦ n • y` on
+   the additive circle is ergodic (wrt the Haar measure).
+ * `add_circle.ergodic_nsmul`: given `n : ℕ` such that `1 < n`, the self map `y ↦ n • y` on
+   the additive circle is ergodic (wrt the Haar measure).
+
+# TODO
+
+ * Show that the map `y ↦ n • y + x` is ergodic for any `x` (and `1 < |n|`).
+
+-/
+
+open set function measure_theory measure_theory.measure filter metric
+open_locale measure_theory nnreal ennreal topological_space pointwise
+
+namespace add_circle
+
+variables {T : ℝ} [hT : fact (0 < T)]
+include hT
+
+/-- If a null-measurable subset of the circle is invariant under rotation by a family of rational
+angles with denominators tending to infinity, then it must be almost empty or almost full. -/
+lemma ae_empty_or_univ_of_forall_vadd_eq_self
+  {s : set $ add_circle T} (hs : null_measurable_set s volume)
+  {ι : Type*} {l : filter ι} [l.ne_bot] {u : ι → add_circle T}
+  (hu₁ : ∀ i, (u i) +ᵥ s = s) (hu₂ : tendsto (add_order_of ∘ u) l at_top) :
+  s =ᵐ[volume] (∅ : set $ add_circle T) ∨ s =ᵐ[volume] univ :=
+begin
+  /- Sketch of proof:
+  Assume `T = 1` for simplicity and let `μ` be the Haar measure. We may assume `s` has positive
+  measure since otherwise there is nothing to prove. In this case, by Lebesgue's density theorem,
+  there exists a point `d` of positive density. Let `Iⱼ` be the sequence of closed balls about `d`
+  of diameter `1 / nⱼ` where `nⱼ` is the additive order of `uⱼ`. Since `d` has positive density we
+  must have `μ (s ∩ Iⱼ) / μ Iⱼ → 1` along `l`. However since `s` is invariant under the action of
+  `uⱼ` and since `Iⱼ` is a fundamental domain for this action, we must have
+  `μ (s ∩ Iⱼ) = nⱼ * μ s = (μ Iⱼ) * μ s`. We thus have `μ s → 1` and thus `μ s = 1`. -/
+  set μ := (volume : measure $ add_circle T),
+  set n : ι → ℕ := add_order_of ∘ u,
+  have hT₀ : 0 < T := hT.out,
+  have hT₁ : ennreal.of_real T ≠ 0 := by simpa,
+  rw [ae_eq_empty, ae_eq_univ_iff_measure_eq hs, add_circle.measure_univ],
+  cases (eq_or_ne (μ s) 0) with h h, { exact or.inl h, },
+  right,
+  obtain ⟨d, -, hd⟩ : ∃ d, d ∈ s ∧ ∀ {ι'} {l : filter ι'} (w : ι' → add_circle T) (δ : ι' → ℝ),
+    tendsto δ l (𝓝[>] 0) → (∀ᶠ j in l, d ∈ closed_ball (w j) (1 * δ j)) →
+      tendsto (λ j, μ (s ∩ closed_ball (w j) (δ j)) / μ (closed_ball (w j) (δ j))) l (𝓝 1) :=
+    exists_mem_of_measure_ne_zero_of_ae h (is_doubling_measure.ae_tendsto_measure_inter_div μ s 1),
+  let I : ι → set (add_circle T) := λ j, closed_ball d (T / (2 * ↑(n j))),
+  replace hd : tendsto (λ j, μ (s ∩ I j) / μ (I j)) l (𝓝 1),
+  { let δ : ι → ℝ := λ j, T / (2 * ↑(n j)),
+    have hδ₀ : ∀ᶠ j in l, 0 < δ j :=
+      (hu₂.eventually_gt_at_top 0).mono (λ j hj, div_pos hT₀ $ by positivity),
+    have hδ₁ : tendsto δ l (𝓝[>] 0),
+    { refine tendsto_nhds_within_iff.mpr ⟨_, hδ₀⟩,
+      replace hu₂ : tendsto (λ j, (T⁻¹ * 2) * n j) l at_top :=
+        (tendsto_coe_nat_at_top_iff.mpr hu₂).const_mul_at_top (by positivity : 0 < T⁻¹ * 2),
+      convert hu₂.inv_tendsto_at_top,
+      ext j,
+      simp only [δ, pi.inv_apply, mul_inv_rev, inv_inv, div_eq_inv_mul, ← mul_assoc], },
+    have hw : ∀ᶠ j in l, d ∈ closed_ball d (1 * δ j) := hδ₀.mono (λ j hj, by simp [hj.le]),
+    exact hd _ δ hδ₁ hw, },
+  suffices : ∀ᶠ j in l, μ (s ∩ I j) / μ (I j) = μ s / ennreal.of_real T,
+  { replace hd := hd.congr' this,
+    rwa [tendsto_const_nhds_iff, ennreal.div_eq_one_iff hT₁ ennreal.of_real_ne_top] at hd, },
+  refine (hu₂.eventually_gt_at_top 0).mono (λ j hj, _),
+  have huj : is_of_fin_add_order (u j) := add_order_of_pos_iff.mp hj,
+  have huj' : 1 ≤ (↑(n j) : ℝ), { norm_cast, exact nat.succ_le_iff.mpr hj, },
+  have hI₀ : μ (I j) ≠ 0 := (measure_closed_ball_pos _ d $ by positivity).ne.symm,
+  have hI₁ : μ (I j) ≠ ⊤ := measure_ne_top _ _,
+  have hI₂ : μ (I j) * ↑(n j) = ennreal.of_real T,
+  { rw [volume_closed_ball, mul_div, mul_div_mul_left T _ two_ne_zero,
+      min_eq_right (div_le_self hT₀.le huj'), mul_comm, ← nsmul_eq_mul, ← ennreal.of_real_nsmul,
+      nsmul_eq_mul, mul_div_cancel'],
+    exact nat.cast_ne_zero.mpr hj.ne', },
+  rw [ennreal.div_eq_div_iff hT₁ ennreal.of_real_ne_top hI₀ hI₁,
+    volume_of_add_preimage_eq s _ (u j) d huj (hu₁ j) closed_ball_ae_eq_ball, nsmul_eq_mul,
+    ← mul_assoc, hI₂],
+end
+
+lemma ergodic_zsmul {n : ℤ} (hn : 1 < |n|) : ergodic (λ (y : add_circle T), n • y) :=
+{ ae_empty_or_univ := λ s hs hs',
+  begin
+    let u : ℕ → add_circle T := λ j, ↑(((↑1 : ℝ) / ↑(n.nat_abs^j)) * T),
+    replace hn : 1 < n.nat_abs, { rwa [int.abs_eq_nat_abs, nat.one_lt_cast] at hn, },
+    have hu₀ : ∀ j, add_order_of (u j) = n.nat_abs^j,
+    { exact λ j, add_order_of_div_of_gcd_eq_one (pow_pos (pos_of_gt hn) j) (gcd_one_left _), },
+    have hnu : ∀ j, n^j • (u j) = 0 := λ j, by rw [← add_order_of_dvd_iff_zsmul_eq_zero, hu₀,
+      int.coe_nat_pow, ← int.abs_eq_nat_abs, ← abs_pow, abs_dvd],
+    have hu₁ : ∀ j, (u j) +ᵥ s = s := λ j, vadd_eq_self_of_preimage_zsmul_eq_self hs' (hnu j),
+    have hu₂ : tendsto (λ j, add_order_of $ u j) at_top at_top,
+    { simp_rw hu₀, exact nat.tendsto_pow_at_top_at_top_of_one_lt hn, },
+    exact ae_empty_or_univ_of_forall_vadd_eq_self hs.null_measurable_set hu₁ hu₂,
+  end,
+  .. measure_preserving_zsmul volume (abs_pos.mp $ lt_trans zero_lt_one hn), }
+
+lemma ergodic_nsmul {n : ℕ} (hn : 1 < n) : ergodic (λ (y : add_circle T), n • y) :=
+ergodic_zsmul (by simp [hn] : 1 < |(n : ℤ)|)
+
+end add_circle

src/measure_theory/constructions/prod.lean

@@ -286,7 +286,7 @@ begin
       { refine eventually_of_forall (λ y, simple_func.tendsto_approx_on _ _ _),
         apply subset_closure,
         simp [-uncurry_apply_pair], } },
-    { simpa [f', hfx, integral_undef] using @tendsto_const_nhds _ _ _ (0 : E) _, } },
+    { simp [f', hfx, integral_undef], } },
   exact strongly_measurable_of_tendsto _ hf' h2f'
 end
 

src/topology/algebra/monoid.lean

@@ -101,6 +101,42 @@ lemma filter.tendsto.mul_const (b : M) {c : M} {f : α → M} {l : filter α}
   (h : tendsto (λ (k:α), f k) l (𝓝 c)) : tendsto (λ (k:α), f k * b) l (𝓝 (c * b)) :=
 h.mul tendsto_const_nhds
 
+section tendsto_nhds
+
+variables {𝕜 : Type*}
+  [preorder 𝕜] [has_zero 𝕜] [has_mul 𝕜] [topological_space 𝕜] [has_continuous_mul 𝕜]
+  {l : filter α} {f : α → 𝕜} {b c : 𝕜} (hb : 0 < b)
+
+lemma filter.tendsto_nhds_within_Ioi.const_mul [pos_mul_strict_mono 𝕜] [pos_mul_reflect_lt 𝕜]
+  (h : tendsto f l (𝓝[>] c)) :
+  tendsto (λ a, b * f a) l (𝓝[>] (b * c)) :=
+tendsto_nhds_within_of_tendsto_nhds_of_eventually_within _
+  ((tendsto_nhds_of_tendsto_nhds_within h).const_mul b) $
+  (tendsto_nhds_within_iff.mp h).2.mono (λ j, (mul_lt_mul_left hb).mpr)
+
+lemma filter.tendsto_nhds_within_Iio.const_mul [pos_mul_strict_mono 𝕜] [pos_mul_reflect_lt 𝕜]
+  (h : tendsto f l (𝓝[<] c)) :
+  tendsto (λ a, b * f a) l (𝓝[<] (b * c)) :=
+tendsto_nhds_within_of_tendsto_nhds_of_eventually_within _
+  ((tendsto_nhds_of_tendsto_nhds_within h).const_mul b) $
+  (tendsto_nhds_within_iff.mp h).2.mono (λ j, (mul_lt_mul_left hb).mpr)
+
+lemma filter.tendsto_nhds_within_Ioi.mul_const [mul_pos_strict_mono 𝕜] [mul_pos_reflect_lt 𝕜]
+  (h : tendsto f l (𝓝[>] c)) :
+  tendsto (λ a, f a * b) l (𝓝[>] (c * b)) :=
+tendsto_nhds_within_of_tendsto_nhds_of_eventually_within _
+  ((tendsto_nhds_of_tendsto_nhds_within h).mul_const b) $
+  (tendsto_nhds_within_iff.mp h).2.mono (λ j, (mul_lt_mul_right hb).mpr)
+
+lemma filter.tendsto_nhds_within_Iio.mul_const [mul_pos_strict_mono 𝕜] [mul_pos_reflect_lt 𝕜]
+  (h : tendsto f l (𝓝[<] c)) :
+  tendsto (λ a, f a * b) l (𝓝[<] (c * b)) :=
+tendsto_nhds_within_of_tendsto_nhds_of_eventually_within _
+  ((tendsto_nhds_of_tendsto_nhds_within h).mul_const b) $
+  (tendsto_nhds_within_iff.mp h).2.mono (λ j, (mul_lt_mul_right hb).mpr)
+
+end tendsto_nhds
+
 /-- Construct a unit from limits of units and their inverses. -/
 @[to_additive filter.tendsto.add_units "Construct an additive unit from limits of additive units
 and their negatives.", simps]
@@ -109,8 +145,8 @@ def filter.tendsto.units [topological_space N] [monoid N] [has_continuous_mul N]
   (h₁ : tendsto (λ x, ↑(f x)) l (𝓝 r₁)) (h₂ : tendsto (λ x, ↑(f x)⁻¹) l (𝓝 r₂)) : Nˣ :=
 { val := r₁,
   inv := r₂,
-  val_inv := tendsto_nhds_unique (by simpa using h₁.mul h₂) tendsto_const_nhds,
-  inv_val := tendsto_nhds_unique (by simpa using h₂.mul h₁) tendsto_const_nhds }
+  val_inv := by { symmetry, simpa using h₁.mul h₂ },
+  inv_val := by { symmetry, simpa using h₂.mul h₁ } }
 
 @[to_additive]
 lemma continuous_at.mul {f g : X → M} {x : X} (hf : continuous_at f x) (hg : continuous_at g x) :

src/topology/separation.lean

@@ -659,7 +659,7 @@ lemma continuous_at_of_tendsto_nhds [topological_space β] [t1_space β] {f : α
   (h : tendsto f (𝓝 a) (𝓝 b)) : continuous_at f a :=
 show tendsto f (𝓝 a) (𝓝 $ f a), by rwa eq_of_tendsto_nhds h
 
-lemma tendsto_const_nhds_iff [t1_space α] {l : filter α} [ne_bot l] {c d : α} :
+@[simp] lemma tendsto_const_nhds_iff [t1_space α] {l : filter β} [ne_bot l] {c d : α} :
   tendsto (λ x, c) l (𝓝 d) ↔ c = d :=
 by simp_rw [tendsto, filter.map_const, pure_le_nhds_iff]