OAI/Combinatorics/RamseyFive/Entropy/Hits.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.FiniteEntropy.hits line 12
  2. lemma OAI.SharpRamseyFive.FiniteEntropy.hits_cons line 16
  3. lemma OAI.SharpRamseyFive.FiniteEntropy.expected_hits line 20
  4. lemma OAI.SharpRamseyFive.FiniteEntropy.event_markov line 39
  5. theorem OAI.SharpRamseyFive.FiniteEntropy.iid_test_rejection line 49
  6. lemma OAI.SharpRamseyFive.FiniteEntropy.first_success_atom_le line 63
  7. theorem OAI.SharpRamseyFive.FiniteEntropy.first_success_bad_mass line 82
  8. def OAI.SharpRamseyFive.FiniteEntropy.uniformOn line 97
  9. lemma OAI.SharpRamseyFive.FiniteEntropy.uniformOn_mass line 104
  10. lemma OAI.SharpRamseyFive.FiniteEntropy.iid_uniformOn line 109
  11. lemma OAI.SharpRamseyFive.FiniteEntropy.uniformOn_row_scaling line 119
  12. lemma OAI.SharpRamseyFive.FiniteEntropy.eventMass_scaling line 129
  13. theorem OAI.SharpRamseyFive.FiniteEntropy.first_success_scaled line 134
  14. lemma OAI.SharpRamseyFive.FiniteEntropy.first_success_scaled_bad line 149
  15. theorem OAI.SharpRamseyFive.FiniteEntropy.uniform_proposal_bad line 159