OAI/Probability/CriticalPercolation/Modular/NormalizedIncidenceTransport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.Aut.mem_ends_iff line 16
2. lemma OAI.CriticalPercolation.BondGraph.Aut.incident_cluster_iff line 21
3. lemma OAI.CriticalPercolation.BondGraph.measurable_incidentCluster line 31
4. def OAI.CriticalPercolation.BondGraph.normalizedSelectedIncidence line 35
5. def OAI.CriticalPercolation.BondGraph.normalizedIncidenceTransport line 39
6. lemma OAI.CriticalPercolation.BondGraph.measurable_normalizedSelectedIncidence line 43
7. lemma OAI.CriticalPercolation.BondGraph.measurable_normalizedIncidenceTransport line 50
8. lemma OAI.CriticalPercolation.BondGraph.Aut.normalizedIncidenceTransport line 58
9. lemma OAI.CriticalPercolation.BondGraph.normalizedIncidenceTransport_out line 67
10. lemma OAI.CriticalPercolation.BondGraph.normalizedIncidenceTransport_in line 88
11. lemma OAI.CriticalPercolation.BondGraph.normalizedSelectedIncidence_le line 109
12. theorem OAI.CriticalPercolation.BondGraph.expected_normalizedSelectedIncidence line 130