OAI/Geometry/HeilbronnTriangle/IntegerPlaneEstimates.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.IntegerPlaneEstimates.Vec line 16
  2. lemma OAI.Problem355.IntegerPlaneEstimates.castVec_zero line 18
  3. def OAI.Problem355.IntegerPlaneEstimates.toLattice line 22
  4. lemma OAI.Problem355.IntegerPlaneEstimates.toLattice_coe line 25
  5. lemma OAI.Problem355.IntegerPlaneEstimates.norm_toLattice line 28
  6. lemma OAI.Problem355.IntegerPlaneEstimates.toLattice_injective line 31
  7. def OAI.Problem355.IntegerPlaneEstimates.liftFinset line 35
  8. lemma OAI.Problem355.IntegerPlaneEstimates.card_liftFinset line 42
  9. lemma OAI.Problem355.IntegerPlaneEstimates.norm_liftFinset_le line 46
  10. lemma OAI.Problem355.IntegerPlaneEstimates.one_le_norm_of_int_ne_zero line 54
  11. lemma OAI.Problem355.IntegerPlaneEstimates.one_le_norm_of_lattice_ne_zero line 64
  12. def OAI.Problem355.IntegerPlaneEstimates.successiveBasis line 81
  13. lemma OAI.Problem355.IntegerPlaneEstimates.successiveBasis_spec line 86
  14. def OAI.Problem355.IntegerPlaneEstimates.first line 95
  15. def OAI.Problem355.IntegerPlaneEstimates.second line 96
  16. lemma OAI.Problem355.IntegerPlaneEstimates.one_le_first line 98
  17. lemma OAI.Problem355.IntegerPlaneEstimates.first_le_second line 102
  18. def OAI.Problem355.IntegerPlaneEstimates.fromLattice line 107
  19. lemma OAI.Problem355.IntegerPlaneEstimates.fromLattice_dot line 110
  20. lemma OAI.Problem355.IntegerPlaneEstimates.cast_fromLattice line 113
  21. lemma OAI.Problem355.IntegerPlaneEstimates.toLattice_ne_zero line 118
  22. lemma OAI.Problem355.IntegerPlaneEstimates.first_le_norm line 128
  23. theorem OAI.Problem355.IntegerPlaneEstimates.exists_shortest_integer line 137
  24. theorem OAI.Problem355.IntegerPlaneEstimates.product_bounds line 153
  25. theorem OAI.Problem355.IntegerPlaneEstimates.plane_counts line 161
  26. theorem OAI.Problem355.IntegerPlaneEstimates.count_of_covolume_radius line 178
  27. theorem OAI.Problem355.IntegerPlaneEstimates.exists_primitive_shortest_integer line 193
  28. theorem OAI.Problem355.IntegerPlaneEstimates.second_le_of_independent line 208
  29. theorem OAI.Problem355.IntegerPlaneEstimates.thin_count line 233