FormalConjectures/ErdosProblems/995.lean

GitHub source file

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

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

3 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 995

References:

Let $n_1 < n_2 < \cdots$ be a lacunary sequence of integers and $f \in L^2([0,1])$ with $\int_0^1 f = 0$. Estimate the growth of $$S_N(\alpha) = \sum_{k \le N} f(\{\alpha n_k\})$$ for almost all $\alpha$, where $\{\cdot\}$ denotes the fractional part. In particular, is it true that $S_N(\alpha) = o\!\left(N \sqrt{\log\log N}\right)$ for almost all $\alpha$?

Erdős [Er49] constructed a lacunary sequence and a mean-zero $f \in L^2([0,1])$ for which, for every $\varepsilon > 0$, $\limsup_N S_N(\alpha) / (N (\log\log N)^{1/2 - \varepsilon}) = \infty$ for almost all $\alpha$, and believed this lower bound to be close to the truth.

The mean-zero hypothesis $\int_0^1 f = 0$ is the natural normalisation: otherwise the sum has a linear main term coming from the average of $f$.

Imports (1)
  1. def Erdos995.partialSum The partial sum $S_N(\alpha) = \sum_{k < N} f(\{\alpha n_k\})$ line 49 source

    Source documentation

    The partial sum $S_N(\alpha) = \sum_{k < N} f(\{\alpha n_k\})$.

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

    Statement uses: Nat, Real

    Proof uses: Finset.sum, Finset.range, Int.fract, HMul.hMul

    8 instances, coercions and auxiliary constants left out.

    noncomputable def partialSum (n : ℕ → ℕ) (f : ℝ → ℝ) (α : ℝ) (N : ℕ) : ℝ :=
…
  2. theorem Erdos995.erdos_995 Erdős Problem 995: For every lacunary sequence sorry line 60 source

    Source documentation

    Erdős Problem 995:

    For every lacunary sequence $(n_k)$ of integers and every $f \in L^2([0,1])$ with $\int_0^1 f = 0$, is it true that for almost all $\alpha$, $$\sum_{k < N} f(\{\alpha n_k\}) = o\!\left(N \sqrt{\log\log N}\right)?$$

    depends on sorry what this means

    Statement uses: Iff, True, Nat, IsLacunary, Real, MeasureTheory.MemLp, OfNat.ofNat, ENNReal, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Icc, Eq, intervalIntegral, Filter.Eventually, Asymptotics.IsLittleO, Filter.atTop, Erdos995.partialSum, HMul.hMul, Real.sqrt, Real.log and 2 more

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

    78 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_995 :
    answer(sorry) ↔
      ∀ (n : ℕ → ℕ), IsLacunary n → ∀ (f : ℝ → ℝ),
        MemLp f 2 (volume.restrict (Icc (0 : ℝ) 1)) →
        ∫ x in (0 : ℝ)..1, f x = 0 →
        ∀ᵐ α ∂(volume.restrict (Icc (0 : ℝ) 1)),
          partialSum n f α =o[atTop] fun N => (N : ℝ) * Real.sqrt (Real.log (Real.log N)) := by
…

    Mentions: IsLacunary, Erdos995.partialSum

  3. theorem Erdos995.erdos_995.variants.erdos_lower_bound Erdős [Er49] showed the growth cannot be pushed below sorry line 77 source

    Source documentation

    Erdős [Er49] showed the growth cannot be pushed below $N (\log\log N)^{1/2}$ by more than an arbitrarily small power: there is a lacunary sequence and a mean-zero $f \in L^2([0,1])$ such that for every $\varepsilon > 0$, for almost all $\alpha$, $$\limsup_{N \to \infty} \frac{\sum_{k < N} f(\{\alpha n_k\})}{N (\log\log N)^{1/2 - \varepsilon}} = \infty.$$

    depends on sorry what this means

    Statement uses: Exists, Nat, And, IsLacunary, Real, MeasureTheory.MemLp, OfNat.ofNat, ENNReal, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Icc, Eq, intervalIntegral, GT.gt, Filter.Eventually, EReal, Filter.limsup, HDiv.hDiv, Erdos995.partialSum, HMul.hMul and 7 more

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

    104 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_995.variants.erdos_lower_bound :
    ∃ (n : ℕ → ℕ), IsLacunary n ∧ ∃ (f : ℝ → ℝ),
      MemLp f 2 (volume.restrict (Icc (0 : ℝ) 1)) ∧
      ∫ x in (0 : ℝ)..1, f x = 0 ∧
      ∀ ε > (0 : ℝ),
        ∀ᵐ α ∂(volume.restrict (Icc (0 : ℝ) 1)),
          atTop.limsup (fun N => (((partialSum n f α N) /
            ((N : ℝ) * (Real.log (Real.log N)) ^ ((1 : ℝ) / 2 - ε)) : ℝ) : EReal)) = ⊤ := by
…

    Mentions: IsLacunary, Erdos995.partialSum