OAI/Probability/CriticalPercolation/Modular/OrderMass.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalPercolation.FiniteEntropy.integral_sq_le_mass_mul line 22
  2. def OAI.CriticalPercolation.Priority.orderMass line 53
  3. def OAI.CriticalPercolation.Priority.orderWeight line 54
  4. def OAI.CriticalPercolation.Priority.orderSquare line 56
  5. lemma OAI.CriticalPercolation.Priority.orderMass_nonneg line 59
  6. lemma OAI.CriticalPercolation.Priority.orderSquare_nonneg line 60
  7. lemma OAI.CriticalPercolation.Priority.orderWeight_sq_le line 63
  8. lemma OAI.CriticalPercolation.Priority.sum_orderMass line 72
  9. lemma OAI.CriticalPercolation.Priority.sum_orderSquare line 77
  10. def OAI.CriticalPercolation.Priority.priorList line 83
  11. def OAI.CriticalPercolation.Priority.suffix line 84
  12. lemma OAI.CriticalPercolation.Priority.priorList_suffix line 86
  13. lemma OAI.CriticalPercolation.Priority.not_before_iff line 90
  14. def OAI.CriticalPercolation.Priority.First line 107
  15. lemma OAI.CriticalPercolation.Priority.first_iff_fresh line 110
  16. lemma OAI.CriticalPercolation.Priority.weighted_first_identity line 115