Ordering.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

The ordering corollary of the joint Dickman law

The proof uses disjoint strips between interior quantiles of the continuous Dickman distribution. Every strip is a difference of two rectangles appearing in the main theorem. No weak-convergence or boundary-event hypothesis is used.

theorem OAI.JointDickman.exists_dickman_quantile line 20
def OAI.JointDickman.normalizedRectangle line 39
Source documentation
The normalized rectangle has exactly the same count as the paper's moving-power event.
```
def normalizedRectangle (a b : ℝ) (n : ℕ) : Prop :=
…
```
theorem OAI.JointDickman.realDensity_congr line 42
theorem OAI.JointDickman.normalizedRectangle_density_tendsto line 52
def OAI.JointDickman.increasingStrip line 63
Source documentation
A horizontal strip below the strict ordering diagonal.
```
def increasingStrip (a b : ℝ) (n : ℕ) : Prop :=
…
```
def OAI.JointDickman.decreasingStrip line 68
Source documentation
The reflected strip above the strict ordering diagonal.
```
def decreasingStrip (a b : ℝ) (n : ℕ) : Prop :=
…
```
theorem OAI.JointDickman.increasingStrip_subset line 72
theorem OAI.JointDickman.decreasingStrip_subset line 77
theorem OAI.JointDickman.realDensity_difference line 82
theorem OAI.JointDickman.increasingStrip_density_tendsto line 110
theorem OAI.JointDickman.decreasingStrip_density_tendsto line 134

theorem OAI.JointDickman.realDensity_sum_le_of_disjoint line 160

Source documentation

Disjoint finite collections of events give lower bounds for the density of an event containing them.

theorem realDensity_sum_le_of_disjoint {ι : Type*} [Fintype ι]
    (P : ι → ℕ → Prop) (Q : ℕ → Prop)
    (hdisj : ∀ n, 2 ≤ n → ∀ i j, P i n → P j n → i = j)
    (hsub : ∀ i n, 2 ≤ n → P i n → Q n) {X : ℝ} (hX : 0 ≤ X) :
    ∑ i, realDensity (P i) X ≤ realDensity Q X := by
…

Mentions: OAI.JointDickman.realDensity

theorem OAI.JointDickman.exists_quantile_grid line 188
theorem OAI.JointDickman.increasingStrip_grid_disjoint line 209
theorem OAI.JointDickman.decreasingStrip_grid_disjoint line 226
def OAI.JointDickman.orderingGridMass line 244
Source documentation
The mass of the finite disjoint strip approximation.
```
noncomputable def orderingGridMass (m : ℕ) : ℝ :=
…
```
theorem OAI.JointDickman.sum_fin_cast_add_one line 247
theorem OAI.JointDickman.quantile_grid_mass line 256
theorem OAI.JointDickman.orderingGridMass_tendsto line 272

theorem OAI.JointDickman.exists_ordering_lower_approximants line 287

Source documentation

Both strict orderings dominate finite strip approximations with the same explicit limiting mass. The approximations approach mass one half.

theorem exists_ordering_lower_approximants (h : JointDickmanLaw) (m : ℕ) :
    ∃ f g : ℝ → ℝ,
      Tendsto f atTop (𝓝 (orderingGridMass m)) ∧
      Tendsto g atTop (𝓝 (orderingGridMass m)) ∧
      (∀ X, 0 ≤ X → f X ≤
        realDensity (fun n => n.maxPrimeFac < (n + 1).maxPrimeFac) X) ∧
      (∀ X, 0 ≤ X → g X ≤
        realDensity (fun n => (n + 1).maxPrimeFac < n.maxPrimeFac) X) := by
…

Mentions: OAI.JointDickman.JointDickmanLaw, OAI.JointDickman.orderingGridMass, OAI.JointDickman.realDensity

theorem OAI.JointDickman.increasingOrderLaw_of_jointDickmanLaw line 323
Source documentation
Corollary 2: asymptotic independence and the continuous common marginal force the increasing ordering to have ordinary density one half.
```
theorem increasingOrderLaw_of_jointDickmanLaw (h : JointDickmanLaw) :
    IncreasingOrderLaw := by
…
```
Mentions: OAI.JointDickman.JointDickmanLaw, OAI.JointDickman.IncreasingOrderLaw
theorem OAI.JointDickman.decreasingOrderLaw_of_jointDickmanLaw line 348