AngularModel.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

The sharp fixed-angular prime model

The input is the explicit published Hecke prime estimate, not a weighted prime-model asymptotic. Partial summation with x^(-1/6)/log x derives the required little-oh at the sharp first-moment scale.

lemma OAI.CubicFirstMoment.fixedAngular_chebyshev_div_tendsto_zero line 19
def OAI.CubicFirstMoment.angularAbelWeight line 47
def OAI.CubicFirstMoment.angularAbelDerivative line 49
lemma OAI.CubicFirstMoment.hasDerivAt_angularAbelWeight line 52
lemma OAI.CubicFirstMoment.angularAbelDerivative_continuousOn line 69
lemma OAI.CubicFirstMoment.angularAbel_boundary_ratio line 79
lemma OAI.CubicFirstMoment.angularAbel_integrand_ratio line 89
lemma OAI.CubicFirstMoment.integral_from_two_div_scale_tendsto_zero line 111
Source documentation
The version of scale comparison starting at two, where the logarithmic Abel weight is regular. Only its limit-zero case is needed.
```
lemma integral_from_two_div_scale_tendsto_zero (f : ℝ → ℝ)
    (hint : ∀ X : ℝ, 2 ≤ X → IntervalIntegrable f volume 2 X)
    (hlim : Tendsto (fun X => f X / firstMomentScaleDerivative X) atTop (𝓝 0)) :
    Tendsto (fun X => (∫ t in 2..X, f t) / firstMomentScale X) atTop (𝓝 0) := by
…
```
Mentions: OAI.CubicFirstMoment.firstMomentScaleDerivative, OAI.CubicFirstMoment.firstMomentScale
def OAI.CubicFirstMoment.angularChebyshevIntegrand line 177
lemma OAI.CubicFirstMoment.angularChebyshevIntegrand_intervalIntegrable line 180
lemma OAI.CubicFirstMoment.angularChebyshev_integral_div_scale_tendsto_zero line 197
lemma OAI.CubicFirstMoment.primaryPrime_norm_gt_one line 218
lemma OAI.CubicFirstMoment.primeNormCoefficient_log line 229
lemma OAI.CubicFirstMoment.primeNormCoefficient_weighted_prefix line 241
def OAI.CubicFirstMoment.angularWeightedPrimeSum line 255
Source documentation
The angular power-weighted sum before multiplying by cStar.
```
def angularWeightedPrimeSum (ℓ : ℤ) (X : ℝ) : ℂ :=
…
```
lemma OAI.CubicFirstMoment.angularWeightedPrimeSum_abel line 258
lemma OAI.CubicFirstMoment.angularWeightedPrimeSum_norm_le line 304
theorem OAI.CubicFirstMoment.angularWeightedPrimeSum_isLittleO line 327
theorem OAI.CubicFirstMoment.angularPrimeModel_isLittleO line 358
Source documentation
The sharp nonzero-angular prime model is negligible at the precise X^(5/6)/log X scale, derived from the published explicit Hecke input.
```
theorem angularPrimeModel_isLittleO (hEF : FixedAngularPrimeExplicitEstimate)
    (ℓ : ℤ) (hℓ : ℓ ≠ 0) :
    primeCutoffSum (angularPrimeModel ℓ) =o[atTop] firstMomentScale := by
…
```
Mentions: OAI.CubicFirstMoment.FixedAngularPrimeExplicitEstimate, OAI.CubicFirstMoment.primeCutoffSum, OAI.CubicFirstMoment.angularPrimeModel, OAI.CubicFirstMoment.firstMomentScale