ThreePrimeLocalFactor.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.ThreePrimeLocalFactor.nonzero_character_sum line 11

Source documentation

Orthogonality with the zero residue removed.

theorem nonzero_character_sum {p : ℕ} [NeZero p] (t : ZMod p) :
    (∑ a ∈ (Finset.univ : Finset (ZMod p)).erase 0,
      ZMod.stdAddChar (t * a)) =
      if t = 0 then (p : ℂ) - 1 else -1 := by
…

def OAI.Problem337.ThreePrimeLocalFactor.primeRamanujanSum line 25
Source documentation
The prime-modulus Ramanujan sum, indexed by nonzero residues.
```
def primeRamanujanSum (p : ℕ) [NeZero p] (u : ℕ) : ℂ :=
…
```
theorem OAI.Problem337.ThreePrimeLocalFactor.primeRamanujanSum_eq line 31
Source documentation
Removing the zero frequency from character orthogonality gives the prime Ramanujan sum. In fact this formula needs only a nonzero modulus.
```
theorem primeRamanujanSum_eq (p : ℕ) [NeZero p] (u : ℕ) :
    primeRamanujanSum p u = if p ∣ u then (p : ℂ) - 1 else -1 := by
…
```
Mentions: OAI.Problem337.ThreePrimeLocalFactor.primeRamanujanSum
def OAI.Problem337.ThreePrimeLocalFactor.localFactor line 38
Source documentation
The normalized cubic prime-frequency contribution to the ternary singular series.
```
def localFactor (p u : ℕ) [NeZero p] : ℂ :=
…
```
theorem OAI.Problem337.ThreePrimeLocalFactor.localFactor_eq line 43
Source documentation
The two familiar local factors follow exactly from finite character orthogonality; this is not an asymptotic prime-counting assertion.
```
theorem localFactor_eq (p u : ℕ) (hp : p.Prime) :
    letI : NeZero p := ⟨hp.ne_zero⟩
…
```
def OAI.Problem337.ThreePrimeLocalFactor.cubicPrimeCoefficient line 58
Source documentation
The normalized cubic exponential-sum contribution of the nonzero frequencies at a prime modulus.
```
def cubicPrimeCoefficient (p u : ℕ) [NeZero p] : ℂ :=
…
```
theorem OAI.Problem337.ThreePrimeLocalFactor.cubicPrimeCoefficient_eq line 67
Source documentation
The cubic coefficient is exactly the signed, normalized Ramanujan sum. Thus the local Euler factor is the zero-frequency contribution plus the actual nonzero-frequency cubic sum.
```
theorem cubicPrimeCoefficient_eq (p u : ℕ) [NeZero p] :
    cubicPrimeCoefficient p u =
      -primeRamanujanSum p u / ((p : ℂ) - 1) ^ 3 := by
…
```
Mentions: OAI.Problem337.ThreePrimeLocalFactor.cubicPrimeCoefficient, OAI.Problem337.ThreePrimeLocalFactor.primeRamanujanSum
theorem OAI.Problem337.ThreePrimeLocalFactor.one_add_cubicPrimeCoefficient line 85
theorem OAI.Problem337.ThreePrimeLocalFactor.one_add_cubicPrimeCoefficient_eq_real line 92
Source documentation
A real-valued statement of the local factor for direct use with real Euler products.
```
theorem one_add_cubicPrimeCoefficient_eq_real (p u : ℕ) (hp : p.Prime) :
    letI : NeZero p := ⟨hp.ne_zero⟩
…
```