OAI/Probability/CriticalZ3/Coarse.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CriticalZ3.Coarse.Point line 12
  2. abbrev OAI.CriticalZ3.Coarse.Direction line 13
  3. abbrev OAI.CriticalZ3.Coarse.outward line 14
  4. def OAI.CriticalZ3.Coarse.center line 16
  5. def OAI.CriticalZ3.Coarse.Q line 17
  6. def OAI.CriticalZ3.Coarse.B line 18
  7. def OAI.CriticalZ3.Coarse.PairRegion line 19
  8. theorem OAI.CriticalZ3.Coarse.center_zero line 21
  9. theorem OAI.CriticalZ3.Coarse.cube_unique line 23
  10. theorem OAI.CriticalZ3.Coarse.Q_disjoint line 41
  11. theorem OAI.CriticalZ3.Coarse.B_subset_Q line 46
  12. theorem OAI.CriticalZ3.Coarse.zero_in_Q line 51
  13. theorem OAI.CriticalZ3.Coarse.zero_outside_pair line 55
  14. def OAI.CriticalZ3.Coarse.interface line 61
  15. theorem OAI.CriticalZ3.Coarse.mem_interface line 66
  16. theorem OAI.CriticalZ3.Coarse.interface_comm line 73
  17. theorem OAI.CriticalZ3.Coarse.interface_eq_endpoints line 77
  18. theorem OAI.CriticalZ3.Coarse.internal_not_interface line 87
  19. theorem OAI.CriticalZ3.Coarse.internal_pair_bond line 97
  20. def OAI.CriticalZ3.Coarse.frame line 103
  21. theorem OAI.CriticalZ3.Coarse.frame_zero line 108
  22. theorem OAI.CriticalZ3.Coarse.frame_next line 112
  23. theorem OAI.CriticalZ3.Coarse.relay_cube_eq line 118
  24. theorem OAI.CriticalZ3.Coarse.image_cube line 131
  25. theorem OAI.CriticalZ3.Coarse.prism_eq_cubes line 139
  26. theorem OAI.CriticalZ3.Coarse.frame_prism line 178
  27. theorem OAI.CriticalZ3.Coarse.neighboring_relay line 186
  28. def OAI.CriticalZ3.LatticeGraph.Subgraph line 203
  29. theorem OAI.CriticalZ3.LatticeGraph.conn_inclusion line 205
  30. theorem OAI.CriticalZ3.LatticeGraph.meets_inclusion line 219
  31. def OAI.CriticalZ3.LatticeGraph.ofBox line 225
  32. theorem OAI.CriticalZ3.LatticeGraph.ofBox_contains line 231
  33. def OAI.CriticalZ3.Coarse.linkBits line 235
  34. def OAI.CriticalZ3.Coarse.block line 238
  35. def OAI.CriticalZ3.Coarse.rootBits line 240
  36. def OAI.CriticalZ3.Coarse.exposed line 242
  37. theorem OAI.CriticalZ3.Coarse.bits_disjoint line 246
  38. theorem OAI.CriticalZ3.Coarse.bits_link_disjoint line 254
  39. theorem OAI.CriticalZ3.Coarse.block_disjoint line 260
  40. theorem OAI.CriticalZ3.Coarse.block_subset_exposed_insert line 277
  41. theorem OAI.CriticalZ3.Coarse.exposed_mono line 287
  42. theorem OAI.CriticalZ3.Coarse.internal_pair_not_exposed line 296
  43. def OAI.CriticalZ3.Coarse.extendGraph line 348
  44. theorem OAI.CriticalZ3.Coarse.extendGraph_subgraph line 371
  45. theorem OAI.CriticalZ3.Coarse.extendGraph_contains line 375
  46. theorem OAI.CriticalZ3.Coarse.extendGraph_bits line 379
  47. theorem OAI.CriticalZ3.Coarse.extendGraph_pair line 387