OAI/Probability/CriticalPercolation/Clusters/ForcedDisconnectContinuity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.forcedClosedSeparated line 19
2. def OAI.CriticalPercolation.BondGraph.disconnectedIndicator line 22
3. lemma OAI.CriticalPercolation.BondGraph.forcedClosedSeparated_of_ends line 25
4. lemma OAI.CriticalPercolation.BondGraph.disconnectedIndicator_of_ends line 39
5. lemma OAI.CriticalPercolation.BondGraph.measurable_forcedClosedSeparated line 43
6. lemma OAI.CriticalPercolation.BondGraph.measurable_disconnectedIndicator line 57
7. lemma OAI.CriticalPercolation.BondGraph.norm_disconnectedIndicator_le line 61
8. lemma OAI.CriticalPercolation.BondGraph.clusterCountDrop_eq_disconnected_of_finite line 65
9. lemma OAI.CriticalPercolation.BondGraph.clusterCountDrop_le_disconnected line 75
10. lemma OAI.CriticalPercolation.BondGraph.finite_clusters_ae_of_subcritical line 83
11. lemma OAI.CriticalPercolation.BondGraph.clusterCountDrop_eq_disconnected_ae_subcritical line 93
12. lemma OAI.CriticalPercolation.BondGraph.eventually_disconnectedIndicator line 100
13. lemma OAI.CriticalPercolation.BondGraph.integral_atParameter line 118
14. theorem OAI.CriticalPercolation.BondGraph.tendsto_integral_disconnectedIndicator line 125