FormalConjectures/ErdosProblems/999.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

4 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 999

References:

Imports (1)
  1. def Erdos999.IsApproximable x is approximable with respect to f if $$\left\lvert x-\frac{p}{q}\right\rvert < \frac{f(q)}{q}$$ has infinitely many solutions with $(p,q)=1$ line 40 source

    Source documentation

    x is approximable with respect to f if $$\left\lvert x-\frac{p}{q}\right\rvert < \frac{f(q)}{q}$$ has infinitely many solutions with $(p,q)=1$.

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

    Statement uses: Nat, Real

    Proof uses: Set.Infinite, Set.ofPred, And, LT.lt, OfNat.ofNat, Exists, Int, Eq, Int.gcd, abs, HSub.hSub, HDiv.hDiv

    15 instances, coercions and auxiliary constants left out.

    def IsApproximable (f : ℕ → ℝ) (x : ℝ) : Prop :=
…
  2. theorem Erdos999.erdos_999 For any function sorry line 55 source

    Source documentation

    For any function $f:\mathbb{N}\to \mathbb{R}_{\geq 0}$ the property that, for almost all $\alpha$ $$\left\lvert \alpha-\frac{p}{q}\right\rvert < \frac{f(q)}{q}$$ has infinitely many solutions with $(p,q)=1$, is equivalent to $$\sum_{q\geq 1}\phi(q)\frac{f(q)}{q}=\infty.$$

    The Duffin–Schaeffer conjecture. It is easy to prove that the latter follows from the former. Erdős proved this in the special case when $f(q)q$ is bounded. The full conjecture was proved by Koukoulopoulos and Maynard [KoMa20].

    depends on sorry what this means

    Statement uses: Iff, True, Nat, Real, LE.le, OfNat.ofNat, Filter.Eventually, Erdos999.IsApproximable, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Not, Summable, HDiv.hDiv, HMul.hMul, Nat.totient, SummationFilter.unconditional

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

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_999 : answer(True) ↔ ∀ f : ℕ → ℝ, (∀ q, 0 ≤ f q) →
    ((∀ᵐ x : ℝ, IsApproximable f x) ↔
      ¬ Summable fun q : ℕ ↦ (Nat.totient q : ℝ) * f q / q) := by
…

    Mentions: Erdos999.IsApproximable

  3. theorem Erdos999.erdos_999.variants.easy_direction It is easy to prove that divergence of the series follows from approximability almost everywhere (the Borel–Cantelli lemma) sorry line 63 source

    Source documentation

    It is easy to prove that divergence of the series follows from approximability almost everywhere (the Borel–Cantelli lemma).

    depends on sorry what this means

    Statement uses: Nat, Real, LE.le, OfNat.ofNat, Filter.Eventually, Erdos999.IsApproximable, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Not, Summable, HDiv.hDiv, HMul.hMul, Nat.totient, SummationFilter.unconditional

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

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_999.variants.easy_direction (f : ℕ → ℝ) (hf : ∀ q, 0 ≤ f q)
    (h : ∀ᵐ x : ℝ, IsApproximable f x) :
    ¬ Summable fun q : ℕ ↦ (Nat.totient q : ℝ) * f q / q := by
…

    Mentions: Erdos999.IsApproximable

  4. theorem Erdos999.erdos_999.variants.erdos Erdős [Er64b] proved the conjecture in the special case when $f(q)q$ is bounded sorry line 70 source

    Source documentation

    Erdős [Er64b] proved the conjecture in the special case when $f(q)q$ is bounded.

    depends on sorry what this means

    Statement uses: Nat, Real, LE.le, OfNat.ofNat, Exists, HMul.hMul, Iff, Filter.Eventually, Erdos999.IsApproximable, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Not, Summable, HDiv.hDiv, Nat.totient, SummationFilter.unconditional

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

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_999.variants.erdos (f : ℕ → ℝ) (hf : ∀ q, 0 ≤ f q)
    (hb : ∃ C : ℝ, ∀ q, f q * q ≤ C) :
    (∀ᵐ x : ℝ, IsApproximable f x) ↔
      ¬ Summable fun q : ℕ ↦ (Nat.totient q : ℝ) * f q / q := by
…

    Mentions: Erdos999.IsApproximable