OAI/Combinatorics/TriangleRemoval/Asymptotics/OneAddLogRpow.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpTerminalLeave.one_add_log_rpow_isLittleO line 16
  2. theorem OAI.SharpTerminalLeave.prefixTemplateFactor_subpower line 40
  3. lemma OAI.SharpTerminalLeave.prefixTargetDensity_eq line 51
  4. lemma OAI.SharpTerminalLeave.prefixTargetDensity_tendsto line 57
  5. lemma OAI.SharpTerminalLeave.prefixTargetTime_eventually_nonneg line 63
  6. theorem OAI.SharpTerminalLeave.prefixDensity_eventual_envelope line 72
  7. lemma OAI.SharpTerminalLeave.prefix_target_D_identity line 89
  8. theorem OAI.SharpTerminalLeave.prefixD_eventual_envelope line 99
  9. lemma OAI.SharpTerminalLeave.prefixDensity_le_one line 113
  10. lemma OAI.SharpTerminalLeave.prefix_scales_eventually_pos line 119
  11. lemma OAI.SharpTerminalLeave.prefix_mixed_power_envelope line 127
  12. theorem OAI.SharpTerminalLeave.prefixTemplateFactor_mixed_gain line 144
  13. theorem OAI.SharpTerminalLeave.prefix_short_suppression line 166
  14. theorem OAI.SharpTerminalLeave.prefix_suffix_scaling line 174
  15. lemma OAI.SharpTerminalLeave.prefixTemplateFactor_le_D_power line 180
  16. theorem OAI.SharpTerminalLeave.prefix_long_suppression line 196