OAI/Probability/BinarySweep/Trajectories/EndpointEvents.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.gridLayer_at line 15
  2. lemma OAI.BinaryCoordinateSweeps.independentPosition_zero line 19
  3. lemma OAI.BinaryCoordinateSweeps.independentPosition_last line 22
  4. def OAI.BinaryCoordinateSweeps.endpointLine line 25
  5. lemma OAI.BinaryCoordinateSweeps.endpoint_gridLayer_iff line 28
  6. lemma OAI.BinaryCoordinateSweeps.gridSweep_endpoint_iff line 46
  7. def OAI.BinaryCoordinateSweeps.localEndpointEvent line 63
  8. def OAI.BinaryCoordinateSweeps.endpointMass line 67
  9. def OAI.BinaryCoordinateSweeps.localEndpointMass line 72
  10. lemma OAI.BinaryCoordinateSweeps.endpointMass_factor line 77
  11. lemma OAI.BinaryCoordinateSweeps.localEndpointEvent_insert line 105
  12. lemma OAI.BinaryCoordinateSweeps.localEndpointEvent_empty_line line 112
  13. lemma OAI.BinaryCoordinateSweeps.assigns_empty_line line 118