OAI/NumberTheory/Ostmann/QuadraticCenter/HalfKernelRankin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Rankin's bound for the reciprocal mass of high-weight half kernels

  1. theorem OAI.Ostmann.high_weight_squarefree_reciprocal line 12
  2. theorem OAI.Ostmann.high_weight_half_kernel_card line 37

    Source documentation

    The exponential high-weight condition forces many factors in the small half kernel.

    theorem high_weight_half_kernel_card (s r : ℕ)
    (hcard : r.primeFactors.card = s.primeFactors.card / 2)
    (u K τ : ℝ) (hu : 1 < u) (hhigh : Real.exp (τ * K) < u ^ s.primeFactors.card) :
    τ * K / (2 * Real.log u) - 1 ≤ r.primeFactors.card := by
…