OAI/Probability/FirstPassage/WitnessEntropy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.spatialNeighbors line 10
  2. lemma OAI.PlanarFPP.spatialNeighbors_card line 13
  3. lemma OAI.PlanarFPP.mem_spatialNeighbors line 17
  4. def OAI.PlanarFPP.spatialItineraries line 23
  5. lemma OAI.PlanarFPP.spatialItineraries_card line 27
  6. lemma OAI.PlanarFPP.mem_spatialItineraries line 38
  7. def OAI.PlanarFPP.increaseFirst line 50
  8. def OAI.PlanarFPP.compositionCandidates line 54
  9. lemma OAI.PlanarFPP.compositionCandidates_card line 61
  10. lemma OAI.PlanarFPP.mem_compositionCandidates line 75
  11. def OAI.PlanarFPP.compositionCover line 117
  12. lemma OAI.PlanarFPP.mem_compositionCover line 120
  13. lemma OAI.PlanarFPP.compositionCover_card line 125