feat(dynamics/fixed_points/topology): new file (#2991)

* Move `is_fixed_pt_of_tendsto_iterate` from
  `topology.metric_space.contracting`, reformulate it without `∃`.
* Add `is_closed_fixed_points`.
* Move `dynamics.fixed_points` to `dynamics.fixed_points.basic`.

src/dynamics/circle/rotation_number/translation_number.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Yury G. Kudryashov
 -/
 import analysis.specific_limits
-import dynamics.fixed_points
 import order.iterate
 import algebra.iterate_hom
 

src/dynamics/fixed_points/topology.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Johannes Hölzl
+-/
+import dynamics.fixed_points.basic
+import topology.separation
+
+/-!
+# Topological properties of fixed points
+
+Currently this file contains two lemmas:
+
+- `is_fixed_pt_of_tendsto_iterate`: if `f^n(x) → y` and `f` is continuous at `y`, then `f y = y`;
+- `is_closed_fixed_points`: the set of fixed points of a continuous map is a closed set.
+
+## TODO
+
+fixed points, iterates
+-/
+
+variables {α : Type*} [topological_space α] [t2_space α] {f : α → α}
+
+open function filter
+open_locale topological_space
+
+/-- If the iterates `f^[n] x` converge to `y` and `f` is continuous at `y`,
+then `y` is a fixed point for `f`. -/
+lemma is_fixed_pt_of_tendsto_iterate {x y : α} (hy : tendsto (λ n, f^[n] x) at_top (𝓝 y))
+  (hf : continuous_at f y) :
+  is_fixed_pt f y :=
+begin
+  refine tendsto_nhds_unique at_top_ne_bot ((tendsto_add_at_top_iff_nat 1).1 _) hy,
+  simp only [iterate_succ' f],
+  exact hf.tendsto.comp hy
+end
+
+/-- The set of fixed points of a continuous map is a closed set. -/
+lemma is_closed_fixed_points (hf : continuous f) : is_closed (fixed_points f) :=
+is_closed_eq hf continuous_id

src/order/fixed_points.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kenny Lau
 -/
 import order.complete_lattice
-import dynamics.fixed_points
+import dynamics.fixed_points.basic
 
 /-!
 # Fixed point construction on complete lattices

src/topology/basic.lean

@@ -664,6 +664,10 @@ def continuous (f : α → β) := ∀s, is_open s → is_open (f ⁻¹' s)
 if `f x` tends to `f x₀` when `x` tends to `x₀`. -/
 def continuous_at (f : α → β) (x : α) := tendsto f (𝓝 x) (𝓝 (f x))
 
+lemma continuous_at.tendsto {f : α → β} {x : α} (h : continuous_at f x) :
+  tendsto f (𝓝 x) (𝓝 (f x)) :=
+h
+
 lemma continuous_at.preimage_mem_nhds {f : α → β} {x : α} {t : set β} (h : continuous_at f x)
   (ht : t ∈ 𝓝 (f x)) : f ⁻¹' t ∈ 𝓝 x :=
 h ht

src/topology/metric_space/contracting.lean

@@ -5,7 +5,7 @@ Authors: Rohan Mitta, Kevin Buzzard, Alistair Tucker, Johannes Hölzl, Yury Kudr
 -/
 import analysis.specific_limits
 import data.setoid.basic
-import dynamics.fixed_points
+import dynamics.fixed_points.topology
 
 /-!
 # Contracting maps
@@ -32,18 +32,6 @@ open filter function
 
 variables {α : Type*}
 
-/-- If the iterates `f^[n] x₀` converge to `x` and `f` is continuous at `x`,
-then `x` is a fixed point for `f`. -/
-lemma is_fixed_pt_of_tendsto_iterate [topological_space α] [t2_space α] {f : α → α} {x : α}
-  (hf : continuous_at f x) (hx : ∃ x₀ : α, tendsto (λ n, f^[n] x₀) at_top (𝓝 x)) :
-  is_fixed_pt f x :=
-begin
-  rcases hx with ⟨x₀, hx⟩,
-  refine tendsto_nhds_unique at_top_ne_bot ((tendsto_add_at_top_iff_nat 1).1 _) hx,
-  simp only [iterate_succ' f],
-  exact tendsto.comp hf hx
-end
-
 /-- A map is said to be `contracting_with K`, if `K < 1` and `f` is `lipschitz_with K`. -/
 def contracting_with [emetric_space α] (K : ℝ≥0) (f : α → α) :=
 (K < 1) ∧ lipschitz_with K f
@@ -109,7 +97,7 @@ have cauchy_seq (λ n, f^[n] x),
 from cauchy_seq_of_edist_le_geometric K (edist x (f x)) (ennreal.coe_lt_one_iff.2 hf.1)
   (ne_of_lt hx) (hf.to_lipschitz_with.edist_iterate_succ_le_geometric x),
 let ⟨y, hy⟩ := cauchy_seq_tendsto_of_complete this in
-⟨y, is_fixed_pt_of_tendsto_iterate hf.2.continuous.continuous_at ⟨x, hy⟩, hy,
+⟨y, is_fixed_pt_of_tendsto_iterate hy hf.2.continuous.continuous_at, hy,
   edist_le_of_edist_le_geometric_of_tendsto K (edist x (f x))
     (hf.to_lipschitz_with.edist_iterate_succ_le_geometric x) hy⟩