OAI/Combinatorics/TriangleRemoval/Asymptotics/LogStepSandwich.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpTerminalLeave.log_step_sandwich line 11
2. theorem OAI.SharpTerminalLeave.density_log_sum_bounds line 23
3. lemma OAI.SharpTerminalLeave.inverse_square_grid_step line 36
4. theorem OAI.SharpTerminalLeave.inverse_square_grid_sum line 50
5. theorem OAI.SharpTerminalLeave.density_survival_exponent_bound line 62