OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothBump.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.SmoothBump.profile line 12

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:713 (same declaration text).

  2. theorem OAI.VelocityDetection.SmoothBump.contDiff_profile line 14
  3. theorem OAI.VelocityDetection.SmoothBump.profile_bounds line 16
  4. theorem OAI.VelocityDetection.SmoothBump.profile_zero line 23
  5. theorem OAI.VelocityDetection.SmoothBump.profile_center line 29
  6. theorem OAI.VelocityDetection.SmoothBump.compactSupport_profile line 33
  7. theorem OAI.VelocityDetection.SmoothBump.exists_second_bound line 39
  8. def OAI.VelocityDetection.SmoothBump.bound line 48
  9. theorem OAI.VelocityDetection.SmoothBump.bound_pos line 50
  10. theorem OAI.VelocityDetection.SmoothBump.second_bound line 52
  11. def OAI.VelocityDetection.SmoothBump.packet line 55
  12. theorem OAI.VelocityDetection.SmoothBump.contDiff_packet line 57
  13. theorem OAI.VelocityDetection.SmoothBump.packet_bounds line 61
  14. theorem OAI.VelocityDetection.SmoothBump.packet_center line 65
  15. theorem OAI.VelocityDetection.SmoothBump.packet_zero line 67
  16. theorem OAI.VelocityDetection.SmoothBump.compactSupport_packet line 77
  17. theorem OAI.VelocityDetection.SmoothBump.spatialD_zero line 84
  18. theorem OAI.VelocityDetection.SmoothBump.spatialD_one line 92
  19. theorem OAI.VelocityDetection.SmoothBump.spatialD_zero_zero line 100
  20. theorem OAI.VelocityDetection.SmoothBump.spatialD_one_one line 113
  21. theorem OAI.VelocityDetection.SmoothBump.laplacian_packet line 126
  22. theorem OAI.VelocityDetection.SmoothBump.laplacian_bound line 133
  23. theorem OAI.VelocityDetection.SmoothBump.eventually_packet_zero line 145
  24. theorem OAI.VelocityDetection.SmoothBump.transport line 152