OAI/Probability/SignedSweeps/UniquePaths.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.sweepPrefix line 12
  2. lemma OAI.SignedSweeps.sweepPrefix_zero line 15
  3. lemma OAI.SignedSweeps.sweepPrefix_full line 18
  4. lemma OAI.SignedSweeps.sweepPrefix_succ line 23
  5. lemma OAI.SignedSweeps.coordinateSubgroup_bit line 29
  6. lemma OAI.SignedSweeps.sweepPrefix_before line 34
  7. lemma OAI.SignedSweeps.sweepPrefix_after line 44
  8. def OAI.SignedSweeps.endpointPath line 57
  9. lemma OAI.SignedSweeps.endpointPath_zero line 60
  10. lemma OAI.SignedSweeps.endpointPath_full line 63
  11. lemma OAI.SignedSweeps.endpointPath_bit line 66
  12. lemma OAI.SignedSweeps.sweepPrefix_eq_endpointPath line 71
  13. def OAI.SignedSweeps.pathAddress line 82
  14. lemma OAI.SignedSweeps.layerSettings_endpointPath line 85
  15. lemma OAI.SignedSweeps.sampleSweep_endpoints_iff line 102
  16. def OAI.SignedSweeps.endpointEncounter line 131