MRTEulerProducts.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The finite Euler-product estimate needed in Halász's method. The pretentious-distance saving is obtained from the actual prime coefficients; no mean-value theorem is assumed here.

lemma OAI.TwoPointCorrelations.mrt_local_euler_bound line 15
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTEulerProducts.lean:15 (same declaration text).
def OAI.TwoPointCorrelations.mrtArchimedeanTwist line 43
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTEulerProducts.lean:43 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtArchimedeanTwist_norm line 46
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTEulerProducts.lean:46 (same declaration text).
def OAI.TwoPointCorrelations.mrtPrimeEulerTerm line 50
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTEulerProducts.lean:50 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeEulerTerm_norm_le line 53
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTEulerProducts.lean:53 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeEulerTerm_re line 60
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTEulerProducts.lean:60 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_finite_euler_distance_bound line 67
Source documentation
The finite Euler product retains the full pretentious-distance gain. The remaining prime-square error is absolutely summable.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTEulerProducts.lean:67 (same declaration text).
```
theorem mrt_finite_euler_distance_bound (b : ℕ → ℂ)
    (hb : ∀ n : ℕ, 0 < n → ‖b n‖ ≤ 1) (t : ℝ) (N : ℕ) :
    ‖∏ p ∈ primesUpTo N, (1 - mrtPrimeEulerTerm b t p)⁻¹‖ ≤
      Real.exp ((∑ p ∈ primesUpTo N, (1 : ℝ) / p) -
        squaredDistance b (mrtArchimedeanTwist t) N +
        ∑ p ∈ primesUpTo N, (1 : ℝ) / (p : ℝ) ^ 2) := by
…
```
Mentions: OAI.TwoPointCorrelations.primesUpTo, OAI.TwoPointCorrelations.mrtPrimeEulerTerm, OAI.TwoPointCorrelations.mrtArchimedeanTwist

theorem OAI.TwoPointCorrelations.mrt_masked_distance_lower line 106

Source documentation

Multiplication by a real mask in [0,1] can reduce the squared pretentious distance by at most a factor of two (MRT Lemma A.4(i)).

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTEulerProducts.lean:106 (same declaration text).

theorem mrt_masked_distance_lower (b twist : ℕ → ℂ) (mask : ℕ → ℝ) (N : ℕ)
    (hb : ∀ p ∈ primesUpTo N, ‖b p‖ ≤ 1)
    (htwist : ∀ p ∈ primesUpTo N, ‖twist p‖ ≤ 1)
    (hmask : ∀ p ∈ primesUpTo N, 0 ≤ mask p ∧ mask p ≤ 1) :
    squaredDistance b twist N ≤
      2 * squaredDistance (fun p => b p * (mask p : ℂ)) twist N := by
…

Mentions: OAI.TwoPointCorrelations.primesUpTo