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

Reference: erdosproblems.com/126

Imports (1)
  1. def Erdos126.IsMaximalAddFactorsCard line 32 source

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

    Statement uses: Nat

    Proof uses: IsGreatest, Set.ofPred, Finset, Eq, Finset.card, LE.le, Nat.primeFactors, Finset.prod, Prod, Finset.offDiag, Erdos126.IsMaximalAddFactorsCard.match_1, HAdd.hAdd

    4 instances, coercions and auxiliary constants left out.

  2. theorem Erdos126.erdos_126 sorry line 47 source

    depends on sorry what this means

    Statement uses: Iff, True, Nat, Erdos126.IsMaximalAddFactorsCard, Filter.Tendsto, Real, HDiv.hDiv, Real.log, Filter.atTop

    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 Erdos126.erdos_126.variants.IsBigO Documented declaration: IsBigO sorry line 60 source

    Source documentation

    Erdős and Turán proved [ErTu34] in their first joint paper that $$ \log n \ll f(n) \ll \frac{n}{\log n} $$

    [ErTu34] Erdős, Paul and Turan, Paul, On a Problem in the Elementary Theory of Numbers. Amer. Math. Monthly (1934), 608-611.

    depends on sorry what this means

    Statement uses: Nat, Erdos126.IsMaximalAddFactorsCard, And, Asymptotics.IsBigO, Real, Filter.atTop, Real.log, HDiv.hDiv

    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_126.variants.IsBigO
    (f : ℕ → ℕ)
    (hf : IsMaximalAddFactorsCard f) :
    ((fun (n : ℕ) => Real.log n) =O[atTop] fun (n : ℕ) => (f n : ℝ)) ∧
      (fun (n : ℕ) => (f n : ℝ)) =O[atTop] fun (n : ℕ) => n / Real.log n := by
…

    Mentions: Erdos126.IsMaximalAddFactorsCard

  4. theorem Erdos126.erdos_126.variants.isLittleO Erdős says that $f(n) = o(\frac{n}{\log n})$ has never been proved sorry line 71 source

    Source documentation

    Erdős says that $f(n) = o(\frac{n}{\log n})$ has never been proved.

    depends on sorry what this means

    Statement uses: Nat, Erdos126.IsMaximalAddFactorsCard, Asymptotics.IsLittleO, Real, Filter.atTop, HDiv.hDiv, Real.log

    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_126.variants.isLittleO
    (f : ℕ → ℕ)
    (hf : IsMaximalAddFactorsCard f) :
    (fun (n : ℕ) => (f n : ℝ)) =o[atTop] (fun (n : ℕ) => n / Real.log n) := by
…

    Mentions: Erdos126.IsMaximalAddFactorsCard