OAI/Combinatorics/MatchingCount/Arithmetic/TreeStateNormalize.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.MatchingFPRAS.ExecutableLadder.StateEnvelopeline 11 - def
OAI.MatchingFPRAS.ExecutableLadder.normalizeStateline 13 - def
OAI.MatchingFPRAS.ExecutableLadder.normalizeStateRealizerline 15 - lemma
OAI.MatchingFPRAS.ExecutableLadder.polynomial_normalizeStateline 20 - lemma
OAI.MatchingFPRAS.ExecutableLadder.normalizeState_weightline 29 - lemma
OAI.MatchingFPRAS.ExecutableLadder.normalizeState_repline 40