OAI/Probability/CriticalPercolation/Gluing/MoveWitness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.boxMove line 17
2. lemma OAI.CriticalPercolation.BondGraph.coordinateMove_eq_boxMove line 22
3. lemma OAI.CriticalPercolation.BondGraph.walk_induced_support line 25
4. lemma OAI.CriticalPercolation.BondGraph.boxMove_eq_restrictedSeed line 41
5. lemma OAI.CriticalPercolation.BondGraph.restrictedSeed_upper line 57
6. lemma OAI.CriticalPercolation.BondGraph.restrictedSeed_finiteWitness line 61
7. lemma OAI.CriticalPercolation.BondGraph.boxMove_upper line 71
8. lemma OAI.CriticalPercolation.BondGraph.boxMove_finiteWitness line 76
9. lemma OAI.CriticalPercolation.BondGraph.boxMove_measurable line 81
10. lemma OAI.CriticalPercolation.BondGraph.lower_two_boxMoves line 87