OAI/Probability/BenjaminiSchramm/PublishedConsequences.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Percolation.BenjaminiSchramm.PublishedSimpleGraph line 15
2. def OAI.Percolation.BenjaminiSchramm.triangleDiagram line 22

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:127 (same declaration text).

3. def OAI.Percolation.BenjaminiSchramm.graphDistance line 26

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:131 (same declaration text).

4. def OAI.Percolation.BenjaminiSchramm.ExponentialDecay line 29

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:134 (same declaration text).

5. def OAI.Percolation.BenjaminiSchramm.pexp line 33

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:138 (same declaration text).

6. def OAI.Percolation.BenjaminiSchramm.PowerTail line 36

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:141 (same declaration text).

7. def OAI.Percolation.BenjaminiSchramm.volumeEvent line 40

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:145 (same declaration text).

8. def OAI.Percolation.BenjaminiSchramm.intrinsicRadiusEvent line 43

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:148 (same declaration text).

9. def OAI.Percolation.BenjaminiSchramm.extrinsicRadiusEvent line 46

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:151 (same declaration text).

10. def OAI.Percolation.BenjaminiSchramm.criticalTail line 49

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:154 (same declaration text).

11. def OAI.Percolation.BenjaminiSchramm.CriticalTailLaws line 53

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:158 (same declaration text).

12. def OAI.Percolation.BenjaminiSchramm.SusceptibilityLaw line 58

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:163 (same declaration text).

13. def OAI.Percolation.BenjaminiSchramm.percolationProbability line 64

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:169 (same declaration text).

14. def OAI.Percolation.BenjaminiSchramm.PercolationProbabilityLaw line 67

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:172 (same declaration text).

15. theorem OAI.Percolation.BenjaminiSchramm.triangle_hasSum line 73
16. theorem OAI.Percolation.BenjaminiSchramm.triangleDiagram_eq_matrix line 84
17. theorem OAI.Percolation.BenjaminiSchramm.triangleDiagram_le_norm_cube line 97
18. theorem OAI.Percolation.BenjaminiSchramm.triangleDiagram_le_operatorNorm_cube line 112
19. theorem OAI.Percolation.BenjaminiSchramm.triangleDiagram_lt_top_of_bounded line 120
20. theorem OAI.Percolation.BenjaminiSchramm.critical_triangle_of_mainConclusion line 127
21. def OAI.Percolation.BenjaminiSchramm.HutchcroftExponentialInput line 135
22. theorem OAI.Percolation.BenjaminiSchramm.exponentialDecay_zero line 141
23. theorem OAI.Percolation.BenjaminiSchramm.exponentialDecay_of_publishedInput line 152
24. theorem OAI.Percolation.BenjaminiSchramm.ptwo_le_pexp_of_publishedInput line 176
25. theorem OAI.Percolation.BenjaminiSchramm.exponential_threshold_of_mainConclusion line 183
26. theorem OAI.Percolation.BenjaminiSchramm.law_restrict_finite_cluster line 189
27. def OAI.Percolation.BenjaminiSchramm.criticalFiniteTail line 196
28. theorem OAI.Percolation.BenjaminiSchramm.criticalFiniteTail_eq line 200
29. def OAI.Percolation.BenjaminiSchramm.HutchcroftCriticalVolumeInput line 208
30. def OAI.Percolation.BenjaminiSchramm.HutchcroftCriticalRadiiInput line 212
31. theorem OAI.Percolation.BenjaminiSchramm.criticalTailLaws_of_publishedInputs line 217
32. def OAI.Percolation.BenjaminiSchramm.HutchcroftFirstMomentInput line 232
33. theorem OAI.Percolation.BenjaminiSchramm.susceptibilityLaw_of_publishedInput line 239
34. def OAI.Percolation.BenjaminiSchramm.TrianglePercolationProbabilityInput line 250
35. theorem OAI.Percolation.BenjaminiSchramm.percolationProbabilityLaw_of_publishedInput line 254
36. theorem OAI.Percolation.BenjaminiSchramm.meanFieldLaws_of_publishedInputs line 260