OAI/Analysis/HardSphere/Geometry/BadGraph.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Lattice.badGraph line 15
  2. def OAI.HardSphere.Lattice.badComponent line 20
  3. def OAI.HardSphere.Lattice.badComponents line 23
  4. lemma OAI.HardSphere.Lattice.mem_badComponent line 26
  5. lemma OAI.HardSphere.Lattice.mem_own_badComponent line 30
  6. lemma OAI.HardSphere.Lattice.badComponent_subset line 33
  7. lemma OAI.HardSphere.Lattice.badComponent_eq_of_reachable line 36
  8. lemma OAI.HardSphere.Lattice.badComponents_disjoint line 43
  9. lemma OAI.HardSphere.Lattice.badComponents_subset line 54
  10. lemma OAI.HardSphere.Lattice.badComponents_nonempty line 59
  11. def OAI.HardSphere.Lattice.candidateSets line 64
  12. lemma OAI.HardSphere.Lattice.reachable_inside_component line 68
  13. lemma OAI.HardSphere.Lattice.badComponents_candidate line 81
  14. abbrev OAI.HardSphere.Lattice.ExploreState line 92
  15. def OAI.HardSphere.Lattice.frontierHead line 94
  16. lemma OAI.HardSphere.Lattice.frontierHead_mem line 97
  17. def OAI.HardSphere.Lattice.exploreNext line 100
  18. def OAI.HardSphere.Lattice.exploreStep line 106
  19. def OAI.HardSphere.Lattice.exploration line 110
  20. def OAI.HardSphere.Lattice.ExploreInvariant line 114
  21. lemma OAI.HardSphere.Lattice.invariant_initial line 119
  22. lemma OAI.HardSphere.Lattice.invariant_step line 123
  23. lemma OAI.HardSphere.Lattice.exploration_invariant line 159
  24. lemma OAI.HardSphere.Lattice.invariant_empty_frontier line 166
  25. lemma OAI.HardSphere.Lattice.exploreStep_card line 178
  26. lemma OAI.HardSphere.Lattice.exploration_covers line 186
  27. def OAI.HardSphere.Lattice.possibleSteps line 211
  28. lemma OAI.HardSphere.Lattice.exploreStep_mem_possible line 216
  29. def OAI.HardSphere.Lattice.possibleStates line 223
  30. lemma OAI.HardSphere.Lattice.exploration_mem_possible line 227
  31. lemma OAI.HardSphere.Lattice.possibleSteps_card_le line 233
  32. lemma OAI.HardSphere.Lattice.possibleStates_card_le line 245
  33. def OAI.HardSphere.Lattice.rootedAnimals line 259
  34. lemma OAI.HardSphere.Lattice.rootedAnimals_card_le line 262
  35. lemma OAI.HardSphere.Lattice.badGraph_mono line 276
  36. lemma OAI.HardSphere.Lattice.internal_boundary line 282
  37. lemma OAI.HardSphere.Lattice.connected_insert line 294
  38. lemma OAI.HardSphere.Lattice.exists_rooted_subanimal line 307
  39. lemma OAI.HardSphere.Lattice.prod_ite_mem line 333
  40. def OAI.HardSphere.Lattice.JointBadLaw line 342
  41. lemma OAI.HardSphere.Lattice.component_event_bound line 347
  42. theorem OAI.HardSphere.Lattice.environment_product_bound line 378