OAI/Combinatorics/RamseyFive/Entropy/ConditionPullback.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.FiniteEntropy.eventPreimage line 14
2. lemma OAI.SharpRamseyFive.FiniteEntropy.mem_eventPreimage line 18
3. lemma OAI.SharpRamseyFive.FiniteEntropy.eventMass_map_preimage line 22
4. lemma OAI.SharpRamseyFive.FiniteEntropy.conditionOn_mean_exact line 28
5. lemma OAI.SharpRamseyFive.FiniteEntropy.map_condition_pullback line 37
6. lemma OAI.SharpRamseyFive.FiniteEntropy.conditionContext_eq_pullback line 50
7. lemma OAI.SharpRamseyFive.FiniteEntropy.withMessage_pair line 65
8. lemma OAI.SharpRamseyFive.FiniteEntropy.conditionContext_pair line 74
9. lemma OAI.SharpRamseyFive.FiniteEntropy.selected_pair line 89