OAI/Combinatorics/TriangleRemoval/Asymptotics/EarlyDensity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpTerminalLeave.earlyDensity line 18
2. lemma OAI.SharpTerminalLeave.earlyDensity_prefix line 21
3. lemma OAI.SharpTerminalLeave.earlyDensity_antitone line 24
4. lemma OAI.SharpTerminalLeave.earlyDensity_succ line 31
5. lemma OAI.SharpTerminalLeave.prefixDensity_eventually_inverse_lower line 37
6. def OAI.SharpTerminalLeave.earlyTemplateScale line 44
7. theorem OAI.SharpTerminalLeave.earlyTemplateScale_regular line 47
8. theorem OAI.SharpTerminalLeave.earlyTemplateScale_log_budget line 91