ThreePrimeEulerProduct.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.ternaryEulerFactor line 10
Source documentation
The standard ternary local Euler factor, extended by one at nonprimes.
```
def ternaryEulerFactor (u p : ℕ) : ℝ :=
…
```
lemma OAI.Problem337.ternaryEulerFactor_add_three line 16
lemma OAI.Problem337.ternaryEulerFactor_two line 23
lemma OAI.Problem337.ternaryEulerFactor_prefix line 35
lemma OAI.Problem337.ternaryEulerFactor_tail_multipliable line 42
lemma OAI.Problem337.ternaryEulerFactor_multipliable line 47
theorem OAI.Problem337.threePrimeSingularSeries_eq_euler_tprod line 53
Source documentation
The shifted odd-prime definition is exactly the conventional Euler product, including the vanishing local factor at two for even inputs.
```
theorem threePrimeSingularSeries_eq_euler_tprod (u : ℕ) :
    threePrimeSingularSeries u = ∏' p : ℕ, ternaryEulerFactor u p := by
…
```
Mentions: OAI.Problem337.threePrimeSingularSeries, OAI.Problem337.ternaryEulerFactor
theorem OAI.Problem337.threePrimeSingularSeries_eq_prime_tprod line 68
Source documentation
Removing the factors equal to one at nonprimes recovers the usual prime-indexed singular series. This identity is valid for all natural inputs.
```
theorem threePrimeSingularSeries_eq_prime_tprod (u : ℕ) :
    threePrimeSingularSeries u = ∏' p : {p : ℕ // p.Prime},
      (if p.val ∣ u then 1 - 1 / ((p.val : ℝ) - 1) ^ 2
       else 1 + 1 / ((p.val : ℝ) - 1) ^ 3) := by
…
```
Mentions: OAI.Problem337.threePrimeSingularSeries
lemma OAI.Problem337.threePrimeSingularSeries_eq_zero_of_even line 84