OAI/Probability/CriticalPercolation/GraphGeometry/UpdateKernel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.updateKernel line 21
2. lemma OAI.CriticalPercolation.BondGraph.clusterUpdate_eq_sum line 25
3. lemma OAI.CriticalPercolation.BondGraph.updateKernel_nonneg line 38
4. lemma OAI.CriticalPercolation.BondGraph.updateKernel_mass line 42
5. lemma OAI.CriticalPercolation.BondGraph.allClosed_weight_le_kernel line 48
6. lemma OAI.CriticalPercolation.BondGraph.avoidedAverage_eq_sum line 62
7. def OAI.CriticalPercolation.BondGraph.avoidedLaw line 73
8. lemma OAI.CriticalPercolation.BondGraph.avoidedLaw_avg line 77
9. lemma OAI.CriticalPercolation.BondGraph.avoidedLaw_nonneg line 86
10. lemma OAI.CriticalPercolation.BondGraph.allClosed_weight_le_avoidance line 92
11. lemma OAI.CriticalPercolation.BondGraph.avoidance_pos line 103
12. lemma OAI.CriticalPercolation.BondGraph.avoidedLaw_mass line 109
13. lemma OAI.CriticalPercolation.BondGraph.avoidedLaw_stationary line 116
14. lemma OAI.CriticalPercolation.BondGraph.tendsto_clusterUpdate line 124