OAI/Probability/CriticalPercolation/Entropy/BinaryRaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.BondGraph.rawContact line 15
  2. lemma OAI.CriticalPercolation.BondGraph.rawContact_nonneg line 23
  3. lemma OAI.CriticalPercolation.BondGraph.rawContact_sum line 36
  4. lemma OAI.CriticalPercolation.BondGraph.contactKernel_le_raw line 47
  5. lemma OAI.CriticalPercolation.BinaryLaw.anchorSet_sides line 73
  6. def OAI.CriticalPercolation.BinaryLaw.scheduledAnchor line 77
  7. def OAI.CriticalPercolation.BinaryLaw.scheduledTargets line 80
  8. lemma OAI.CriticalPercolation.BinaryLaw.scheduledAnchor_eq line 83
  9. lemma OAI.CriticalPercolation.BinaryLaw.scheduledTargets_eq line 88
  10. lemma OAI.CriticalPercolation.BinaryLaw.prefix_succ_fst line 93
  11. lemma OAI.CriticalPercolation.BinaryLaw.scheduledTargets_anchors line 104
  12. def OAI.CriticalPercolation.BinaryLaw.rawProduct line 135
  13. lemma OAI.CriticalPercolation.BinaryLaw.rawProduct_nonneg line 141
  14. lemma OAI.CriticalPercolation.BinaryLaw.density_le_rawProduct line 148
  15. def OAI.CriticalPercolation.BinaryLaw.scheduleWeight line 179
  16. lemma OAI.CriticalPercolation.BinaryLaw.rawProduct_eq_finprod line 185
  17. lemma OAI.CriticalPercolation.BinaryLaw.rawProduct_words line 200