OAI/Combinatorics/TriangleRemoval/Stability/GridCavityError.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpTerminalLeave.messageIntegral_time_lipschitz line 23
  2. theorem OAI.SharpTerminalLeave.cavityLimit_time_lipschitz line 42
  3. theorem OAI.SharpTerminalLeave.cavity_integrand_time_lipschitz line 66
  4. theorem OAI.SharpTerminalLeave.sum_fin_filter_lt_eq_range line 83
  5. theorem OAI.SharpTerminalLeave.gridMessage_exact_range line 104
  6. theorem OAI.SharpTerminalLeave.uniform_subaverage_mem_unit line 118
  7. theorem OAI.SharpTerminalLeave.gridMessage_mem_unit line 137
  8. def OAI.SharpTerminalLeave.gridCavityError line 141
  9. theorem OAI.SharpTerminalLeave.gridCavityError_nonneg line 145
  10. theorem OAI.SharpTerminalLeave.gridCavityError_coord line 148
  11. theorem OAI.SharpTerminalLeave.grid_integrand_error line 154
  12. theorem OAI.SharpTerminalLeave.grid_message_integral_error line 171
  13. theorem OAI.SharpTerminalLeave.gridCavityError_volterra line 212
  14. theorem OAI.SharpTerminalLeave.gridCavityError_bound line 267
  15. theorem OAI.SharpTerminalLeave.gridMessage_tendsto_terminal line 277