OAI/NumberTheory/CubicMoment/Estimates/HuxleyResiduePoints.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The literal residue sums as a finite set of reduced fractions.

  1. abbrev OAI.CubicFirstMoment.HuxleyResidueIndex line 11
  2. abbrev OAI.CubicFirstMoment.huxleyResidueFintype line 14
  3. abbrev OAI.CubicFirstMoment.huxleyResidueIndexFintype line 18
  4. def OAI.CubicFirstMoment.huxleyIndexLift line 22
  5. lemma OAI.CubicFirstMoment.huxleyIndexLift_injective line 25
  6. def OAI.CubicFirstMoment.huxleyResiduePointSet line 37
  7. lemma OAI.CubicFirstMoment.huxleyResiduePointSet_reduced line 41
  8. lemma OAI.CubicFirstMoment.huxleyResiduePointSet_shift line 49
  9. lemma OAI.CubicFirstMoment.huxleyResiduePointSet_sum line 56
  10. lemma OAI.CubicFirstMoment.huxleySieveMass_eq_points line 73