FormalConjectures/ErdosProblems/997.lean

GitHub source file

4 declarations, 3 contain sorry, 0 declared as axioms

1. def Erdos997.IsWellDistributed Call line 52 source

   Source documentation

   Call $x_1,x_2,\ldots \in (0,1)$ well-distributed if, for every $\epsilon>0$, if $k$ is sufficiently large then, for all $n>0$ and intervals $I\subseteq [0,1]$, $\lvert \# \{ n < m\leq n+k : x_m\in I\} - \lvert I\rvert k\rvert < \epsilon k.$

   The notion of a well-distributed sequence was introduced by Hlawka and Petersen [Hl55].

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Real

   Proof uses: GT.gt, OfNat.ofNat, Filter.Eventually, LE.le, Finset, Finset.filter, Membership.mem, Set, Set.Ico, Finset.Ioc, HAdd.hAdd, LT.lt, abs, HSub.hSub, Finset.card, HMul.hMul, Filter.atTop

   23 instances, coercions and auxiliary constants left out.

   def IsWellDistributed (x : ℕ → ℝ) : Prop :=
   …

2. theorem Erdos997.erdos_997 sorry line 67 source

   depends on sorry what this means

   Statement uses: Iff, True, Real, Not, Erdos997.IsWellDistributed, Nat, Int.fract, HMul.hMul, Nat.nth, Nat.Prime

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   15 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

3. theorem Erdos997.erdos_997.variants.lacunary Erdős proved that, if $n_k$ is a lacunary sequence, then the sequence $\{ \alpha n_k\}$ is not well-distributed for almost all $\alpha$ sorry line 77 source

   Source documentation

   Erdős proved that, if $n_k$ is a lacunary sequence, then the sequence $\{ \alpha n_k\}$ is not well-distributed for almost all $\alpha$.

   depends on sorry what this means

   Statement uses: Nat, IsLacunary, Filter.Eventually, Real, Not, Erdos997.IsWellDistributed, Int.fract, HMul.hMul, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   23 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_997.variants.lacunary (n : ℕ → ℕ) (h : IsLacunary n) :
       ∀ᵐ α, ¬ IsWellDistributed (fun k ↦ Int.fract (α * (n k : ℝ))) := by
   …

   Mentions: IsLacunary, Erdos997.IsWellDistributed

4. theorem Erdos997.erdos_997.variants.irrational He also claimed in [Er64b] to have proved that there exists an irrational $\alpha$ for which $\{\alpha p_n\}$ is not well-distributed sorry line 90 source

   Source documentation

   He also claimed in [Er64b] to have proved that there exists an irrational $\alpha$ for which $\{\alpha p_n\}$ is not well-distributed. He later retracted this claim in [Er85e], saying "The theorem is no doubt correct and perhaps will not be difficult to prove but I never was able to reconstruct my 'proof' which perhaps never existed."

   The existence of such an $\alpha$ was established by Champagne, Le, Liu, and Wooley [CLLW24].

   depends on sorry what this means

   Statement uses: Exists, Real, And, Irrational, Not, Erdos997.IsWellDistributed, Nat, Int.fract, HMul.hMul, Nat.nth, Nat.Prime

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   15 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_997.variants.irrational :
       ∃ α : ℝ, Irrational α ∧
         ¬ IsWellDistributed (fun n ↦ Int.fract (α * (n.nth Nat.Prime))) := by
   …

   Mentions: Erdos997.IsWellDistributed