OAI/Probability/BinarySweep/Trajectories/EndpointOccupancy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.card_gridOutside_mul line 16
  2. lemma OAI.BinaryCoordinateSweeps.sum_endpointLineCount line 21
  3. lemma OAI.BinaryCoordinateSweeps.heavy_count line 28
  4. def OAI.BinaryCoordinateSweeps.holeHeavyLines line 36
  5. def OAI.BinaryCoordinateSweeps.particleHeavyLines line 39
  6. lemma OAI.BinaryCoordinateSweeps.holeHeavy_card line 43
  7. lemma OAI.BinaryCoordinateSweeps.particleHeavy_card line 51
  8. lemma OAI.BinaryCoordinateSweeps.endpoint_not_light line 61
  9. lemma OAI.BinaryCoordinateSweeps.endpoint_line_set_mass line 72
  10. lemma OAI.BinaryCoordinateSweeps.holeHeavy_mass line 85
  11. lemma OAI.BinaryCoordinateSweeps.small_lines_mass line 96
  12. lemma OAI.BinaryCoordinateSweeps.holeHeavy_occupancy_bound line 110
  13. lemma OAI.BinaryCoordinateSweeps.particleHeavy_occupancy_bound line 127