SignedKernelCharacter.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A primitive character for each non-small signed squarefree kernel

theorem OAI.Ostmann.prime_character_zero line 10
theorem OAI.Ostmann.prime_jacobi_zero line 17

theorem OAI.Ostmann.kernel_prime_character_value line 28

Source documentation

Equality at coprime odd arguments extends to all odd primes because both characters vanish at a prime factor of the odd kernel.

theorem kernel_prime_character_value (d : ℤ) (N : ℕ) (χ : PrimitiveRealCharacter)
    (hNq : N ∣ χ.modulus) (hNd : N ∣ d.natAbs)
    (hvalue : ∀ a : ℕ, Odd a → a.Coprime N → χ.character a = (jacobiSym d a : ℝ)) :
    ∀ p : ℕ, p.Prime → p ≠ 2 → χ.character p = (jacobiSym d p : ℝ) := by
…

Mentions: OAI.Ostmann.PrimitiveRealCharacter

theorem OAI.Ostmann.exists_signed_kernel_character line 41

Source documentation

The auxiliary N is the odd part of the kernel. Its divisibility and conductor bounds also give a finite list of possible kernels for a fixed exceptional conductor. No character-classification result is assumed.

theorem exists_signed_kernel_character (d : ℤ) (hsf : Squarefree d.natAbs)
    (hd : 2 < d.natAbs) :
    ∃ (χ : PrimitiveRealCharacter) (N : ℕ),
      1 < N ∧ N ∣ χ.modulus ∧ χ.modulus ≤ 8 * N ∧
      (d.natAbs = N ∨ d.natAbs = 2 * N) ∧
      χ.modulus ≤ 4 * d.natAbs ∧ d.natAbs ≤ 2 * χ.modulus ∧
      ∀ p : ℕ, p.Prime → p ≠ 2 → χ.character p = (jacobiSym d p : ℝ) := by
…

Mentions: OAI.Ostmann.PrimitiveRealCharacter