OAI/Geometry/HeilbronnTriangle/IntegerSamplingPairs.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem355.IntegerSamplingPairs.collisionMass line 16
  2. theorem OAI.Problem355.IntegerSamplingPairs.collisionMass_le line 21
  3. theorem OAI.Problem355.IntegerSamplingPairs.conditionalColumnMass_le line 71
  4. theorem OAI.Problem355.IntegerSamplingPairs.mixture_mass_le line 85
  5. theorem OAI.Problem355.IntegerSamplingPairs.conditional_collisionMass_le line 95
  6. theorem OAI.Problem355.IntegerSamplingPairs.mixture_collisionMass_le line 110
  7. theorem OAI.Problem355.IntegerSamplingPairs.collisionMass_eq_finTwo line 130
  8. def OAI.Problem355.IntegerSamplingPairs.boxColumn line 148
  9. theorem OAI.Problem355.IntegerSamplingPairs.boxColumn_injective line 151
  10. theorem OAI.Problem355.IntegerSamplingPairs.boxColumn_inBox line 157
  11. theorem OAI.Problem355.IntegerSamplingPairs.project_boxColumn line 168
  12. theorem OAI.Problem355.IntegerSamplingPairs.columnLaw_collision_le line 172
  13. theorem OAI.Problem355.IntegerSamplingPairs.box_finTwo_collision_le line 189
  14. theorem OAI.Problem355.IntegerSamplingPairs.mixture_columnLaw_finTwo_collision_le line 204