OAI/Combinatorics/TriangleRemoval/Process/DivergentArms.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpTerminalLeave.factorial_weight_add_leline 19 - lemma
OAI.SharpTerminalLeave.cube_ge_selfline 29 - lemma
OAI.SharpTerminalLeave.cube_ge_sqline 30 - def
OAI.SharpTerminalLeave.DivergentArmsline 34 - lemma
OAI.SharpTerminalLeave.actualPairVisitProbability_le_leftline 42 - lemma
OAI.SharpTerminalLeave.actualPairVisitProbability_le_rightline 51 - theorem
OAI.SharpTerminalLeave.actualPairVisitProbability_pattern_factorialline 60