AngularAlgebra.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Algebra of fixed angular prime moments

The angular weight is the phase of a nonzero Eisenstein integer raised to an integer power. These elementary facts ensure that fixed angular weights preserve absolute values and distribute through finite prime sums.

theorem OAI.CubicFirstMoment.cStar_pos line 20
Source documentation
The bias constant in the manuscript is strictly positive.
```
theorem cStar_pos : 0 < cStar := by
…
```
Mentions: OAI.CubicFirstMoment.cStar
theorem OAI.CubicFirstMoment.firstMomentScale_pos line 25
Source documentation
The scale of the first moment is positive beyond one.
```
theorem firstMomentScale_pos {X : ℝ} (hX : 1 < X) : 0 < firstMomentScale X := by
…
```
Mentions: OAI.CubicFirstMoment.firstMomentScale
theorem OAI.CubicFirstMoment.theta_zero line 29
theorem OAI.CubicFirstMoment.theta_one line 32
theorem OAI.CubicFirstMoment.theta_mul line 35
theorem OAI.CubicFirstMoment.norm_theta line 40
theorem OAI.CubicFirstMoment.norm_theta_mul line 45
theorem OAI.CubicFirstMoment.theta_add line 49
theorem OAI.CubicFirstMoment.primeCutoffSum_add line 54
theorem OAI.CubicFirstMoment.primeCutoffSum_sub line 59
theorem OAI.CubicFirstMoment.primeCutoffSum_const_mul line 64
def OAI.CubicFirstMoment.angularPrimeModel line 69
Source documentation
The elementary prime model in the fixed angular mode ℓ.
```
def angularPrimeModel (ℓ : ℤ) (p : Eisenstein) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.angularPrimeMoment line 73
Source documentation
The prime Gauss-sum moment in the fixed angular mode ℓ.
```
def angularPrimeMoment (ℓ : ℤ) (X : ℝ) : ℂ :=
…
```
def OAI.CubicFirstMoment.angularPrimeDifference line 77
Source documentation
The difference between the Gauss-sum moment and its elementary model.
```
def angularPrimeDifference (ℓ : ℤ) (X : ℝ) : ℂ :=
…
```
theorem OAI.CubicFirstMoment.angularPrimeDifference_eq_sub line 81
theorem OAI.CubicFirstMoment.angularCancellation_of_comparison line 89
Source documentation
Angular comparison and the model prime-number theorem imply angular cancellation by subtraction.
```
theorem angularCancellation_of_comparison
    (hcomparison : AngularComparisonStatement)
    (hmodel : ∀ ℓ : ℤ, ℓ ≠ 0 → Asymptotics.IsLittleO Filter.atTop
      (primeCutoffSum (angularPrimeModel ℓ)) firstMomentScale) :
    AngularCancellationStatement := by
…
```
Mentions: OAI.CubicFirstMoment.AngularComparisonStatement, OAI.CubicFirstMoment.primeCutoffSum, OAI.CubicFirstMoment.angularPrimeModel, OAI.CubicFirstMoment.firstMomentScale, OAI.CubicFirstMoment.AngularCancellationStatement