OAI/Combinatorics/RamseyFive/Entropy/HighEndpointCutoffs.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.FiniteEntropy.first_entropy_of_partner_cap line 11
  2. theorem OAI.SharpRamseyFive.FiniteEntropy.high_first_upper_tail line 25
  3. def OAI.SharpRamseyFive.FiniteEntropy.highGoodFirst line 39
  4. theorem OAI.SharpRamseyFive.FiniteEntropy.high_bad_first_mass line 42
  5. lemma OAI.SharpRamseyFive.FiniteEntropy.support_first_subset_image line 71
  6. lemma OAI.SharpRamseyFive.FiniteEntropy.support_fiber_card line 77
  7. def OAI.SharpRamseyFive.FiniteEntropy.highBadMass line 87
  8. theorem OAI.SharpRamseyFive.FiniteEntropy.high_endpoint_bad line 90
  9. theorem OAI.SharpRamseyFive.FiniteEntropy.high_endpoint_bad_of_domain line 115
  10. lemma OAI.SharpRamseyFive.FiniteEntropy.support_swap_first_fiber line 130
  11. theorem OAI.SharpRamseyFive.FiniteEntropy.high_endpoint_bad_second line 147
  12. lemma OAI.SharpRamseyFive.FiniteEntropy.support_second_subset_image line 162
  13. lemma OAI.SharpRamseyFive.FiniteEntropy.support_second_fiber_card line 168
  14. theorem OAI.SharpRamseyFive.FiniteEntropy.high_endpoint_bad_second_of_domain line 178
  15. lemma OAI.SharpRamseyFive.FiniteEntropy.high_endpoint_atom line 193
  16. lemma OAI.SharpRamseyFive.FiniteEntropy.high_endpoint_mass line 198