OAI/Probability/CriticalPercolation/Modular/ModularClusterMass.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.BondGraph.stabilizerWeight line 14
  2. def OAI.CriticalPercolation.BondGraph.modularMass line 16
  3. lemma OAI.CriticalPercolation.BondGraph.stabilizerWeight_ne_top line 19
  4. lemma OAI.CriticalPercolation.BondGraph.stabilizerWeight_pos line 22
  5. lemma OAI.CriticalPercolation.BondGraph.stabilizerWeight_self line 26
  6. lemma OAI.CriticalPercolation.BondGraph.stabilizerWeight_change_base line 29
  7. lemma OAI.CriticalPercolation.BondGraph.modularMass_change_base line 37
  8. lemma OAI.CriticalPercolation.BondGraph.modularMass_eq_top_change_base line 48
  9. lemma OAI.CriticalPercolation.BondGraph.modularMass_mono line 53
  10. lemma OAI.CriticalPercolation.BondGraph.modularMass_finite line 63
  11. lemma OAI.CriticalPercolation.BondGraph.infinite_of_modularMass_top line 75
  12. lemma OAI.CriticalPercolation.BondGraph.Aut.stabilizerWeight line 82
  13. lemma OAI.CriticalPercolation.BondGraph.Aut.modularMass_image line 86
  14. def OAI.CriticalPercolation.BondGraph.lightInfiniteEvent line 94
  15. def OAI.CriticalPercolation.BondGraph.heavyClusterEvent line 97
  16. lemma OAI.CriticalPercolation.BondGraph.measurable_modularClusterMass line 100
  17. lemma OAI.CriticalPercolation.BondGraph.measurableSet_lightInfiniteEvent line 106
  18. lemma OAI.CriticalPercolation.BondGraph.measurableSet_heavyClusterEvent line 111
  19. lemma OAI.CriticalPercolation.BondGraph.infiniteEvent_eq_light_union_heavy line 115