OAI/Probability/CriticalZ3/Exploration.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CriticalZ3.Coarse.Packet line 14

    Source documentation

    A packet stores exactly the finite parent-chain graph, extended only on assignment.

    structure Packet (r : ℕ) where
…
  2. def OAI.CriticalZ3.Coarse.Packet.event line 23
  3. theorem OAI.CriticalZ3.Coarse.Packet.measurableSet_event line 26
  4. theorem OAI.CriticalZ3.Coarse.Packet.event_determined line 29
  5. def OAI.CriticalZ3.Coarse.Packet.child line 33
  6. theorem OAI.CriticalZ3.Coarse.Packet.child_bits line 40
  7. structure OAI.CriticalZ3.Coarse.Exploration line 45
  8. def OAI.CriticalZ3.Coarse.Exploration.visited line 54
  9. def OAI.CriticalZ3.Coarse.Exploration.reveal line 56
  10. def OAI.CriticalZ3.Coarse.Exploration.after line 60
  11. def OAI.CriticalZ3.Coarse.Exploration.candidates line 62
  12. def OAI.CriticalZ3.Coarse.Exploration.Accept line 65
  13. def OAI.CriticalZ3.Coarse.Exploration.markedBad line 69
  14. def OAI.CriticalZ3.Coarse.Exploration.advance line 74
  15. theorem OAI.CriticalZ3.Coarse.Exploration.reveal_disjoint line 88
  16. def OAI.CriticalZ3.Coarse.Exploration.scheme line 93
  17. structure OAI.CriticalZ3.Coarse.Exploration.Valid line 102
  18. theorem OAI.CriticalZ3.Coarse.outward_injective line 118
  19. theorem OAI.CriticalZ3.Coarse.neighbor_ne line 122
  20. theorem OAI.CriticalZ3.Coarse.Exploration.mem_candidates line 130
  21. theorem OAI.CriticalZ3.Coarse.Exploration.queue_visited line 134
  22. theorem OAI.CriticalZ3.Coarse.Exploration.processed_visited line 138
  23. theorem OAI.CriticalZ3.Coarse.Exploration.candidates_distinct line 140
  24. theorem OAI.CriticalZ3.Coarse.Exploration.advance_empty line 149
  25. theorem OAI.CriticalZ3.Coarse.Exploration.current_support line 158
  26. theorem OAI.CriticalZ3.Coarse.Exploration.later_disjoint line 169
  27. theorem OAI.CriticalZ3.Coarse.Exploration.later_probability line 189
  28. theorem OAI.CriticalZ3.Coarse.Exploration.valid_advance line 199