OAI/Analysis/LipschitzFree/GraphWalks.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Matched graph walks and exceptional record estimates

  1. def OAI.DiscreteFree.PortGraph.Matched line 20
  2. theorem OAI.DiscreteFree.PortGraph.Matched.compat line 24
  3. theorem OAI.DiscreteFree.PortGraph.Matched.take line 30
  4. def OAI.DiscreteFree.PortGraph.Good line 42
  5. theorem OAI.DiscreteFree.PortGraph.Good.length_lt line 45
  6. def OAI.DiscreteFree.PortGraph.RecordLength line 54
  7. def OAI.DiscreteFree.PortGraph.record line 58
  8. theorem OAI.DiscreteFree.PortGraph.record_spec line 61
  9. theorem OAI.DiscreteFree.PortGraph.record_le line 65
  10. theorem OAI.DiscreteFree.PortGraph.le_record line 68
  11. theorem OAI.DiscreteFree.PortGraph.record_extension line 74
  12. theorem OAI.DiscreteFree.PortGraph.matched_exceptional_endpoint line 88
  13. theorem OAI.DiscreteFree.PortGraph.Matched.exists_based line 112