MRTPrimeSquareMean.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The prime-square error in the corrected Ramaré decomposition has a small mean square. The count is evaluated by pairing prime-square divisibility tests; distinct primes give the product modulus exactly.

def OAI.TwoPointCorrelations.mrtPrimeSquareCount line 15
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeSquareMean.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeSquareCount_nonneg line 18
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeSquareMean.lean:18 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_prime_square_joint_count line 23
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeSquareMean.lean:23 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_prime_square_count_second_moment line 63
Source documentation
No logarithm or cardinality of the prime set occurs in the divisibility-count second moment.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeSquareMean.lean:63 (same declaration text).
```
theorem mrt_prime_square_count_second_moment (P : Finset ℕ)
    (hP : ∀ p ∈ P, p.Prime) (N : ℕ) :
    (∑ n ∈ Icc 1 N, (mrtPrimeSquareCount P n) ^ 2) ≤
      (N : ℝ) * ((∑ p ∈ P, 1 / (p : ℝ) ^ 2) +
        (∑ p ∈ P, 1 / (p : ℝ) ^ 2) ^ 2) := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtPrimeSquareCount
theorem OAI.TwoPointCorrelations.mrt_prime_square_coefficient_mass line 108
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeSquareMean.lean:108 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_prime_square_dyadic_mean line 141

Source documentation

The mean-square cost of any prime-square-supported Ramaré error.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeSquareMean.lean:141 (same declaration text).

theorem mrt_prime_square_dyadic_mean (P : Finset ℕ)
    (hP : ∀ p ∈ P, p.Prime) (b : ℕ → ℂ) {N : ℕ} (hN : 0 < N)
    (hb : ∀ n ∈ Ioc N (2 * N), ‖b n‖ ≤ mrtPrimeSquareCount P n)
    {T : ℝ} (hT : 0 < T) :
    (∫ t in -T..T, ‖mrtDyadicPolynomial b N t‖ ^ 2) ≤
      32 * Real.exp 1 * (T / (N : ℝ) + 1) *
        ((∑ p ∈ P, 1 / (p : ℝ) ^ 2) + (∑ p ∈ P, 1 / (p : ℝ) ^ 2) ^ 2) := by
…

Mentions: OAI.TwoPointCorrelations.mrtPrimeSquareCount, OAI.TwoPointCorrelations.mrtDyadicPolynomial