OAI/NumberTheory/Ostmann/QuadraticSieve/PrimitiveKernelCharacter.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.character_ne_one_of_conductor_dvd line 10
2. def OAI.Ostmann.primitiveRealOfCharacter line 17
3. theorem OAI.Ostmann.primitiveRealOfCharacter_value line 29
4. theorem OAI.Ostmann.exists_odd_kernel_primitive line 39

   Source documentation

   An odd squarefree numerator, including either sign, has a primitive representative whose conductor lies between N and 4N.

   theorem exists_odd_kernel_primitive (N : ℕ) (hN : 1 < N) (hsf : Squarefree N)
       (hodd : Odd N) (negative : Bool) :
       ∃ χ : PrimitiveRealCharacter, N ∣ χ.modulus ∧ χ.modulus ≤ 4 * N ∧
         ∀ a : ℕ, Odd a → a.Coprime N →
           χ.character a = (jacobiSym (if negative then -(N : ℤ) else N) a : ℝ) := by
   …

   Mentions: OAI.Ostmann.PrimitiveRealCharacter

5. theorem OAI.Ostmann.exists_even_kernel_primitive line 58

   Source documentation

   The same construction for twice an odd squarefree numerator.

   theorem exists_even_kernel_primitive (N : ℕ) (hN : 1 < N) (hsf : Squarefree N)
       (hodd : Odd N) (negative : Bool) :
       ∃ χ : PrimitiveRealCharacter, N ∣ χ.modulus ∧ χ.modulus ≤ 8 * N ∧
         ∀ a : ℕ, Odd a → a.Coprime N →
           χ.character a = (jacobiSym (if negative then -(2 * (N : ℤ)) else 2 * N) a : ℝ) := by
   …

   Mentions: OAI.Ostmann.PrimitiveRealCharacter