OAI/Probability/CriticalPercolation/Modular/ClusterMassInfinite.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.FiniteClusters.size line 15
  2. def OAI.CriticalPercolation.FiniteClusters.mass line 17
  3. def OAI.CriticalPercolation.FiniteClusters.coefficient line 19
  4. def OAI.CriticalPercolation.FiniteClusters.rootSum line 21
  5. def OAI.CriticalPercolation.FiniteClusters.rootDiscrepancy line 24
  6. def OAI.CriticalPercolation.FiniteClusters.rootAbsolute line 27
  7. def OAI.CriticalPercolation.FiniteClusters.edgeMass line 30
  8. def OAI.CriticalPercolation.FiniteClusters.edgeDiscrepancy line 35
  9. lemma OAI.CriticalPercolation.FiniteClusters.size_eq_of_reachable line 38
  10. lemma OAI.CriticalPercolation.FiniteClusters.mass_eq_of_reachable line 43
  11. lemma OAI.CriticalPercolation.FiniteClusters.mass_nonneg line 48
  12. lemma OAI.CriticalPercolation.FiniteClusters.cappedMass_le_one line 51
  13. lemma OAI.CriticalPercolation.FiniteClusters.mass_mul_size_le_one line 53
  14. lemma OAI.CriticalPercolation.FiniteClusters.mass_eq_zero_of_infinite line 60
  15. lemma OAI.CriticalPercolation.FiniteClusters.coefficient_abs_le line 64
  16. lemma OAI.CriticalPercolation.FiniteClusters.rootAbsolute_nonneg line 73
  17. lemma OAI.CriticalPercolation.FiniteClusters.abs_rootDiscrepancy line 76
  18. lemma OAI.CriticalPercolation.FiniteClusters.rootAbsolute_bound line 81
  19. lemma OAI.CriticalPercolation.FiniteClusters.edgeMass_nonneg line 113
  20. lemma OAI.CriticalPercolation.FiniteClusters.edgeMass_le_two line 119
  21. lemma OAI.CriticalPercolation.FiniteClusters.edgeDiscrepancy_abs_le line 125
  22. lemma OAI.CriticalPercolation.FiniteClusters.measurable_size line 135
  23. lemma OAI.CriticalPercolation.FiniteClusters.measurable_mass line 138
  24. lemma OAI.CriticalPercolation.FiniteClusters.measurable_coefficient line 143
  25. lemma OAI.CriticalPercolation.FiniteClusters.measurable_incidentCluster line 146
  26. lemma OAI.CriticalPercolation.FiniteClusters.measurable_rootSum line 150
  27. lemma OAI.CriticalPercolation.FiniteClusters.measurable_rootAbsolute line 154
  28. lemma OAI.CriticalPercolation.FiniteClusters.measurable_rootDiscrepancy line 158
  29. lemma OAI.CriticalPercolation.FiniteClusters.measurable_edgeMass line 162
  30. lemma OAI.CriticalPercolation.FiniteClusters.measurable_edgeDiscrepancy line 166