OAI/Probability/CriticalPercolation/Modular/ObjectAvoidMass.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.objectAvoidMass line 21
2. def OAI.CriticalPercolation.BondGraph.objectAvoidTotal line 25
3. lemma OAI.CriticalPercolation.BondGraph.avg_objectAvoidMass line 28
4. lemma OAI.CriticalPercolation.BondGraph.objectAvoidMass_nonneg line 40
5. lemma OAI.CriticalPercolation.BondGraph.sum_objectAvoidMass line 47
6. lemma OAI.CriticalPercolation.BondGraph.objectAvoidTotal_symm line 53
7. lemma OAI.CriticalPercolation.BondGraph.objectAvoidTotal_le_one line 62
8. lemma OAI.CriticalPercolation.BondGraph.objectAvoidTotal_minorization line 70
9. lemma OAI.CriticalPercolation.BondGraph.objectAvoidMass_halfstationary line 81
10. def OAI.CriticalPercolation.BondGraph.objectAvoidLaw line 94
11. lemma OAI.CriticalPercolation.BondGraph.objectAvoidLaw_stationary line 97
12. theorem OAI.CriticalPercolation.BondGraph.objectAvoidLaw_associated line 109
13. lemma OAI.CriticalPercolation.BondGraph.avg_objectAvoidLaw line 134
14. theorem OAI.CriticalPercolation.BondGraph.clusterObject_avoidance_cross line 141