RamanujanSingularLimit.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.threePrimeArithmeticFactor_prod_primesLE line 14
Source documentation
Inserting the neutral nonprime factors gives the canonical shifted natural-index truncation of the prime Euler product.
```
theorem threePrimeArithmeticFactor_prod_primesLE (N u : ℕ) :
    (∏ p ∈ Nat.primesLE (N + 2), threePrimeArithmeticFactor p u) =
      threePrimeArithmeticFactor 2 u *
        ∏ n ∈ Finset.range N, threePrimeArithmeticFactor (n + 3) u := by
…
```
Mentions: OAI.Problem337.threePrimeArithmeticFactor
theorem OAI.Problem337.sum_ramanujanCoefficient_primorial line 36
Source documentation
The divisor partial sums over a primorial are actual finite cubic Ramanujan sums and exactly equal the corresponding local-density product.
```
theorem sum_ramanujanCoefficient_primorial (N u : ℕ) :
    (∑ d ∈ (primorial (N + 2)).divisors, RamanujanEuler.coefficient d u) =
      ((threePrimeArithmeticFactor 2 u *
        ∏ n ∈ Finset.range N, threePrimeArithmeticFactor (n + 3) u : ℝ) : ℂ) := by
…
```
Mentions: OAI.Problem337.RamanujanEuler.coefficient, OAI.Problem337.threePrimeArithmeticFactor
theorem OAI.Problem337.tendsto_sum_ramanujanCoefficient_primorial line 52
Source documentation
The finite coefficient sums over divisors of expanding primorials converge to the canonical singular series. No prime-count asymptotic is used.
```
theorem tendsto_sum_ramanujanCoefficient_primorial (u : ℕ) :
    Tendsto (fun N : ℕ =>
      ∑ d ∈ (primorial (N + 2)).divisors, RamanujanEuler.coefficient d u)
      atTop (𝓝 (threePrimeSingularSeries u : ℂ)) := by
…
```
Mentions: OAI.Problem337.RamanujanEuler.coefficient, OAI.Problem337.threePrimeSingularSeries
lemma OAI.Problem337.ramanujanCoefficient_eq_zero_of_not_squarefree line 63
Source documentation
Nonsquarefree moduli contribute zero to the cubic Möbius-weighted sum.
```
lemma ramanujanCoefficient_eq_zero_of_not_squarefree (n u : ℕ)
    (hn : ¬Squarefree n) : RamanujanEuler.coefficient n u = 0 := by
…
```
Mentions: OAI.Problem337.RamanujanEuler.coefficient
theorem OAI.Problem337.tendsto_sum_ramanujanCoefficient_primorial_tsum line 75
Source documentation
Because nonsquarefree coefficient terms vanish, the primorial-divisor partial sums exhaust all the nonzero terms of any convergent coefficient series. Absolute convergence itself is deliberately an explicit input.
```
theorem tendsto_sum_ramanujanCoefficient_primorial_tsum (u : ℕ)
    (hs : Summable (fun n : ℕ => RamanujanEuler.coefficient n u)) :
    Tendsto (fun N : ℕ =>
      ∑ d ∈ (primorial (N + 2)).divisors, RamanujanEuler.coefficient d u)
      atTop (𝓝 (∑' n : ℕ, RamanujanEuler.coefficient n u)) := by
…
```
Mentions: OAI.Problem337.RamanujanEuler.coefficient
theorem OAI.Problem337.tsum_ramanujanCoefficient_eq_singularSeries line 116
Source documentation
Conditional only on actual coefficient summability, the ordinary infinite cubic Ramanujan series is exactly the canonical Euler-product singular series. This does not provide a three-prime counting asymptotic.
```
theorem tsum_ramanujanCoefficient_eq_singularSeries (u : ℕ)
    (hs : Summable (fun n : ℕ => RamanujanEuler.coefficient n u)) :
    (∑' n : ℕ, RamanujanEuler.coefficient n u) = (threePrimeSingularSeries u : ℂ) := by
…
```
Mentions: OAI.Problem337.RamanujanEuler.coefficient, OAI.Problem337.threePrimeSingularSeries