OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cutoff.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.Cutoff.joinAt line 12
  2. theorem OAI.VelocityDetection.Cutoff.hasDerivAt_joinAt line 15
  3. theorem OAI.VelocityDetection.Cutoff.continuous_joinAt line 47
  4. def OAI.VelocityDetection.Cutoff.polynomial line 54
  5. def OAI.VelocityDetection.Cutoff.polynomialD line 56
  6. def OAI.VelocityDetection.Cutoff.polynomialDD line 58
  7. theorem OAI.VelocityDetection.Cutoff.hasDerivAt_polynomial line 60
  8. theorem OAI.VelocityDetection.Cutoff.hasDerivAt_polynomialD line 67
  9. def OAI.VelocityDetection.Cutoff.step line 74
  10. def OAI.VelocityDetection.Cutoff.stepD line 76
  11. def OAI.VelocityDetection.Cutoff.stepDD line 78
  12. theorem OAI.VelocityDetection.Cutoff.hasDerivAt_step line 80
  13. theorem OAI.VelocityDetection.Cutoff.hasDerivAt_stepD line 85
  14. theorem OAI.VelocityDetection.Cutoff.deriv_step line 90
  15. theorem OAI.VelocityDetection.Cutoff.deriv_stepD line 92
  16. theorem OAI.VelocityDetection.Cutoff.continuous_stepDD line 94
  17. theorem OAI.VelocityDetection.Cutoff.contDiff_step line 99
  18. theorem OAI.VelocityDetection.Cutoff.step_of_nonpos line 108
  19. theorem OAI.VelocityDetection.Cutoff.step_of_one_le line 111
  20. theorem OAI.VelocityDetection.Cutoff.stepD_of_nonpos line 120
  21. theorem OAI.VelocityDetection.Cutoff.stepD_of_one_le line 123
  22. theorem OAI.VelocityDetection.Cutoff.stepDD_of_nonpos line 132
  23. theorem OAI.VelocityDetection.Cutoff.stepDD_of_one_le line 135
  24. theorem OAI.VelocityDetection.Cutoff.stepD_nonneg line 144
  25. theorem OAI.VelocityDetection.Cutoff.monotone_step line 155
  26. theorem OAI.VelocityDetection.Cutoff.step_mem_Icc line 159
  27. theorem OAI.VelocityDetection.Cutoff.polynomialDD_bound line 168
  28. theorem OAI.VelocityDetection.Cutoff.stepDD_bound line 184
  29. def OAI.VelocityDetection.Cutoff.profile line 191
  30. def OAI.VelocityDetection.Cutoff.profileD line 193
  31. def OAI.VelocityDetection.Cutoff.profileDD line 197
  32. theorem OAI.VelocityDetection.Cutoff.left_deriv line 202
  33. theorem OAI.VelocityDetection.Cutoff.right_deriv line 205
  34. theorem OAI.VelocityDetection.Cutoff.hasDerivAt_profile line 208
  35. theorem OAI.VelocityDetection.Cutoff.hasDerivAt_profileD line 215
  36. theorem OAI.VelocityDetection.Cutoff.deriv_profile line 224
  37. theorem OAI.VelocityDetection.Cutoff.deriv_profileD line 227
  38. theorem OAI.VelocityDetection.Cutoff.contDiff_profile line 230
  39. theorem OAI.VelocityDetection.Cutoff.profile_mem_Icc line 233
  40. theorem OAI.VelocityDetection.Cutoff.profile_one line 241
  41. theorem OAI.VelocityDetection.Cutoff.profile_zero line 245
  42. theorem OAI.VelocityDetection.Cutoff.profileDD_bound line 252
  43. def OAI.VelocityDetection.Cutoff.cutoff line 265
  44. theorem OAI.VelocityDetection.Cutoff.contDiff_cutoff line 267
  45. theorem OAI.VelocityDetection.Cutoff.cutoff_mem_Icc line 270
  46. theorem OAI.VelocityDetection.Cutoff.cutoff_one line 278
  47. theorem OAI.VelocityDetection.Cutoff.cutoff_zero line 285
  48. theorem OAI.VelocityDetection.Cutoff.cutoff_one_on_support line 297
  49. theorem OAI.VelocityDetection.Cutoff.cutoff_le_doubled line 304
  50. theorem OAI.VelocityDetection.Cutoff.hasCompactSupport_cutoff line 312
  51. theorem OAI.VelocityDetection.Cutoff.spatialD_cutoff_zero line 320
  52. theorem OAI.VelocityDetection.Cutoff.spatialD_cutoff_one line 329
  53. theorem OAI.VelocityDetection.Cutoff.spatialD_cutoff_zero_zero line 338
  54. theorem OAI.VelocityDetection.Cutoff.spatialD_cutoff_one_one line 350
  55. theorem OAI.VelocityDetection.Cutoff.laplacian_cutoff line 362
  56. theorem OAI.VelocityDetection.Cutoff.profile_abs_le line 370
  57. theorem OAI.VelocityDetection.Cutoff.laplacian_cutoff_bound line 374
  58. theorem OAI.VelocityDetection.Cutoff.laplacian_cutoff_bound_3000 line 392
  59. theorem OAI.VelocityDetection.Cutoff.continuous_profileD line 397
  60. theorem OAI.VelocityDetection.Cutoff.continuous_profileDD line 400
  61. theorem OAI.VelocityDetection.Cutoff.continuous_laplacian_cutoff line 408
  62. theorem OAI.VelocityDetection.Cutoff.profileD_zero line 416