MainStatements.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The joint Dickman law and strict ordering densities

The moving smoothness thresholds for both consecutive integers use the base n. Counting is ordinary natural density through real endpoints.

def OAI.JointDickman.realDensity line 21
Source documentation
The paper's real-endpoint ordinary density. The natural floor is harmless for the positive endpoints in the limit, and includes exactly 2 ≤ n ≤ X.
Also declared: ComparatorChallenges/JointDickman.lean:33 (same declaration text).
```
noncomputable def realDensity (P : ℕ → Prop) (X : ℝ) : ℝ :=
…
```
theorem OAI.JointDickman.realDensity_tendsto_of_nat line 26
Source documentation
Integer-scale ordinary density gives the same limit through all real endpoints. The factor floor X / X accounts for the change of normalization.
```
theorem realDensity_tendsto_of_nat {P : ℕ → Prop} {L : ℝ}
    (h : Tendsto (empiricalDensity P) atTop (𝓝 L)) :
    Tendsto (realDensity P) atTop (𝓝 L) := by
…
```
Mentions: OAI.JointDickman.empiricalDensity, OAI.JointDickman.realDensity
def OAI.JointDickman.JointDickmanLaw line 45
Source documentation
Theorem 1 (thm:main): the moving-threshold joint Dickman law, through all real endpoints with ordinary counting. Both powers use the base n.
```
def JointDickmanLaw : Prop :=
…
```
def OAI.JointDickman.IncreasingOrderLaw line 52
Source documentation
Corollary 2 (cor:comparison), first strict ordering.
```
def IncreasingOrderLaw : Prop :=
…
```
def OAI.JointDickman.DecreasingOrderLaw line 57
Source documentation
The reverse ordering has the same density.
```
def DecreasingOrderLaw : Prop :=
…
```
theorem OAI.JointDickman.ordering_density_sum line 63
Source documentation
The sum of the two strict-ordering densities has an exact elementary formula. No joint-distribution assertion is used here.
```
theorem ordering_density_sum (X : ℝ) :
    realDensity (fun n => n.maxPrimeFac < (n + 1).maxPrimeFac) X +
      realDensity (fun n => (n + 1).maxPrimeFac < n.maxPrimeFac) X =
        ((⌊X⌋₊ - 1 : ℕ) : ℝ) / X := by
…
```
Mentions: OAI.JointDickman.realDensity
theorem OAI.JointDickman.ordering_density_sum_tendsto line 69
theorem OAI.JointDickman.increasingOrderLaw_iff_decreasingOrderLaw line 90
Source documentation
It is enough to prove either ordering density. Complementarity supplies the other; this does not establish their common value independently.
```
theorem increasingOrderLaw_iff_decreasingOrderLaw :
    IncreasingOrderLaw ↔ DecreasingOrderLaw := by
…
```
Mentions: OAI.JointDickman.IncreasingOrderLaw, OAI.JointDickman.DecreasingOrderLaw