MRTRamareIdentity.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The corrected Ramaré identity from MRT v3, equation (3.2). The denominator retains 1_{p ∤ m}; repeated prime factors are allowed.

lemma OAI.TwoPointCorrelations.finitePrimeDivisorCount_eq_card line 14
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareIdentity.lean:14 (same declaration text).
lemma OAI.TwoPointCorrelations.finitePrimeDivisorCount_insert line 18
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareIdentity.lean:18 (same declaration text).
lemma OAI.TwoPointCorrelations.finitePrimeDivisorCount_pos_of_mem line 23
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareIdentity.lean:23 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_prime_divisor_count_mul line 29
Source documentation
The correction term distinguishes a new prime from a repeated prime.
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareIdentity.lean:29 (same declaration text).
```
theorem mrt_prime_divisor_count_mul (P : Finset ℕ)
    (hP : ∀ p ∈ P, p.Prime) {p : ℕ} (hp : p ∈ P) (m : ℕ) :
    finitePrimeDivisorCount P (p * m) =
      (if p ∣ m then 0 else 1) + finitePrimeDivisorCount P m := by
…
```
Mentions: OAI.TwoPointCorrelations.finitePrimeDivisorCount
lemma OAI.TwoPointCorrelations.mrt_ramare_common_denominator line 52
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareIdentity.lean:52 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_ramare_identity line 64

Source documentation

Corrected pointwise factorization, with no squarefree assumption.

Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareIdentity.lean:64 (same declaration text).

theorem mrt_ramare_identity (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (F : ℕ → ℂ) (n : ℕ) :
    (if finitePrimeDivisorCount P n = 0 then 0 else F n) =
      ∑ p ∈ P, if p ∣ n then
        F (p * (n / p)) /
          (((if p ∣ n / p then 0 else 1) + finitePrimeDivisorCount P (n / p) : ℕ) : ℂ)
        else 0 := by
…

Mentions: OAI.TwoPointCorrelations.finitePrimeDivisorCount

theorem OAI.TwoPointCorrelations.mrt_ramare_sum line 83

Source documentation

Exact finite prime/cofactor decomposition of a supported sum.

Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareIdentity.lean:83 (same declaration text).

theorem mrt_ramare_sum (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (F : ℕ → ℂ) (N : ℕ) :
    (∑ n ∈ Icc 1 N, if finitePrimeDivisorCount P n = 0 then 0 else F n) =
      ∑ p ∈ P, ∑ m ∈ Icc 1 (N / p),
        F (p * m) /
          (((if p ∣ m then 0 else 1) + finitePrimeDivisorCount P m : ℕ) : ℂ) := by
…

Mentions: OAI.TwoPointCorrelations.finitePrimeDivisorCount

lemma OAI.TwoPointCorrelations.mrt_inverse_successor_difference line 101
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareIdentity.lean:101 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_ramare_denominator_error line 118
Source documentation
Replacing the corrected denominator by ω_P(m)+1 costs only the prime-square terms. This is the correction explicitly needed in MRT v3.
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareIdentity.lean:118 (same declaration text).
```
theorem mrt_ramare_denominator_error (P : Finset ℕ) {p m : ℕ}
    (hp : p ∈ P) (z : ℂ) :
    ‖z / (((if p ∣ m then 0 else 1) + finitePrimeDivisorCount P m : ℕ) : ℂ) -
      z / ((finitePrimeDivisorCount P m + 1 : ℕ) : ℂ)‖ ≤
        if p ∣ m then ‖z‖ else 0 := by
…
```
Mentions: OAI.TwoPointCorrelations.finitePrimeDivisorCount
theorem OAI.TwoPointCorrelations.mrt_ramare_sum_error line 131
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareIdentity.lean:131 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_count_multiples line 147
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareIdentity.lean:147 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_ramare_error_of_bounded line 158

Source documentation

The prime-square exceptional contribution has the expected reciprocal square bound. No sieve estimate is needed for this error.

Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareIdentity.lean:158 (same declaration text).

theorem mrt_ramare_error_of_bounded (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (F : ℕ → ℂ) (N : ℕ) (hF : ∀ n, 0 < n → ‖F n‖ ≤ 1) :
    ‖(∑ n ∈ Icc 1 N, if finitePrimeDivisorCount P n = 0 then 0 else F n) -
      (∑ p ∈ P, ∑ m ∈ Icc 1 (N / p),
        F (p * m) / ((finitePrimeDivisorCount P m + 1 : ℕ) : ℂ))‖ ≤
      (N : ℝ) * ∑ p ∈ P, (1 : ℝ) / (p : ℝ) ^ 2 := by
…

Mentions: OAI.TwoPointCorrelations.finitePrimeDivisorCount