OAI/Combinatorics/MatchingCount/Algorithm/OnlineHistorySize.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MatchingFPRAS.OnlineTrial.product_bitsline 14 - def
OAI.MatchingFPRAS.OnlineTrial.sizeNormline 23 - lemma
OAI.MatchingFPRAS.OnlineTrial.sizeNorm_fieldsline 26 - def
OAI.MatchingFPRAS.OnlineTrial.vectorPolynomialline 32 - def
OAI.MatchingFPRAS.OnlineTrial.productPolynomialline 35 - lemma
OAI.MatchingFPRAS.OnlineTrial.vector_weight_boundline 38 - lemma
OAI.MatchingFPRAS.OnlineTrial.product_weight_boundline 55 - def
OAI.MatchingFPRAS.OnlineTrial.statePolynomialline 80 - lemma
OAI.MatchingFPRAS.OnlineTrial.data_weightline 81 - lemma
OAI.MatchingFPRAS.OnlineTrial.stateSize_mkline 87 - lemma
OAI.MatchingFPRAS.OnlineTrial.state_weight_boundline 92