RamanujanEuler.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.RamanujanEuler.primeCoefficient line 12
Source documentation
The nonzero-frequency local coefficient in the ternary prime problem.
```
def primeCoefficient (p u : ℕ) : ℂ :=
…
```
def OAI.Problem337.RamanujanEuler.coefficient line 18
Source documentation
The usual cubic Ramanujan coefficient, extended by zero at modulus zero. At positive modulus this is the actual unit-character sum weighted by the cube of the Möbius-to-totient ratio.
```
def coefficient (n u : ℕ) : ℂ :=
…
```
theorem OAI.Problem337.RamanujanEuler.coefficient_of_ne_zero line 24
theorem OAI.Problem337.RamanujanEuler.moebius_cube_squarefree line 29
theorem OAI.Problem337.RamanujanEuler.totient_squarefree_complex line 43
theorem OAI.Problem337.RamanujanEuler.coefficient_squarefree line 56
Source documentation
Exact multiplicative factorization of the analytic coefficient at squarefree moduli.
```
theorem coefficient_squarefree {n : ℕ} (hn : Squarefree n) (u : ℕ) :
    coefficient n u = ∏ p ∈ n.primeFactors, primeCoefficient p u := by
…
```
Mentions: OAI.Problem337.RamanujanEuler.coefficient, OAI.Problem337.RamanujanEuler.primeCoefficient
theorem OAI.Problem337.RamanujanEuler.one_add_primeCoefficient line 67
Source documentation
The local coefficient plus its zero-frequency term is the familiar real Euler factor.
```
theorem one_add_primeCoefficient (p u : ℕ) (hp : p.Prime) :
    1 + primeCoefficient p u =
      ((if p ∣ u then 1 - 1 / ((p : ℝ) - 1) ^ 2
        else 1 + 1 / ((p : ℝ) - 1) ^ 3 : ℝ) : ℂ) := by
…
```
Mentions: OAI.Problem337.RamanujanEuler.primeCoefficient
theorem OAI.Problem337.RamanujanEuler.sum_coefficient_divisors line 80
Source documentation
Exact finite Euler factorization of the cubic Ramanujan series over the divisors of a squarefree modulus. Every summand on the left is an actual finite unit-character sum, not an asserted asymptotic main term.
```
theorem sum_coefficient_divisors {n : ℕ} (hn : Squarefree n) (u : ℕ) :
    (∑ d ∈ n.divisors, coefficient d u) =
      ∏ p ∈ n.primeFactors,
        ((if p ∣ u then 1 - 1 / ((p : ℝ) - 1) ^ 2
          else 1 + 1 / ((p : ℝ) - 1) ^ 3 : ℝ) : ℂ) := by
…
```
Mentions: OAI.Problem337.RamanujanEuler.coefficient

theorem OAI.Problem337.RamanujanEuler.sum_coefficient_divisors_re line 109

Source documentation

The finite cubic Ramanujan sum is real; its real part is precisely the real finite singular product.

theorem sum_coefficient_divisors_re {n : ℕ} (hn : Squarefree n) (u : ℕ) :
    (∑ d ∈ n.divisors, coefficient d u).re =
      ∏ p ∈ n.primeFactors,
        (if p ∣ u then 1 - 1 / ((p : ℝ) - 1) ^ 2
          else 1 + 1 / ((p : ℝ) - 1) ^ 3) := by
…

Mentions: OAI.Problem337.RamanujanEuler.coefficient