OAI/Combinatorics/RamseyFive/Entropy/EventMass.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.FiniteEntropy.eventMass line 10
  2. lemma OAI.SharpRamseyFive.FiniteEntropy.eventMass_nonneg line 12
  3. lemma OAI.SharpRamseyFive.FiniteEntropy.eventMass_le_one line 15
  4. lemma OAI.SharpRamseyFive.FiniteEntropy.rejection_mass line 19
  5. def OAI.SharpRamseyFive.FiniteEntropy.iid line 32
  6. lemma OAI.SharpRamseyFive.FiniteEntropy.iid_cons line 40
  7. def OAI.SharpRamseyFive.FiniteEntropy.firstAccepted line 44
  8. lemma OAI.SharpRamseyFive.FiniteEntropy.firstAccepted_cons line 49
  9. lemma OAI.SharpRamseyFive.FiniteEntropy.sum_iid_succ line 53
  10. lemma OAI.SharpRamseyFive.FiniteEntropy.first_integrand line 64
  11. lemma OAI.SharpRamseyFive.FiniteEntropy.first_law_succ line 75
  12. lemma OAI.SharpRamseyFive.FiniteEntropy.first_law_zero_none line 95
  13. lemma OAI.SharpRamseyFive.FiniteEntropy.first_law_zero_some line 99
  14. lemma OAI.SharpRamseyFive.FiniteEntropy.first_law_none line 103
  15. lemma OAI.SharpRamseyFive.FiniteEntropy.first_law_some line 112
  16. lemma OAI.SharpRamseyFive.FiniteEntropy.acceptance_geom_sum line 128
  17. theorem OAI.SharpRamseyFive.FiniteEntropy.first_success_law line 136
  18. theorem OAI.SharpRamseyFive.FiniteEntropy.first_success_density line 153