OAI/Combinatorics/RamseyFive/Marking/HighSampleRetention.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.HighSamples.SampleConflict line 16
2. theorem OAI.SharpRamseyFive.HighSamples.fixed_target_loss line 19
3. lemma OAI.SharpRamseyFive.HighSamples.mean_second line 44
4. lemma OAI.SharpRamseyFive.HighSamples.mean_sampleConflict line 50
5. theorem OAI.SharpRamseyFive.HighSamples.sampled_target_loss line 55
6. def OAI.SharpRamseyFive.Marking.highLeft line 152
7. def OAI.SharpRamseyFive.Marking.highRight line 154
8. def OAI.SharpRamseyFive.Marking.highRepresentative line 157
9. lemma OAI.SharpRamseyFive.Marking.highLeft_cap line 161
10. lemma OAI.SharpRamseyFive.Marking.highRight_cap line 167
11. lemma OAI.SharpRamseyFive.Marking.high_pair_half line 175
12. theorem OAI.SharpRamseyFive.Marking.highRepresentative_bounds line 182
13. theorem OAI.SharpRamseyFive.Marking.highRepresentative_conflict line 216