OAI/NumberTheory/CubicGram/LatticeCounts.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Eisenstein lattice counts and arbitrarily small divisor losses.

  1. lemma OAI.CubicFirstMoment.norm_mul_eq line 15
  2. lemma OAI.CubicFirstMoment.norm_one_eq line 17
  3. lemma OAI.CubicFirstMoment.norm_pos_of_ne_zero line 18
  4. lemma OAI.CubicFirstMoment.one_le_norm line 20
  5. lemma OAI.CubicFirstMoment.norm_finset_prod line 24
  6. def OAI.CubicFirstMoment.nonzeroNormBall line 31
  7. lemma OAI.CubicFirstMoment.mem_nonzeroNormBall line 33
  8. theorem OAI.CubicFirstMoment.nonzeroNormBall_card_le line 37
  9. theorem OAI.CubicFirstMoment.primeDivisorWeight_small_power line 112
  10. theorem OAI.CubicFirstMoment.divisorEnergy_small_power line 147