OAI/NumberTheory/Ostmann/Quadratic/QuadraticKernelDecomposition.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual signed squarefree kernels of nonzero affine values

  1. theorem OAI.Ostmann.exists_signed_squarefree_decomposition line 11
  2. theorem OAI.Ostmann.signed_kernel_mem_range line 25
  3. theorem OAI.Ostmann.affine_kernel_mem_range line 39

    Source documentation

    The bound used by the large sieve follows directly from the original endpoint interval and the common center.

    theorem affine_kernel_mem_range {X m : ℕ} {h u x : ℤ} {t : ℕ}
    (hu : u ≠ 0) (ht : 0 < t) (hsf : Squarefree u.natAbs)
    (heq : u * (t : ℤ) ^ 2 = (m : ℤ) * x - h) (hx : |x| ≤ X) :
    u ∈ signedSquarefreeRange (m * X + h.natAbs) := by
…

    Mentions: OAI.Ostmann.signedSquarefreeRange