OAI/Probability/CriticalZ3/RelayProbability.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalZ3.Model.Internal line 15
  2. def OAI.CriticalZ3.Model.UniformOn line 19
  3. theorem OAI.CriticalZ3.Model.box_internal line 22
  4. theorem OAI.CriticalZ3.Model.internal_mono line 26
  5. theorem OAI.CriticalZ3.Model.UniformOn.box line 32
  6. theorem OAI.CriticalZ3.Model.seedReaches_target_mono line 36
  7. theorem OAI.CriticalZ3.Model.seedReaches_image_probability line 41
  8. def OAI.CriticalZ3.LatticeGraph.ContainsSet line 66
  9. theorem OAI.CriticalZ3.LatticeGraph.ContainsSet.box line 69
  10. def OAI.CriticalZ3.Box.rect line 80
  11. theorem OAI.CriticalZ3.Box.contains_rect line 83
  12. def OAI.CriticalZ3.Box.framedRect line 97
  13. theorem OAI.CriticalZ3.Box.abs_vertex_sub line 100
  14. theorem OAI.CriticalZ3.Box.framedRect_map line 109
  15. theorem OAI.CriticalZ3.Box.framedRect_expand_map line 118
  16. theorem OAI.CriticalZ3.ScaleData.radius_seed line 131
  17. theorem OAI.CriticalZ3.ScaleData.extension_interface line 137
  18. theorem OAI.MeasureTheory.finite_relay_bound line 167
  19. theorem OAI.CriticalZ3.ScaleData.R_pos line 190
  20. theorem OAI.CriticalZ3.ScaleData.route_width_nonneg line 192
  21. def OAI.CriticalZ3.ScaleData.routeBox line 199
  22. theorem OAI.CriticalZ3.ScaleData.routeBox_contains line 203
  23. theorem OAI.CriticalZ3.ScaleData.relay_in_frame line 209