RamanujanProduct.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.RamanujanProduct.unitSum line 11
Source documentation
A character sum over the units of a finite ring, written as a sum over the whole ring so that product-ring factorization is transparent.
```
def unitSum {R : Type*} [CommRing R] [Fintype R]
    (ψ : AddChar R ℂ) (t : R) : ℂ := by
…
```
def OAI.Problem337.RamanujanProduct.leftChar line 16
def OAI.Problem337.RamanujanProduct.rightChar line 20
theorem OAI.Problem337.RamanujanProduct.character_prod line 24
theorem OAI.Problem337.RamanujanProduct.unitSum_prod line 33
Source documentation
A character sum over units factors through the two coordinate characters. No primitivity or coprimality assumption is needed here.
```
theorem unitSum_prod {R S : Type*} [CommRing R] [CommRing S]
    [Fintype R] [Fintype S] (ψ : AddChar (R × S) ℂ) (t : R × S) :
    unitSum ψ t = unitSum (leftChar ψ) t.1 * unitSum (rightChar ψ) t.2 := by
…
```
Mentions: OAI.Problem337.RamanujanProduct.unitSum, OAI.Problem337.RamanujanProduct.leftChar, OAI.Problem337.RamanujanProduct.rightChar
theorem OAI.Problem337.RamanujanProduct.leftChar_primitive line 51
Source documentation
A primitive product-ring character remains primitive on each coordinate ring.
```
theorem leftChar_primitive {R S : Type*} [CommRing R] [CommRing S]
    (ψ : AddChar (R × S) ℂ) (hψ : ψ.IsPrimitive) :
    (leftChar ψ).IsPrimitive := by
…
```
Mentions: OAI.Problem337.RamanujanProduct.leftChar
theorem OAI.Problem337.RamanujanProduct.rightChar_primitive line 61

theorem OAI.Problem337.RamanujanProduct.primitive_comp_ringEquiv line 73

Source documentation

Transporting a primitive character along a ring equivalence preserves primitivity.

theorem primitive_comp_ringEquiv {R S : Type*} [CommRing R] [CommRing S]
    (ψ : AddChar S ℂ) (hψ : ψ.IsPrimitive) (e : R ≃+* S) :
    (ψ.compAddMonoidHom e.toAddMonoidHom).IsPrimitive := by
…

theorem OAI.Problem337.RamanujanProduct.unitSum_ringEquiv line 86
Source documentation
The unit character sum is invariant under simultaneous transport of the character and its argument by a ring equivalence.
```
theorem unitSum_ringEquiv {R S : Type*} [CommRing R] [CommRing S]
    [Fintype R] [Fintype S] (ψ : AddChar S ℂ) (e : R ≃+* S) (t : R) :
    unitSum (ψ.compAddMonoidHom e.toAddMonoidHom) t = unitSum ψ (e t) := by
…
```
Mentions: OAI.Problem337.RamanujanProduct.unitSum
theorem OAI.Problem337.RamanujanProduct.prime_unitSum line 97
Source documentation
Every primitive character has the same unit sum at prime modulus.
```
theorem prime_unitSum {p : ℕ} [Fact p.Prime] (ψ : AddChar (ZMod p) ℂ)
    (hψ : ψ.IsPrimitive) (t : ZMod p) :
    unitSum ψ t = if t = 0 then (p : ℂ) - 1 else -1 := by
…
```
Mentions: OAI.Problem337.RamanujanProduct.unitSum
theorem OAI.Problem337.RamanujanProduct.unitSum_chineseRemainder line 120
Source documentation
CRT factorization of an actual unit character sum. The coordinate characters are transported characters, so no choice of inverse CRT coefficients is hidden in the statement.
```
theorem unitSum_chineseRemainder {m n : ℕ} [NeZero m] [NeZero n]
    (h : m.Coprime n) (ψ : AddChar (ZMod (m * n)) ℂ) (u : ℕ) :
    let χ := ψ.compAddMonoidHom (ZMod.chineseRemainder h).symm.toAddMonoidHom
…
```
theorem OAI.Problem337.RamanujanProduct.unitSum_of_primeProduct line 139
Source documentation
At a squarefree modulus supplied as a product of distinct primes, every primitive character gives the expected product of Ramanujan factors. This finite identity is independent of analytic prime estimates.
```
theorem unitSum_of_primeProduct (s : Finset ℕ) :
    ∀ (_hs : ∀ p ∈ s, p.Prime) (n : ℕ) [NeZero n],
      n = ∏ p ∈ s, p →
      ∀ (ψ : AddChar (ZMod n) ℂ), ψ.IsPrimitive → ∀ u : ℕ,
        unitSum ψ (-(u : ZMod n)) =
          ∏ p ∈ s, (if p ∣ u then (p : ℂ) - 1 else -1) := by
…
```
Mentions: OAI.Problem337.RamanujanProduct.unitSum

theorem OAI.Problem337.RamanujanProduct.unitSum_squarefree line 193

Source documentation

The prime-product formula in the customary squarefree-modulus form.

theorem unitSum_squarefree {n : ℕ} [NeZero n] (hn : Squarefree n)
    (ψ : AddChar (ZMod n) ℂ) (hψ : ψ.IsPrimitive) (u : ℕ) :
    unitSum ψ (-(u : ZMod n)) =
      ∏ p ∈ n.primeFactors, (if p ∣ u then (p : ℂ) - 1 else -1) := by
…

Mentions: OAI.Problem337.RamanujanProduct.unitSum

def OAI.Problem337.RamanujanProduct.ramanujanSum line 203
Source documentation
The standard Ramanujan sum at any nonzero modulus, with its usual unit-residue restriction.
```
def ramanujanSum (n : ℕ) [NeZero n] (u : ℕ) : ℂ :=
…
```
theorem OAI.Problem337.RamanujanProduct.ramanujanSum_squarefree line 206
theorem OAI.Problem337.RamanujanProduct.unitSum_eq_ramanujanSum line 213
Source documentation
A primitive character can replace the standard character in a squarefree Ramanujan sum without changing its value.
```
theorem unitSum_eq_ramanujanSum {n : ℕ} [NeZero n] (hn : Squarefree n)
    (ψ : AddChar (ZMod n) ℂ) (hψ : ψ.IsPrimitive) (u : ℕ) :
    unitSum ψ (-(u : ZMod n)) = ramanujanSum n u := by
…
```
Mentions: OAI.Problem337.RamanujanProduct.unitSum, OAI.Problem337.RamanujanProduct.ramanujanSum
theorem OAI.Problem337.RamanujanProduct.ramanujanSum_mul line 220
Source documentation
Multiplicativity for the standard character at coprime squarefree moduli, without any explicit choice of inverse CRT coefficients.
```
theorem ramanujanSum_mul {m n : ℕ} [NeZero m] [NeZero n]
    (hm : Squarefree m) (hn : Squarefree n) (h : m.Coprime n) (u : ℕ) :
    ramanujanSum (m * n) u = ramanujanSum m u * ramanujanSum n u := by
…
```
Mentions: OAI.Problem337.RamanujanProduct.ramanujanSum