OAI/Probability/CriticalPercolation/Modular/ExpectedIncidenceTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.lintegral_ne_top_of_uniform_bound line 14
2. lemma OAI.CriticalPercolation.sum_integral_toReal line 20
3. def OAI.CriticalPercolation.BondGraph.selectedIncidenceReturn line 35
4. lemma OAI.CriticalPercolation.BondGraph.selectedIncidenceReturn_eq_tsum line 39
5. lemma OAI.CriticalPercolation.BondGraph.measurable_selectedIncidenceReturn line 47
6. lemma OAI.CriticalPercolation.BondGraph.selectedIncidenceReturn_le line 52
7. lemma OAI.CriticalPercolation.BondGraph.selectedIncidenceReturn_toReal line 62
8. lemma OAI.CriticalPercolation.BondGraph.expected_selectedIncidence_real line 73