ThreePrimeLocalSeries.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.threePrimeArithmeticFactor line 14
Source documentation
The normalized actual local unit-triple count at prime moduli, with one at nonprime indices. The inactive branch makes this a total natural-indexed function without imposing a finiteness instance on ZMod 0.
```
def threePrimeArithmeticFactor (p u : ℕ) : ℝ :=
…
```
lemma OAI.Problem337.threePrimeArithmeticFactor_of_prime line 19
lemma OAI.Problem337.threePrimeArithmeticFactor_of_not_prime line 27
theorem OAI.Problem337.threePrimeOddFactor_eq_arithmeticFactor line 33
Source documentation
The analytically indexed odd-prime Euler factor is the normalized actual count of its local unit solutions.
```
theorem threePrimeOddFactor_eq_arithmeticFactor (u n : ℕ) :
    1 + threePrimeOddPerturbation u n = threePrimeArithmeticFactor (n + 3) u := by
…
```
Mentions: OAI.Problem337.threePrimeOddPerturbation, OAI.Problem337.threePrimeArithmeticFactor
theorem OAI.Problem337.threePrimeArithmeticFactor_two line 45
Source documentation
The local unit-triple factor at two records precisely the parity obstruction.
```
theorem threePrimeArithmeticFactor_two (u : ℕ) :
    threePrimeArithmeticFactor 2 u = if Odd u then 2 else 0 := by
…
```
Mentions: OAI.Problem337.threePrimeArithmeticFactor
theorem OAI.Problem337.threePrimeSingularSeries_eq_localProduct line 55
Source documentation
Exact interpretation of the singular series as the product of normalized finite local unit-triple solution counts.
```
theorem threePrimeSingularSeries_eq_localProduct (u : ℕ) :
    threePrimeSingularSeries u = threePrimeArithmeticFactor 2 u *
      ∏' n : ℕ, threePrimeArithmeticFactor (n + 3) u := by
…
```
Mentions: OAI.Problem337.threePrimeSingularSeries, OAI.Problem337.threePrimeArithmeticFactor
theorem OAI.Problem337.threePrimeArithmeticFactors_multipliable line 63
Source documentation
The actual local-factor product converges, rather than merely being a formal Euler-product notation.
```
theorem threePrimeArithmeticFactors_multipliable (u : ℕ) :
    Multipliable (fun n : ℕ => threePrimeArithmeticFactor (n + 3) u) := by
…
```
Mentions: OAI.Problem337.threePrimeArithmeticFactor