OAI/Combinatorics/RamseyFive/Entropy/RevealDomains.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_mono_pos line 16
  2. lemma OAI.SharpRamseyFive.FiniteEntropy.reveal_positive line 24
  3. lemma OAI.SharpRamseyFive.FiniteEntropy.fiber_reveal_support line 31
  4. lemma OAI.SharpRamseyFive.FiniteEntropy.fiber_reveal_agrees line 39
  5. def OAI.SharpRamseyFive.FiniteEntropy.InDomains line 46
  6. lemma OAI.SharpRamseyFive.FiniteEntropy.InDomains.fiber line 49
  7. lemma OAI.SharpRamseyFive.FiniteEntropy.InDomains.entropy_cap line 54
  8. def OAI.SharpRamseyFive.FiniteEntropy.FixedOutside line 63
  9. lemma OAI.SharpRamseyFive.FiniteEntropy.constant_coordinate_entropy line 66
  10. lemma OAI.SharpRamseyFive.FiniteEntropy.FixedOutside.entropy_zero line 80
  11. lemma OAI.SharpRamseyFive.FiniteEntropy.FixedOutside.fiber line 85
  12. lemma OAI.SharpRamseyFive.FiniteEntropy.FixedOutside.entropy_le_sum line 96
  13. def OAI.SharpRamseyFive.FiniteEntropy.activeDeficit line 106
  14. def OAI.SharpRamseyFive.FiniteEntropy.marginalDeficit line 109
  15. lemma OAI.SharpRamseyFive.FiniteEntropy.marginalDeficit_le_active line 112
  16. lemma OAI.SharpRamseyFive.FiniteEntropy.activeDeficit_reveal line 118
  17. def OAI.SharpRamseyFive.FiniteEntropy.blockActive line 140
  18. lemma OAI.SharpRamseyFive.FiniteEntropy.mem_blockActive_left line 144
  19. lemma OAI.SharpRamseyFive.FiniteEntropy.mem_blockActive_right line 147
  20. lemma OAI.SharpRamseyFive.FiniteEntropy.freshBlockLaw_supported line 150
  21. lemma OAI.SharpRamseyFive.FiniteEntropy.representativeSet_subset_active line 158
  22. lemma OAI.SharpRamseyFive.FiniteEntropy.blockActive_erase line 166
  23. def OAI.SharpRamseyFive.FiniteEntropy.blockAllDeficit line 173
  24. theorem OAI.SharpRamseyFive.FiniteEntropy.block_round_deficit line 176
  25. theorem OAI.SharpRamseyFive.FiniteEntropy.exists_actual_pre_round_with_deficit line 214