OAI/Probability/CriticalPercolation/GraphGeometry/CoordinateScheme.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CriticalPercolation.Corridor.CoordinateData line 17
2. def OAI.CriticalPercolation.Corridor.CoordinateData.T line 42
3. def OAI.CriticalPercolation.Corridor.CoordinateData.scheme line 44
4. structure OAI.CriticalPercolation.Corridor.CoordinateData.Bounds line 54
5. lemma OAI.CriticalPercolation.Corridor.CoordinateData.T_pos line 88
6. lemma OAI.CriticalPercolation.Corridor.CoordinateData.L_large line 90
7. lemma OAI.CriticalPercolation.Corridor.CoordinateData.small_rho line 94
8. lemma OAI.CriticalPercolation.Corridor.CoordinateData.layout line 102
9. lemma OAI.CriticalPercolation.Corridor.CoordinateData.root_seed line 110
10. lemma OAI.CriticalPercolation.Corridor.CoordinateData.marks_disjoint line 116
11. lemma OAI.CriticalPercolation.Corridor.CoordinateData.domain_eq line 123
12. lemma OAI.CriticalPercolation.Corridor.CoordinateData.local_time_step line 129
13. lemma OAI.CriticalPercolation.Corridor.CoordinateData.local_height_step line 133
14. lemma OAI.CriticalPercolation.Corridor.CoordinateData.source_behind line 137