OAI/Combinatorics/RamseyFive/Entropy/WindowLossAggregation.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SharpRamseyFive.FiniteEntropy.retained_filter_lossline 13 - theorem
OAI.SharpRamseyFive.ProjectiveIncidence.original_window_target_failureline 58