OAI/Combinatorics/RamseyFive/Entropy/FlagAlphabetLogs.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.Marking.point_card_le_two line 16
2. lemma OAI.SharpRamseyFive.Marking.point_log_card line 31
3. lemma OAI.SharpRamseyFive.Marking.flagPair_log_card line 44
4. lemma OAI.SharpRamseyFive.Marking.incidentFlag_log_card line 61
5. lemma OAI.SharpRamseyFive.SelectedTuple.log_choose_le line 76
6. lemma OAI.SharpRamseyFive.SelectedTuple.SelectedStream.density_pos line 93
7. theorem OAI.SharpRamseyFive.SelectedTuple.SelectedStream.entropy_lower_explicit line 101
8. theorem OAI.SharpRamseyFive.SelectedTuple.SelectedStream.flag_entropy_lower line 117
9. theorem OAI.SharpRamseyFive.SelectedTuple.SelectedStream.flag_entropy_lower_fraction line 130