OAI/MathematicalPhysics/NavierStokes/VelocityDetection/BurstSchedule.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.BurstSchedule.amplitude line 13
  2. def OAI.VelocityDetection.BurstSchedule.phase line 15
  3. theorem OAI.VelocityDetection.BurstSchedule.contDiff_amplitude line 17
  4. theorem OAI.VelocityDetection.BurstSchedule.contDiff_phase line 22
  5. theorem OAI.VelocityDetection.BurstSchedule.amplitude_bounds line 27
  6. theorem OAI.VelocityDetection.BurstSchedule.phase_bounds line 33
  7. theorem OAI.VelocityDetection.BurstSchedule.amplitude_before line 40
  8. theorem OAI.VelocityDetection.BurstSchedule.amplitude_after line 44
  9. theorem OAI.VelocityDetection.BurstSchedule.amplitude_middle line 48
  10. theorem OAI.VelocityDetection.BurstSchedule.phase_before line 52
  11. theorem OAI.VelocityDetection.BurstSchedule.phase_after line 56
  12. theorem OAI.VelocityDetection.BurstSchedule.phase_middle line 60
  13. theorem OAI.VelocityDetection.BurstSchedule.deriv_amplitude line 64
  14. theorem OAI.VelocityDetection.BurstSchedule.deriv_phase line 72
  15. theorem OAI.VelocityDetection.BurstSchedule.deriv_amplitude_before line 82
  16. theorem OAI.VelocityDetection.BurstSchedule.deriv_amplitude_after line 86
  17. theorem OAI.VelocityDetection.BurstSchedule.deriv_amplitude_middle line 90
  18. theorem OAI.VelocityDetection.BurstSchedule.deriv_phase_before line 95
  19. theorem OAI.VelocityDetection.BurstSchedule.deriv_phase_after line 99
  20. theorem OAI.VelocityDetection.BurstSchedule.source_at_zero line 103
  21. theorem OAI.VelocityDetection.BurstSchedule.barrier_slope line 110
  22. def OAI.VelocityDetection.BurstSchedule.error line 118
  23. theorem OAI.VelocityDetection.BurstSchedule.error_pos line 120
  24. theorem OAI.VelocityDetection.BurstSchedule.error_small line 122
  25. theorem OAI.VelocityDetection.BurstSchedule.error_sum line 126
  26. theorem OAI.VelocityDetection.BurstSchedule.error_sum_le line 131
  27. def OAI.VelocityDetection.BurstSchedule.lapBound line 146
  28. def OAI.VelocityDetection.BurstSchedule.duration line 148
  29. theorem OAI.VelocityDetection.BurstSchedule.lapBound_pos line 150
  30. theorem OAI.VelocityDetection.BurstSchedule.duration_pos line 155
  31. theorem OAI.VelocityDetection.BurstSchedule.duration_small line 159
  32. theorem OAI.VelocityDetection.BurstSchedule.duration_error line 165
  33. def OAI.VelocityDetection.BurstSchedule.localTime line 173
  34. def OAI.VelocityDetection.BurstSchedule.weight line 175
  35. def OAI.VelocityDetection.BurstSchedule.clock line 177
  36. theorem OAI.VelocityDetection.BurstSchedule.contDiff_localTime line 179
  37. theorem OAI.VelocityDetection.BurstSchedule.contDiff_weight line 183
  38. theorem OAI.VelocityDetection.BurstSchedule.contDiff_clock line 186
  39. theorem OAI.VelocityDetection.BurstSchedule.deriv_weight line 189
  40. theorem OAI.VelocityDetection.BurstSchedule.deriv_clock line 196
  41. theorem OAI.VelocityDetection.BurstSchedule.weight_source line 203
  42. def OAI.VelocityDetection.BurstSchedule.barrier line 208
  43. theorem OAI.VelocityDetection.BurstSchedule.contDiff_barrier line 210
  44. theorem OAI.VelocityDetection.BurstSchedule.deriv_barrier line 214
  45. theorem OAI.VelocityDetection.BurstSchedule.barrier_bounds line 221
  46. theorem OAI.VelocityDetection.BurstSchedule.barrier_deriv_nonneg line 225
  47. theorem OAI.VelocityDetection.BurstSchedule.barrier_deriv_large line 230