MangoldtMajorArcReduction.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.MangoldtMajorArcReduction.majorArcs line 13
Source documentation
The major arcs complementary to the proved logarithmic minor arcs.
```
def majorArcs (N : ℕ) : Set ℝ :=
…
```
def OAI.Problem337.MangoldtMajorArcReduction.majorIntegral line 18
Source documentation
The actual major-arc contribution, not a model exponential sum.
```
def majorIntegral (N : ℕ) : ℂ :=
…
```
lemma OAI.Problem337.MangoldtMajorArcReduction.measurableSet_majorArcs line 21
theorem OAI.Problem337.MangoldtMajorArcReduction.mangoldt_coefficient_eq_major_add_minor line 25
Source documentation
Exact major/minor decomposition of the actual arithmetic coefficient.
```
theorem mangoldt_coefficient_eq_major_add_minor (N : ℕ) :
    (mangoldtTripleSum N : ℂ) = majorIntegral N +
      ∫ x in minorArcs 3 N, mangoldtPhaseSum N x ^ 3 * phase (-(N : ℤ)) x := by
…
```
Mentions: OAI.Problem337.mangoldtTripleSum, OAI.Problem337.MangoldtMajorArcReduction.majorIntegral
theorem OAI.Problem337.MangoldtMajorArcReduction.mangoldt_coefficient_sub_major line 40
theorem OAI.Problem337.MangoldtMajorArcReduction.mangoldt_coefficient_sub_major_isLittleO line 48
Source documentation
The actual major integral approximates the arithmetic coefficient with an unconditional little-oh quadratic error.
```
theorem mangoldt_coefficient_sub_major_isLittleO :
    (fun N : ℕ => (mangoldtTripleSum N : ℂ) - majorIntegral N) =o[atTop]
      (fun N : ℕ => (N : ℝ) ^ 2) := by
…
```
Mentions: OAI.Problem337.mangoldtTripleSum, OAI.Problem337.MangoldtMajorArcReduction.majorIntegral
theorem OAI.Problem337.MangoldtMajorArcReduction.quantitativeThreePrimeLowerBound_of_major_lower line 55
Source documentation
A positive quadratic lower bound on the actual major contribution alone now suffices. There is no remaining minor-arc analytic hypothesis.
```
theorem quantitativeThreePrimeLowerBound_of_major_lower
    (hmajor : ∃ c : ℝ, 0 < c ∧ ∀ᶠ N : ℕ in atTop, Odd N →
      c * (N : ℝ) ^ 2 ≤ (majorIntegral N).re) :
    QuantitativeThreePrimeLowerBound := by
…
```
Mentions: OAI.Problem337.MangoldtMajorArcReduction.majorIntegral, OAI.Problem337.QuantitativeThreePrimeLowerBound
theorem OAI.Problem337.MangoldtMajorArcReduction.ternaryMangoldtAsymptotic_of_major_asymptotic line 75
Source documentation
The full ternary asymptotic follows from its major-arc part alone, since the actual minor integral has already been estimated unconditionally.
```
theorem ternaryMangoldtAsymptotic_of_major_asymptotic
    (hmajor : ∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop, Odd N →
      ‖majorIntegral N -
        (((1 / 2 : ℝ) * threePrimeSingularSeries N * (N : ℝ) ^ 2 : ℝ) : ℂ)‖ ≤
        ε * (N : ℝ) ^ 2) : TernaryMangoldtAsymptotic := by
…
```
Mentions: OAI.Problem337.MangoldtMajorArcReduction.majorIntegral, OAI.Problem337.threePrimeSingularSeries, OAI.Problem337.TernaryMangoldtAsymptotic