OAI/Combinatorics/TriangleRemoval/Tracking/RootedCompletionMax.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.rootedCompletionMax line 16
  2. lemma OAI.SharpTerminalLeave.rootedCompletionMax_ge_one line 20
  3. lemma OAI.SharpTerminalLeave.rootedCompletionMax_bound line 26
  4. lemma OAI.SharpTerminalLeave.rootedCompletionMax_large line 34
  5. lemma OAI.SharpTerminalLeave.rootedCompletionMax_small line 47
  6. theorem OAI.SharpTerminalLeave.rooted_tail_from_survival line 55
  7. def OAI.SharpTerminalLeave.rootedMomentOrder line 80
  8. lemma OAI.SharpTerminalLeave.rooted_moment_edge_cap line 82
  9. lemma OAI.SharpTerminalLeave.rooted_moment_coefficient line 105
  10. lemma OAI.SharpTerminalLeave.historyAlive_past line 138
  11. lemma OAI.SharpTerminalLeave.stopped_state_mean_past line 149
  12. theorem OAI.SharpTerminalLeave.prefix_rooted_killed_tail line 161
  13. lemma OAI.SharpTerminalLeave.rooted_moment_tail_logsquare line 185
  14. theorem OAI.SharpTerminalLeave.polynomial_logsquare_le_prefix_margin line 204
  15. def OAI.SharpTerminalLeave.PrefixRootedUpper line 234
  16. theorem OAI.SharpTerminalLeave.prefix_rooted_upper_failure line 242