OAI/Probability/CriticalPercolation/Clusters/ExpectedCluster.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.finite_spatialMarkov line 18
2. def OAI.CriticalPercolation.BondGraph.expectedCluster line 34
3. def OAI.CriticalPercolation.BondGraph.expectedResidual line 38
4. lemma OAI.CriticalPercolation.BondGraph.expectedResidual_eq line 47
5. lemma OAI.CriticalPercolation.BondGraph.expectedResidual_nonneg line 71
6. lemma OAI.CriticalPercolation.BondGraph.expectedResidual_monotone line 78