OAI/Combinatorics/RamseyFive/Entropy/IndependentSampling.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.eventWeight_mean line 14
2. lemma OAI.SharpRamseyFive.FiniteEntropy.eventWeight_le_one line 18
3. lemma OAI.SharpRamseyFive.FiniteEntropy.eventWeight_exists_le line 24
4. lemma OAI.SharpRamseyFive.FiniteEntropy.iid_eval_mean line 40
5. lemma OAI.SharpRamseyFive.FiniteEntropy.iid_eval_event line 44
6. lemma OAI.SharpRamseyFive.FiniteEntropy.iid_exists_event line 49
7. lemma OAI.SharpRamseyFive.FiniteEntropy.iid_nested_exists_event line 54
8. lemma OAI.SharpRamseyFive.FiniteEntropy.eventMass_filter_mean line 64
9. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_congr_pos line 67
10. lemma OAI.SharpRamseyFive.ProjectiveIncidence.variableTreeLaw_mean line 84
11. theorem OAI.SharpRamseyFive.ProjectiveIncidence.variable_table_target_failure line 90