OAI/Combinatorics/TriangleRemoval/Queries/ContinuationCollisionRemainderTendsto.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpTerminalLeave.continuation_collision_remainder_tendsto line 17
2. theorem OAI.SharpTerminalLeave.goodPrefix_relative_l2 line 25
3. lemma OAI.SharpTerminalLeave.normalization_sq line 42
4. lemma OAI.SharpTerminalLeave.normalization_pos line 47
5. lemma OAI.SharpTerminalLeave.sharpConstant_pos line 50
6. lemma OAI.SharpTerminalLeave.sharpConstant_sq line 54
7. theorem OAI.SharpTerminalLeave.prefix_terminal_scale_tendsto line 59