OAI/Probability/UnimodularPercolation/TwoCluster/Transport.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Percolation.clusterDensity line 18
2. def OAI.Percolation.densityInfluence line 21
3. theorem OAI.Percolation.clusterDensity_nonneg line 25
4. theorem OAI.Percolation.clusterDensity_le_one line 28
5. theorem OAI.Percolation.clusterDensity_antitone line 31
6. theorem OAI.Percolation.densityInfluence_nonneg line 40
7. theorem OAI.Percolation.densityInfluence_le_one line 47
8. theorem OAI.Percolation.measurable_clusterDensity line 54
9. theorem OAI.Percolation.measurable_densityInfluence line 58
10. theorem OAI.Percolation.integrable_densityInfluence line 64
11. theorem OAI.Percolation.cluster_insert_finite line 72
12. theorem OAI.Percolation.cluster_insert_finite_ae line 83
13. theorem OAI.Percolation.finiteDensity_eq_clusterDensity line 92
14. theorem OAI.Percolation.domainBits_insert line 104
15. theorem OAI.Percolation.densityInfluence_tendsto_finite line 110
16. theorem OAI.Percolation.densityInfluence_integral_tendsto line 139
17. theorem OAI.Percolation.densityInfluence_finite_sum_bound line 160
18. theorem OAI.Percolation.densityInfluence_lintegral_sum_bound line 186
19. def OAI.Percolation.boundaryDensityInfluence line 215
20. def OAI.Percolation.localDensityLoss line 219
21. theorem OAI.Percolation.measurable_boundaryDensityInfluence line 223
22. theorem OAI.Percolation.measurable_localDensityLoss line 232
23. theorem OAI.Percolation.densityInfluence_eq_of_conn line 238
24. theorem OAI.Percolation.densityInfluence_aut line 245
25. theorem OAI.Percolation.localDensityLoss_aut line 254
26. theorem OAI.Percolation.tsum_bond_endpoints_le_two line 272
27. theorem OAI.Percolation.clusterAveraged_localDensityLoss_le line 290
28. theorem OAI.Percolation.clusterAveraged_localDensityLoss_integral_bound line 315
29. theorem OAI.Percolation.weighted_localDensityLoss_bound line 334