MangoldtMinorArcActual.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.MangoldtMinorArcActual.minorArcs line 16
Source documentation
The logarithmic minor arcs, with the denominator cutoff needed to save D powers of the logarithm in the actual Mangoldt exponential sum.
```
def minorArcs (D N : ℕ) : Set ℝ :=
…
```
Mentions: OAI.Problem337.D
lemma OAI.Problem337.MangoldtMinorArcActual.measurableSet_minorArcs line 21
lemma OAI.Problem337.MangoldtMinorArcActual.minorArcs_subset line 24
lemma OAI.Problem337.MangoldtMinorArcActual.phase_eq_vaughan line 28
Source documentation
The two independently developed Fourier conventions agree exactly.
```
lemma phase_eq_vaughan (n : ℕ) (x : ℝ) :
    phase (n : ℤ) x = VaughanBilinear.phase (x * n) := by
…
```
Mentions: OAI.Problem337.VaughanBilinear.phase
lemma OAI.Problem337.MangoldtMinorArcActual.mangoldtPhaseSum_eq_weightedSum line 36
theorem OAI.Problem337.MangoldtMinorArcActual.eventually_mangoldtPhaseSum_norm_le line 47
Source documentation
Actual minor-arc cancellation. The pointwise exponential-sum estimate is proved, not assumed: it combines Vaughan's estimate with Dirichlet geometry.
```
theorem eventually_mangoldtPhaseSum_norm_le (D : ℕ) :
    ∀ᶠ N : ℕ in atTop, ∀ x ∈ minorArcs D N,
      ‖mangoldtPhaseSum N x‖ ≤ (N : ℝ) / Real.log (N : ℝ) ^ D := by
…
```
Mentions: OAI.Problem337.D, OAI.Problem337.MangoldtMinorArcActual.minorArcs
lemma OAI.Problem337.MangoldtMinorArcActual.mangoldt_square_sum_le line 57
Source documentation
A crude but unconditional coefficient energy bound is sufficient once three logarithmic powers have been saved pointwise.
```
lemma mangoldt_square_sum_le (N : ℕ) :
    (∑ n ∈ Finset.Icc 1 N, ‖(ArithmeticFunction.vonMangoldt n : ℂ)‖ ^ 2) ≤
      (N : ℝ) * Real.log (N : ℝ) ^ 2 := by
…
```
lemma OAI.Problem337.MangoldtMinorArcActual.mangoldtPhaseSum_eq_natPolynomial line 73
theorem OAI.Problem337.MangoldtMinorArcActual.eventually_mangoldt_minor_integral_le line 80
Source documentation
On the explicit logarithmic minor arcs the actual cubic extraction integral is at most N²/log N, without a prime-distribution hypothesis.
```
theorem eventually_mangoldt_minor_integral_le :
    ∀ᶠ N : ℕ in atTop,
      ‖∫ x in minorArcs 3 N, mangoldtPhaseSum N x ^ 3 * phase (-(N : ℤ)) x‖ ≤
        (N : ℝ) ^ 2 / Real.log (N : ℝ) := by
…
```
Mentions: OAI.Problem337.MangoldtMinorArcActual.minorArcs
theorem OAI.Problem337.MangoldtMinorArcActual.eventually_mangoldt_minor_integral_small line 100
Source documentation
The minor arcs contribute an arbitrarily small quadratic error. Their cutoff is fixed at log(N)^18, independently of the requested error.
```
theorem eventually_mangoldt_minor_integral_small (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop,
      ‖∫ x in minorArcs 3 N, mangoldtPhaseSum N x ^ 3 * phase (-(N : ℤ)) x‖ ≤
        ε * (N : ℝ) ^ 2 := by
…
```
Mentions: OAI.Problem337.MangoldtMinorArcActual.minorArcs
theorem OAI.Problem337.MangoldtMinorArcActual.mangoldt_minor_integral_isLittleO line 115
Source documentation
Standard little-oh form of the unconditional minor-arc estimate.
```
theorem mangoldt_minor_integral_isLittleO :
    (fun N : ℕ => ∫ x in minorArcs 3 N,
      mangoldtPhaseSum N x ^ 3 * phase (-(N : ℤ)) x) =o[atTop]
        (fun N : ℕ => (N : ℝ) ^ 2) := by
…
```
Mentions: OAI.Problem337.MangoldtMinorArcActual.minorArcs