OAI/Probability/CriticalPercolation/Modular/HeavyFiniteGeometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.distinctHeavyEvent line 18
2. lemma OAI.CriticalPercolation.BondGraph.measurableSet_distinctHeavyEvent line 22
3. lemma OAI.CriticalPercolation.BondGraph.Aut.distinctHeavyEvent_image_iff line 27
4. lemma OAI.CriticalPercolation.BondGraph.Aut.distinctHeavyEvent_measure line 37
5. lemma OAI.CriticalPercolation.BondGraph.distinctHeavy_force_adjacent_length line 49
6. lemma OAI.CriticalPercolation.BondGraph.distinctHeavy_force_adjacent line 87
7. lemma OAI.CriticalPercolation.BondGraph.atMostOneHeavy_ae_of_adjacent_null line 94