OAI/MeasureTheory/Falconer/Recursion/PolicyFarSuccessors.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual positive states of a comparable far collision

The two new endpoint cells lie in the same original endpoint cell. Both retain the descriptor masks and reset only the positive interval and index.

  1. theorem OAI.Falconer.PolicyJetData.partner_lengths line 19
  2. def OAI.Falconer.PolicyJetData.farPositiveSuccessor line 27
  3. theorem OAI.Falconer.PolicyJetData.farPositiveSuccessor_state line 36
  4. theorem OAI.Falconer.PolicyJetData.farPositiveSuccessor_count line 42
  5. theorem OAI.Falconer.PolicyJetData.farPositiveSuccessor_geometry line 50
  6. theorem OAI.Falconer.PolicyJetData.farCollisionMaximum_le_positive_successors line 80