OAI/Combinatorics/TriangleRemoval/Process/RelativeScaleBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpTerminalLeave.relativeScaleBudget line 18
2. theorem OAI.SharpTerminalLeave.history_relative_loss_counter line 21
3. lemma OAI.SharpTerminalLeave.relativeScaleBudget_nonneg line 46
4. lemma OAI.SharpTerminalLeave.relativeScaleBudget_mono line 55
5. theorem OAI.SharpTerminalLeave.relativeCopyCounter_le line 63