OAI/Combinatorics/TriangleRemoval/Process/PowerEulerError.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpTerminalLeave.power_euler_error line 14
2. lemma OAI.SharpTerminalLeave.densityEdgeSafe_rate_error line 34
3. theorem OAI.SharpTerminalLeave.densityEdgeSafe_copy_euler_error line 67
4. lemma OAI.SharpTerminalLeave.relative_power_drift_bound line 114
5. lemma OAI.SharpTerminalLeave.history_relative_drift_sum line 140
6. theorem OAI.SharpTerminalLeave.early_relative_drift_bound line 165