OAI/Combinatorics/RamseyFive/Entropy/TargetAverage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.TreeCodec.mean_pathBudget_twice line 11
2. lemma OAI.SharpRamseyFive.FiniteEntropy.original_target_mean_point line 25
3. lemma OAI.SharpRamseyFive.FiniteEntropy.original_target_mean_dual line 48
4. lemma OAI.SharpRamseyFive.TreeCodec.mean_two_pathBudget_scaled line 78