MRTTypicalRamare.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Ramaré factorization on the actual typical-factorization set. Removing one selected prime band leaves exactly the remaining-band condition; the prime-square correction and its bound are retained.

lemma OAI.TwoPointCorrelations.mrtTypical_count_pos line 15
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalRamare.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtTypical_prime_mul line 21
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalRamare.lean:21 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtTypical_ramare_supported line 48
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalRamare.lean:48 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_typical_ramare_sum line 59

Source documentation

Exact corrected typical-set decomposition at one prime band.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/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

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/TwoPoint/ShortIntervals/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

lemma OAI.TwoPointCorrelations.mrt_LSeries_term_mul line 114
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalRamare.lean:114 (same declaration text).

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/TwoPoint/ShortIntervals/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