OAI/NumberTheory/CubicMoment/Estimates/ShortFactorSize.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The auxiliary size cutoffs in the uniform short-factor estimate are automatic.

  1. lemma OAI.CubicFirstMoment.shortFactorPolynomial_uniform_quadratic_size line 11
  2. lemma OAI.CubicFirstMoment.primary_gram_rows_card_quadratic line 33
  3. lemma OAI.CubicFirstMoment.balanced_rows_card_quadratic line 43