Equidistribution.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

8 declarations, 4 contain sorry, 0 declared as axioms

Equidistributed Sequences

Corollary 4.2 of Chapter 1 states that the sequence $(x^n), n = 1, 2, ... ,$ is equidistributed modulo 1 for almost all x > 1. And a little bit further down: "one does not know whether sequences such as $(e^n)$, $(π^n)$, or even $((\frac 3 2)^n)$" are equidistributed modulo 1 or not.

References:

Uniform Distribution of Sequences by L. Kuipers and H. Niederreiter, 1974
Wikipedia
[Mat80] de Mathan, Bernard. "Numbers contravening a condition in density modulo 1." Acta Mathematica Hungarica 36.3-4 (1980): 237-241.
[Pol79] Pollington, Andrew Douglas. "On the density of sequence $\{n_ {k}\xi\} $." Illinois Journal of Mathematics 23.4 (1979): 511-515.

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100OpenSet1.lean

def Equidistribution.IsAccumulationPoint A point x is an accumulation point of a sequence s_0, s_1, ... if any neighbourhood of x contains a point of the sequence distinct from x line 48 source
Source documentation
A point x is an accumulation point of a sequence s_0, s_1, ... if any neighbourhood of x contains a point of the sequence distinct from x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat
Proof uses: Membership.mem, Set, closure, SDiff.sdiff, Set.range, Singleton.singleton
6 instances, coercions and auxiliary constants left out.
```
def IsAccumulationPoint (x : ℝ) (s : ℕ → ℝ) : Prop :=
…
```
theorem Equidistribution.isAccumulationPoint_exists_subsequence_tendsto If a point x is an accumulation point of a sequence s_0, s_1, ... then there is a subsequence of s that tends to x line 56 source
Source documentation
If a point x is an accumulation point of a sequence s_0, s_1, ... then there is a subsequence of s that tends to x

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, Equidistribution.IsAccumulationPoint, Exists, And, StrictMono, Filter.Tendsto, Function.comp, Filter.atTop, nhds
Proof uses: MapClusterPt.tendsto_subseq, Iff.mpr, MapClusterPt, Set, Membership.mem, Filter, Filter.Frequently, mapClusterPt_iff_frequently, Eq.mpr, LE.le, id, Eq, congrArg, propext, Filter.frequently_atTop, Classical.byContradiction, Not, Inter.inter, Set.iInter, Finset and 34 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem isAccumulationPoint_exists_subsequence_tendsto
    (x : ℝ) (s : ℕ → ℝ) (hx : IsAccumulationPoint x s) :
    ∃ (u : ℕ → ℕ), StrictMono u ∧ Filter.atTop.Tendsto (s ∘ u) (𝓝 x) := by
…
```
Mentions: Equidistribution.IsAccumulationPoint
theorem Equidistribution.isEquidistributedModuloOne_three_halves_pow The sequence (3/2)^n is equidistributed modulo 1 sorry line 81 source
Source documentation
The sequence (3/2)^n is equidistributed modulo 1.

depends on sorry what this means
Statement uses: IsEquidistributedModuloOne, Nat, HPow.hPow, Real, HDiv.hDiv, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isEquidistributedModuloOne_three_halves_pow :
    IsEquidistributedModuloOne (fun n => (3 / 2 : ℝ)^n) := by
…
```
Mentions: IsEquidistributedModuloOne
theorem Equidistribution.isEquidistributedModuloOne_transcendental_three_halves_pow It is not true that for every transcendental number x the sequence x * (3 / 2) ^ n is equidistributed modulo 1 sorry line 95 source
Source documentation
It is not true that for every transcendental number x the sequence x * (3 / 2) ^ n is equidistributed modulo 1. The sequence (3 / 2) ^ n is lacunary, so by the theorem of Pollington [Pol79] and de Mathan [Mat80] the set of real numbers x for which x * (3 / 2) ^ n is not even dense modulo 1 has Hausdorff dimension 1. This set is uncountable, so it contains transcendental numbers. Alternatively, an elementary nested-interval construction (see issue #5003) gives a Cantor set of x with Int.fract (x * (3 / 2) ^ (8 * j)) ∈ [0, 1 / 10] for all j, which already rules out equidistribution for uncountably many, hence some transcendental, x. By Koksma's metric theorem (Kuipers–Niederreiter, Chapter 1, Section 4), the sequence x * (3 / 2) ^ n is equidistributed modulo 1 for almost all x.

depends on sorry what this means
Statement uses: Not, Real, Transcendental, Rat, IsEquidistributedModuloOne, Nat, HMul.hMul, HPow.hPow, HDiv.hDiv, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
50 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isEquidistributedModuloOne_transcendental_three_halves_pow :
    ¬ ∀ x : ℝ, Transcendental ℚ x →
      IsEquidistributedModuloOne (fun n ↦ x * (3 / 2 : ℝ) ^ n) := by
…
```
Mentions: IsEquidistributedModuloOne
theorem Equidistribution.isAccumulationPoint_three_halves_pow_infinite The sequence (3/2)^n has infinitely many accumulation points modulo 1 sorry line 104 source
Source documentation
The sequence (3/2)^n has infinitely many accumulation points modulo 1.

depends on sorry what this means
Statement uses: Set.Infinite, Real, Set.ofPred, Equidistribution.IsAccumulationPoint, Nat, Int.fract, HPow.hPow, HDiv.hDiv, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isAccumulationPoint_three_halves_pow_infinite :
    {x | IsAccumulationPoint x (fun n => Int.fract <| (3 / 2 : ℝ)^n)}.Infinite := by
…
```
Mentions: Equidistribution.IsAccumulationPoint
theorem Equidistribution.isAccumulationPoint_three_halves_pow Find an accumulation point of the sequence (3/2)^n modulo 1 sorry line 112 source
Source documentation
Find an accumulation point of the sequence (3/2)^n modulo 1.

depends on sorry what this means
Statement uses: Equidistribution.IsAccumulationPoint, sorryAx, Real, Bool.false, Nat, Int.fract, HPow.hPow, HDiv.hDiv, OfNat.ofNat
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isAccumulationPoint_three_halves_pow :
    IsAccumulationPoint answer(sorry) (fun n => Int.fract <| (3 / 2 : ℝ)^n) := by
…
```
Mentions: Equidistribution.IsAccumulationPoint
theorem Equidistribution.fract_three_halves_pow_injective The values of (3/2)^n modulo 1 are pairwise distinct: if (3/2)^n - (3/2)^m were an integer for m < n, then 3^n - 3^m * 2^(n - m) would be even line 119 source
Source documentation
The values of (3/2)^n modulo 1 are pairwise distinct: if (3/2)^n - (3/2)^m were an integer for m < n, then 3^n - 3^m * 2^(n - m) would be even.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Nat, Real, Int.fract, HPow.hPow, HDiv.hDiv, OfNat.ofNat
Proof uses: Eq, Decidable.byContradiction, Not, LT.lt, Or, False, Classical.em, Int, HSub.hSub, Exists, Iff.mp, Int.fract_eq_fract, Ne, ne_of_gt, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool and 36 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
theorem fract_three_halves_pow_injective :
    Function.Injective fun n : ℕ => Int.fract ((3 / 2 : ℝ) ^ n) := by
…
```
theorem Equidistribution.isAccumulationPoint_three_halves_pow_exists 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 line 148 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Real, Equidistribution.IsAccumulationPoint, Nat, Int.fract, HPow.hPow, HDiv.hDiv, OfNat.ofNat
Proof uses: Set.Infinite, Set.range, Set.infinite_range_of_injective, Equidistribution.fract_three_halves_pow_injective, LE.le, Set, Set.Icc, Membership.mem, Eq, And.intro, Int.fract_nonneg, LT.lt.le, Int.fract_lt_one, And, AccPt, Filter.principal, Set.Infinite.exists_accPt_of_subset_isCompact, CompactIccSpace.isCompact_Icc, Exists.intro, Iff.mpr and 7 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem isAccumulationPoint_three_halves_pow_exists :
    ∃ p, (IsAccumulationPoint p (fun n => Int.fract <| (3 / 2 : ℝ)^n)) := by
…
```
Mentions: Equidistribution.IsAccumulationPoint