OAI/NumberTheory/CubicMoment/Estimates/NoncubeExponents.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Strict exponent gaps away from the two exceptional conductor shapes. These are the normalized exponents of the two cubic-sieve bounds and of the ordinary character large sieve, respectively.

  1. def OAI.CubicFirstMoment.pSieveExponent line 13
  2. def OAI.CubicFirstMoment.qSieveExponent line 16
  3. def OAI.CubicFirstMoment.ordinarySieveExponent line 19
  4. def OAI.CubicFirstMoment.noncubeSieveExponent line 22
  5. lemma OAI.CubicFirstMoment.pSieveExponent_neg line 25
  6. lemma OAI.CubicFirstMoment.qSieveExponent_neg line 38
  7. lemma OAI.CubicFirstMoment.ordinarySieveExponent_diag_neg line 43
  8. theorem OAI.CubicFirstMoment.noncubeSieveExponent_neg line 50

    Source documentation

    The only nonnegative-gap possibilities in the large-conductor region are precisely the two shapes treated by the structured moment argument.

    theorem noncubeSieveExponent_neg {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q)
    (hsize : p+2*q ≤ 1) (hlarge : 0 < p+2*q)
    (hfirst : p ≠ 1 ∨ q ≠ 0) (hbalanced : p ≠ 1/3 ∨ q ≠ 1/3) :
    noncubeSieveExponent p q < 0 := by
…

    Mentions: OAI.CubicFirstMoment.noncubeSieveExponent

  9. lemma OAI.CubicFirstMoment.continuous_noncubeSieveExponent line 65