PaperMain.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The joint Dickman law for consecutive integers

theorem OAI.JointDickmanPaper.joint_law line 13
Source documentation
Theorem 1: ordinary natural density, with both thresholds based at n.
Distinct definitions of this name: ComparatorChallenges/JointDickman.lean:44 (same statement text; different proof or body). Qualify references as OAI.JointDickmanPaper.joint_law@path.
```
theorem joint_law (a b : ℝ) (ha : 0 < a) (ha1 : a < 1) (hb : 0 < b) (hb1 : b < 1) :
    Tendsto (realDensity (fun n =>
      (n.maxPrimeFac : ℝ) ≤ (n : ℝ) ^ a ∧ ((n + 1).maxPrimeFac : ℝ) ≤ (n : ℝ) ^ b))
      atTop (𝓝 (Erdos970.NumberTheoryLean.Dickman.rho (1 / a) *
        Erdos970.NumberTheoryLean.Dickman.rho (1 / b))) :=
…
```
Mentions: OAI.Erdos970.NumberTheoryLean.Dickman.rho
theorem OAI.JointDickmanPaper.increasing_order line 21
Source documentation
Corollary 2: the increasing strict ordering has natural density one half.
Distinct definitions of this name: ComparatorChallenges/JointDickman.lean:52 (same statement text; different proof or body). Qualify references as OAI.JointDickmanPaper.increasing_order@path.
```
theorem increasing_order :
    Tendsto (realDensity (fun n => n.maxPrimeFac < (n + 1).maxPrimeFac))
      atTop (𝓝 (1 / 2)) :=
…
```
theorem OAI.JointDickmanPaper.decreasing_order line 27
Source documentation
The reverse strict ordering also has natural density one half.
Distinct definitions of this name: ComparatorChallenges/JointDickman.lean:58 (same statement text; different proof or body). Qualify references as OAI.JointDickmanPaper.decreasing_order@path.
```
theorem decreasing_order :
    Tendsto (realDensity (fun n => (n + 1).maxPrimeFac < n.maxPrimeFac))
      atTop (𝓝 (1 / 2)) :=
…
```