OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalRamare.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.mrtTypical_count_pos line 15

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalRamare.lean:15 (same declaration text).

2. lemma OAI.TwoPointCorrelations.mrtTypical_prime_mul line 21

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalRamare.lean:21 (same declaration text).

3. lemma OAI.TwoPointCorrelations.mrtTypical_ramare_supported line 48

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalRamare.lean:48 (same declaration text).

4. theorem OAI.TwoPointCorrelations.mrt_typical_ramare_sum line 59

   Source documentation

   Exact corrected typical-set decomposition at one prime band.

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalRamare.lean:59 (same declaration text).

   theorem mrt_typical_ramare_sum {ι : Type*} (J : Finset ι) (P : ι → Finset ℕ)
       (hP : ∀ j ∈ J, ∀ p ∈ P j, p.Prime)
       (hdis : Set.PairwiseDisjoint (J : Set ι) P) {j : ι} (hj : j ∈ J)
       (F : ℕ → ℂ) (N : ℕ) :
       (∑ n ∈ Icc 1 N, if mrtTypical J P n then F n else 0) =
         ∑ p ∈ P j, ∑ m ∈ Icc 1 (N / p),
           if mrtTypical (J.erase j) P m then
             F (p * m) /
               (((if p ∣ m then 0 else 1) + finitePrimeDivisorCount (P j) m : ℕ) : ℂ)
           else 0 := by
   …

   Mentions: OAI.TwoPointCorrelations.mrtTypical, OAI.TwoPointCorrelations.finitePrimeDivisorCount

5. theorem OAI.TwoPointCorrelations.mrt_typical_ramare_error line 82

   Source documentation

   The same prime-square exceptional bound holds after restriction to all the other typical-factorization bands.

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalRamare.lean:82 (same declaration text).

   theorem mrt_typical_ramare_error {ι : Type*} (J : Finset ι) (P : ι → Finset ℕ)
       (hP : ∀ j ∈ J, ∀ p ∈ P j, p.Prime)
       (hdis : Set.PairwiseDisjoint (J : Set ι) P) {j : ι} (hj : j ∈ J)
       (F : ℕ → ℂ) (N : ℕ) (hF : OneBounded F) :
       ‖(∑ n ∈ Icc 1 N, if mrtTypical J P n then F n else 0) -
         (∑ p ∈ P j, ∑ m ∈ Icc 1 (N / p),
           if mrtTypical (J.erase j) P m then
             F (p * m) / ((finitePrimeDivisorCount (P j) m + 1 : ℕ) : ℂ)
           else 0)‖ ≤ (N : ℝ) * ∑ p ∈ P j, (1 : ℝ) / (p : ℝ) ^ 2 := by
   …

   Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtTypical, OAI.TwoPointCorrelations.finitePrimeDivisorCount

6. lemma OAI.TwoPointCorrelations.mrt_LSeries_term_mul line 114

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalRamare.lean:114 (same declaration text).

7. theorem OAI.TwoPointCorrelations.mrt_typical_dirichlet_factorization line 124

   Source documentation

   The actual Dirichlet polynomial splits into a prime factor and a cofactor polynomial with the corrected reciprocal prime-count weight.

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalRamare.lean:124 (same declaration text).

   theorem mrt_typical_dirichlet_factorization {ι : Type*} (J : Finset ι)
       (P : ι → Finset ℕ) (hP : ∀ j ∈ J, ∀ p ∈ P j, p.Prime)
       (hdis : Set.PairwiseDisjoint (J : Set ι) P) {j : ι} (hj : j ∈ J)
       (F : ℕ → ℂ) (hF : ∀ m n, 0 < m → 0 < n → F (m * n) = F m * F n)
       (s : ℂ) (N : ℕ) :
       (∑ n ∈ Icc 1 N, if mrtTypical J P n then LSeries.term F s n else 0) =
         ∑ p ∈ P j, ∑ m ∈ Icc 1 (N / p),
           if mrtTypical (J.erase j) P m then
             (LSeries.term F s p * LSeries.term F s m) /
               (((if p ∣ m then 0 else 1) + finitePrimeDivisorCount (P j) m : ℕ) : ℂ)
           else 0 := by
   …

   Mentions: OAI.TwoPointCorrelations.mrtTypical, OAI.TwoPointCorrelations.finitePrimeDivisorCount