OAI/Combinatorics/SharpRamsey/Learning/ReadyTests.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- structure
OAI.SharpLogRamsey.ReadyTests.Callline 16 - def
OAI.SharpLogRamsey.ReadyTests.Call.lossline 35 - lemma
OAI.SharpLogRamsey.ReadyTests.kernel_eq_uniformline 47 - lemma
OAI.SharpLogRamsey.ReadyTests.Call.loss_boundline 52 - def
OAI.SharpLogRamsey.ReadyTests.lossline 67 - lemma
OAI.SharpLogRamsey.ReadyTests.loss_boundline 72