OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothProfiles.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VelocityDetection.SmoothProfiles.step line 12

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

  2. def OAI.VelocityDetection.SmoothProfiles.pulse line 14
  3. theorem OAI.VelocityDetection.SmoothProfiles.contDiff_pulse line 16
  4. theorem OAI.VelocityDetection.SmoothProfiles.pulse_nonneg line 19
  5. theorem OAI.VelocityDetection.SmoothProfiles.differentiable_step line 22
  6. theorem OAI.VelocityDetection.SmoothProfiles.pulse_zero_of_nonpos line 25
  7. theorem OAI.VelocityDetection.SmoothProfiles.pulse_zero_of_one_le line 34
  8. theorem OAI.VelocityDetection.SmoothProfiles.support_pulse line 43
  9. theorem OAI.VelocityDetection.SmoothProfiles.compactSupport_pulse line 48
  10. theorem OAI.VelocityDetection.SmoothProfiles.integrable_pulse line 52
  11. theorem OAI.VelocityDetection.SmoothProfiles.integral_pulse line 55
  12. def OAI.VelocityDetection.SmoothProfiles.spatialPulse line 63
  13. theorem OAI.VelocityDetection.SmoothProfiles.contDiff_spatialPulse line 66
  14. theorem OAI.VelocityDetection.SmoothProfiles.spatialPulse_nonneg line 71
  15. theorem OAI.VelocityDetection.SmoothProfiles.support_spatialPulse line 74
  16. theorem OAI.VelocityDetection.SmoothProfiles.spatialPulse_support_bound line 90
  17. theorem OAI.VelocityDetection.SmoothProfiles.compactSupport_spatialPulse line 97
  18. theorem OAI.VelocityDetection.SmoothProfiles.integrable_spatialPulse line 101
  19. theorem OAI.VelocityDetection.SmoothProfiles.integral_spatialPulse line 105
  20. def OAI.VelocityDetection.SmoothProfiles.impulse line 114
  21. theorem OAI.VelocityDetection.SmoothProfiles.contDiff_impulse line 116
  22. theorem OAI.VelocityDetection.SmoothProfiles.impulse_nonneg line 121
  23. theorem OAI.VelocityDetection.SmoothProfiles.impulse_support_bound line 124
  24. theorem OAI.VelocityDetection.SmoothProfiles.compactSupport_impulse line 130
  25. theorem OAI.VelocityDetection.SmoothProfiles.integral_impulse line 140
  26. theorem OAI.VelocityDetection.SmoothProfiles.impulse_zero_of_time_nonpos line 144
  27. theorem OAI.VelocityDetection.SmoothProfiles.impulse_zero_of_time_one_le line 149
  28. theorem OAI.VelocityDetection.SmoothProfiles.impulse_derivatives_bounded line 154