CompactSelfIsometry.lean

1 module
2 
3 public import Mathlib.Topology.MetricSpace.Isometry
4 public import Mathlib.Topology.MetricSpace.Cauchy
5 public import Mathlib.Topology.Sequences
6 public import Mathlib.Tactic
7 
8 @[expose] public section
9 
10 namespace KomorebiPaperIX.CompactSelfIsometry
11 
12 variable {X : Type*} [MetricSpace X] {f : X → X}
13 
14 theorem iterate_isometry (hf : Isometry f) (n : ℕ) : Isometry f^[n] := by
15   induction n with
16   | zero => exact isometry_id
17   | succ n ih => exact ih.comp hf
18 
19 theorem denseRange [CompactSpace X] (hf : Isometry f) : DenseRange f := by
20   rw [Metric.denseRange_iff]
21   intro x ε hε
22   obtain ⟨a, φ, hφ, ht⟩ := CompactSpace.tendsto_subseq (fun n : ℕ => f^[n] x)
23   obtain ⟨N, hN⟩ := Metric.cauchySeq_iff.mp ht.cauchySeq ε hε
24   have hclose := hN N le_rfl (N + 1) (by omega)
25   have hlt : φ N < φ (N + 1) := hφ (by omega)
26   let k := φ (N + 1) - φ N
27   have hk : 0 < k := by dsimp [k]; omega
28   have heq : φ N + k = φ (N + 1) := by dsimp [k]; omega
29   have hd : dist x (f^[k] x) < ε := by
30     rw [← (iterate_isometry hf (φ N)).dist_eq]
31     simpa only [Function.comp_apply, ← Function.iterate_add_apply, heq] using hclose
32   obtain ⟨l, hl⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hk)
33   refine ⟨f^[l] x, ?_⟩
34   simpa only [hl, Function.iterate_succ_apply'] using hd
35 
36 theorem surjective [CompactSpace X] (hf : Isometry f) : Function.Surjective f := by
37   intro x
38   have hx := denseRange hf x
39   rw [(isCompact_range hf.continuous).isClosed.closure_eq] at hx
40   exact hx
41 
42 end KomorebiPaperIX.CompactSelfIsometry

Back to source controls