FormalConjecturesForMathlib/NumberTheory/SmoothScale.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

1 declarations, 0 contain sorry, 0 declared as axioms

The scale L

L n = exp (sqrt (log n * log (log n))) is the scale that shows up in smooth-number and covering-system estimates, usually as n ^ (1 + o(1)) corrections of the form L n ^ (-1 + o(1)).

Imports (2)
Imported by 1 file
  1. def scaleL The scale $L(n)=\exp(\sqrt{\log n\log\log n})$ line 34 source

    Source documentation

    The scale $L(n)=\exp(\sqrt{\log n\log\log n})$.

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

    Statement uses: Nat, Real

    Proof uses: Real.exp, Real.sqrt, HMul.hMul, Real.log

    4 instances, coercions and auxiliary constants left out.

    noncomputable def scaleL (n : ℕ) : ℝ := exp (sqrt (log n * log (log n)))