OAI/Combinatorics/TriangleRemoval/Stability/CavityGenerator.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.cavityGenerator line 24
  2. theorem OAI.SharpTerminalLeave.cavityGenerator_apply line 30
  3. def OAI.SharpTerminalLeave.cavityVelocity line 35
  4. def OAI.SharpTerminalLeave.cavityResidual line 40
  5. theorem OAI.SharpTerminalLeave.cavityMessage_derivative_bound line 43
  6. theorem OAI.SharpTerminalLeave.cavityMessage_bound line 71
  7. theorem OAI.SharpTerminalLeave.cavityResidual_bound line 90
  8. theorem OAI.SharpTerminalLeave.continuousOn_cavityVelocity line 130
  9. theorem OAI.SharpTerminalLeave.continuousOn_cavityLog_vector line 149
  10. theorem OAI.SharpTerminalLeave.continuousOn_cavityResidual line 154
  11. theorem OAI.SharpTerminalLeave.cavityLog_provisional_bound line 160
  12. def OAI.SharpTerminalLeave.cavityIncidentMessages line 197
  13. theorem OAI.SharpTerminalLeave.continuous_cavityIncidentMessages line 200
  14. theorem OAI.SharpTerminalLeave.cavityIncidentMessages_zero line 208
  15. theorem OAI.SharpTerminalLeave.cavityIncidentMessages_norm_iff line 213
  16. theorem OAI.SharpTerminalLeave.cavity_strict_continuation line 227
  17. theorem OAI.SharpTerminalLeave.cavityTime_strictMono line 299
  18. theorem OAI.SharpTerminalLeave.cavity_closed_continuation line 304