OAI/Probability/CriticalPercolation/GraphGeometry/LatticeGrowth.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.Corridor.slotSite line 16
  2. lemma OAI.CriticalPercolation.Corridor.slotSite_quadrant line 18
  3. lemma OAI.CriticalPercolation.Corridor.gridSlot_slotSite line 21
  4. lemma OAI.CriticalPercolation.Corridor.slotSite_gridSlot line 24
  5. lemma OAI.CriticalPercolation.Corridor.slotSite_zero line 28
  6. lemma OAI.CriticalPercolation.Corridor.parent_slot_lt line 30
  7. lemma OAI.CriticalPercolation.Corridor.target_quadrant line 37
  8. def OAI.CriticalPercolation.Corridor.incoming line 42
  9. lemma OAI.CriticalPercolation.Corridor.incoming_source line 46
  10. lemma OAI.CriticalPercolation.Corridor.incoming_target line 57
  11. lemma OAI.CriticalPercolation.Corridor.incoming_exists line 68
  12. structure OAI.CriticalPercolation.Corridor.GrowthState line 79
  13. def OAI.CriticalPercolation.Corridor.GrowthState.initial line 83
  14. def OAI.CriticalPercolation.Corridor.GrowthState.advance line 85
  15. lemma OAI.CriticalPercolation.Corridor.GrowthState.good_mono line 89
  16. lemma OAI.CriticalPercolation.Corridor.GrowthState.seen_mono line 96
  17. def OAI.CriticalPercolation.Corridor.GrowthState.Valid line 99
  18. lemma OAI.CriticalPercolation.Corridor.GrowthState.initial_valid line 104
  19. lemma OAI.CriticalPercolation.Corridor.GrowthState.advance_valid line 111
  20. lemma OAI.CriticalPercolation.Corridor.GrowthState.seen_intersection line 127
  21. def OAI.CriticalPercolation.Corridor.GrowthState.Covered line 145
  22. lemma OAI.CriticalPercolation.Corridor.GrowthState.initial_covered line 148
  23. lemma OAI.CriticalPercolation.Corridor.GrowthState.advance_covered line 152
  24. lemma OAI.CriticalPercolation.Corridor.GrowthState.active_pos line 168
  25. lemma OAI.CriticalPercolation.Corridor.GrowthState.outgoing_nonincident line 175