Basic.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic and counting conventions for the joint Dickman law

Nat.maxPrimeFac has exactly the paper's convention P⁺(1) = 1. The counting endpoint below is an integer; the paper's real endpoint is obtained by flooring it.

def OAI.JointDickman.normalizedPrimeFactor line 19
Source documentation
The logarithmic size of the largest prime factor of n, measured at base.
```
noncomputable def normalizedPrimeFactor (base n : ℕ) : ℝ :=
…
```
def OAI.JointDickman.fixedScaleEvent line 23
Source documentation
The fixed-scale smoothness event in the proof of the joint law.
```
def fixedScaleEvent (a b : ℝ) (N n : ℕ) : Prop :=
…
```
def OAI.JointDickman.movingEvent line 28
Source documentation
The moving-threshold event in the main theorem.
```
def movingEvent (a b : ℝ) (n : ℕ) : Prop :=
…
```
def OAI.JointDickman.empiricalCount line 33
Source documentation
Ordinary counting on the paper's interval 2 ≤ n ≤ N.
Also declared: ComparatorChallenges/JointDickman.lean:28 (same declaration text).
```
noncomputable def empiricalCount (P : ℕ → Prop) (N : ℕ) : ℕ := by
…
```
def OAI.JointDickman.empiricalDensity line 38
Source documentation
Ordinary, unweighted density normalized by the counting endpoint.
```
noncomputable def empiricalDensity (P : ℕ → Prop) (N : ℕ) : ℝ :=
…
```
theorem OAI.JointDickman.maxPrimeFac_ne_succ line 41
theorem OAI.JointDickman.maxPrimeFac_pos line 51
theorem OAI.JointDickman.normalizedPrimeFactor_nonneg line 56
theorem OAI.JointDickman.normalizedPrimeFactor_le_one line 63
theorem OAI.JointDickman.normalizedPrimeFactor_succ_le line 71
Source documentation
The second coordinate can exceed one only by the indicated vanishing error.
```
theorem normalizedPrimeFactor_succ_le {n : ℕ} (hn : 2 ≤ n) :
    normalizedPrimeFactor n (n + 1) ≤
      1 + 1 / ((n : ℝ) * Real.log (n : ℝ)) := by
…
```
Mentions: OAI.JointDickman.normalizedPrimeFactor
theorem OAI.JointDickman.normalizedPrimeFactor_le_iff line 91
theorem OAI.JointDickman.normalizedPrimeFactor_lt_iff line 98
theorem OAI.JointDickman.normalizedPrimeFactor_order_iff line 105
theorem OAI.JointDickman.movingEvent_iff_normalized line 115
theorem OAI.JointDickman.fixedScaleEvent_iff_normalized line 121
theorem OAI.JointDickman.empiricalDensity_nonneg line 128
theorem OAI.JointDickman.empiricalCount_mono line 132
theorem OAI.JointDickman.empiricalDensity_mono line 141

theorem OAI.JointDickman.orderingCounts_add line 148

Source documentation

The two strict orderings partition all consecutive pairs in the counting range.

theorem orderingCounts_add (N : ℕ) :
    empiricalCount (fun n => n.maxPrimeFac < (n + 1).maxPrimeFac) N +
      empiricalCount (fun n => (n + 1).maxPrimeFac < n.maxPrimeFac) N = N - 1 := by
…

Mentions: OAI.JointDickman.empiricalCount