ModelPartialSummation.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

The elementary prime model from the ordinary prime ideal theorem

The only number-theoretic hypothesis used here is the ordinary asymptotic for the number of primary prime elements. The power-weighted consequence is derived by Abel summation.

def OAI.CubicFirstMoment.firstMomentScaleDerivative line 21
Source documentation
The derivative of the scale appearing in the first moment.
```
def firstMomentScaleDerivative (X : ℝ) : ℝ :=
…
```
lemma OAI.CubicFirstMoment.hasDerivAt_firstMomentScale line 24
lemma OAI.CubicFirstMoment.firstMomentScaleDerivative_continuousOn line 40
lemma OAI.CubicFirstMoment.firstMomentScaleDerivative_pos line 49
lemma OAI.CubicFirstMoment.tendsto_firstMomentScale line 57
def OAI.CubicFirstMoment.normCountingSum line 71
Source documentation
Cumulative count of an arithmetic sequence collected by integer norm.
```
def normCountingSum (c : ℕ → ℝ) (X : ℝ) : ℝ :=
…
```
def OAI.CubicFirstMoment.normWeightedSum line 75
Source documentation
Its power-weighted cumulative sum.
```
def normWeightedSum (c : ℕ → ℝ) (X : ℝ) : ℝ :=
…
```
lemma OAI.CubicFirstMoment.normWeightedSum_abel line 78
lemma OAI.CubicFirstMoment.integral_div_firstMomentScale_tendsto line 116
Source documentation
Integrating an asymptotic against the derivative of the first-moment scale. This is the elementary comparison step in partial summation.
```
lemma integral_div_firstMomentScale_tendsto (f : ℝ → ℝ) (L : ℝ)
    (hint : ∀ X : ℝ, 1 ≤ X → IntervalIntegrable f volume 1 X)
    (hlim : Tendsto (fun X => f X / firstMomentScaleDerivative X) atTop (𝓝 L)) :
    Tendsto (fun X => (∫ t in 1..X, f t) / firstMomentScale X) atTop (𝓝 L) := by
…
```
Mentions: OAI.CubicFirstMoment.firstMomentScaleDerivative, OAI.CubicFirstMoment.firstMomentScale
lemma OAI.CubicFirstMoment.weighted_boundary_ratio line 194
lemma OAI.CubicFirstMoment.weighted_integrand_ratio line 206
lemma OAI.CubicFirstMoment.normWeightedSum_tendsto_of_pnt line 224
Source documentation
Abel summation of an ordinary counting asymptotic; no weighted prime estimate is among the hypotheses.
```
lemma normWeightedSum_tendsto_of_pnt (c : ℕ → ℝ) (hc₀ : c 0 = 0)
    (hpnt : Tendsto (fun X => normCountingSum c X * Real.log X / X) atTop (𝓝 1)) :
    Tendsto (fun X => normWeightedSum c X / firstMomentScale X) atTop (𝓝 (6 / 5 : ℝ)) := by
…
```
Mentions: OAI.CubicFirstMoment.normCountingSum, OAI.CubicFirstMoment.normWeightedSum, OAI.CubicFirstMoment.firstMomentScale
def OAI.CubicFirstMoment.primaryPrimeCount line 261
Source documentation
The ordinary count of primary prime elements in the norm ball.
```
def primaryPrimeCount (X : ℝ) : ℝ := (primeCutoff X).card
```
Mentions: OAI.CubicFirstMoment.primeCutoff
def OAI.CubicFirstMoment.PrimaryPrimePNT line 265
Source documentation
The ordinary prime ideal theorem, in the normalization used here. The weighted first moment is proved below, rather than included in this input.
```
def PrimaryPrimePNT : Prop :=
…
```
def OAI.CubicFirstMoment.primaryPrimeMultiplicity line 269
Source documentation
The number of primary primes having a specified integer norm.
```
def primaryPrimeMultiplicity (n : ℕ) : ℝ :=
…
```
lemma OAI.CubicFirstMoment.primaryPrimeFiber_eq line 272
lemma OAI.CubicFirstMoment.primaryPrimeMultiplicity_zero line 284
lemma OAI.CubicFirstMoment.primeNorm_sum_eq line 297
lemma OAI.CubicFirstMoment.normCountingSum_primaryPrimeMultiplicity line 314
lemma OAI.CubicFirstMoment.normWeightedSum_primaryPrimeMultiplicity line 319
lemma OAI.CubicFirstMoment.primaryPrime_weighted_asymptotic line 326
Source documentation
The power-weighted ordinary prime model, obtained solely from the ordinary PNT.
```
lemma primaryPrime_weighted_asymptotic (hpnt : PrimaryPrimePNT) :
    Tendsto (fun X => (∑ p ∈ primeCutoff X, norm p ^ (-1 / 6 : ℝ)) / firstMomentScale X)
      atTop (𝓝 (6 / 5 : ℝ)) := by
…
```
Mentions: OAI.CubicFirstMoment.PrimaryPrimePNT, OAI.CubicFirstMoment.primeCutoff, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.firstMomentScale
lemma OAI.CubicFirstMoment.primaryPrime_weighted_remainder line 341
theorem OAI.CubicFirstMoment.primeModel_asymptotic_of_PNT line 356
Source documentation
The elementary model has the claimed main term, conditionally only on ordinary prime counting.
```
theorem primeModel_asymptotic_of_PNT (hpnt : PrimaryPrimePNT) :
    (fun X => primeCutoffSum (angularPrimeModel 0) X -
      (((6 / 5 : ℝ) * cStar * firstMomentScale X : ℝ) : ℂ))
      =o[atTop] firstMomentScale := by
…
```
Mentions: OAI.CubicFirstMoment.PrimaryPrimePNT, OAI.CubicFirstMoment.primeCutoffSum, OAI.CubicFirstMoment.angularPrimeModel, OAI.CubicFirstMoment.cStar, OAI.CubicFirstMoment.firstMomentScale