OAI/Probability/CriticalPercolation/Entropy/BinaryDescriptor.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CriticalPercolation.BinaryLaw.FixedDescriptor line 16
  2. lemma OAI.CriticalPercolation.BinaryLaw.fixedDescriptor_card line 18
  3. def OAI.CriticalPercolation.BinaryLaw.descriptor line 21
  4. lemma OAI.CriticalPercolation.BinaryLaw.descriptor_sides line 25
  5. lemma OAI.CriticalPercolation.BinaryLaw.sum_history_words line 31
  6. def OAI.CriticalPercolation.BinaryLaw.jointMass line 41
  7. lemma OAI.CriticalPercolation.BinaryLaw.jointMass_nonneg line 45
  8. lemma OAI.CriticalPercolation.BinaryLaw.jointMass_normalized line 51
  9. def OAI.CriticalPercolation.BinaryLaw.descriptorMass line 76
  10. lemma OAI.CriticalPercolation.BinaryLaw.descriptorMass_sum line 80
  11. theorem OAI.CriticalPercolation.BinaryLaw.exists_descriptor line 84
  12. def OAI.CriticalPercolation.BinaryLaw.fixedMass line 99
  13. lemma OAI.CriticalPercolation.BinaryLaw.fixedMass_sum line 104
  14. def OAI.CriticalPercolation.BinaryLaw.conditionedMass line 130
  15. lemma OAI.CriticalPercolation.BinaryLaw.conditionedMass_normalized line 134
  16. lemma OAI.CriticalPercolation.BinaryLaw.conditionedMass_nonneg line 139
  17. lemma OAI.CriticalPercolation.BinaryLaw.conditionedMass_support line 150