OAI/Analysis/PeriodicLattice/Profiles.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Locally finite smooth profiles and their parameter estimates.

  1. def OAI.PeriodicLattice.Profiles.clock line 19
  2. def OAI.PeriodicLattice.Profiles.bump line 23
  3. theorem OAI.PeriodicLattice.Profiles.clock_contDiff line 28
  4. theorem OAI.PeriodicLattice.Profiles.clock_nonneg line 32
  5. theorem OAI.PeriodicLattice.Profiles.clock_le_one line 34
  6. theorem OAI.PeriodicLattice.Profiles.clock_zero line 36
  7. theorem OAI.PeriodicLattice.Profiles.clock_one line 40
  8. theorem OAI.PeriodicLattice.Profiles.clock_monotone line 44
  9. theorem OAI.PeriodicLattice.Profiles.bump_contDiff line 48
  10. theorem OAI.PeriodicLattice.Profiles.bump_nonneg line 52
  11. theorem OAI.PeriodicLattice.Profiles.bump_le_one line 55
  12. theorem OAI.PeriodicLattice.Profiles.bump_one line 60
  13. theorem OAI.PeriodicLattice.Profiles.bump_zero line 65
  14. theorem OAI.PeriodicLattice.Profiles.bump_support line 70
  15. theorem OAI.PeriodicLattice.Profiles.clock_deriv_eq_zero line 75
  16. theorem OAI.PeriodicLattice.Profiles.clock_deriv_contDiff line 87
  17. theorem OAI.PeriodicLattice.Profiles.lattice_intervals_locallyFinite line 90
  18. def OAI.PeriodicLattice.Profiles.latticeBump line 99
  19. theorem OAI.PeriodicLattice.Profiles.latticeBump_contDiff line 103
  20. theorem OAI.PeriodicLattice.Profiles.latticeBump_locallyFinite line 107
  21. def OAI.PeriodicLattice.Profiles.selector line 118
  22. theorem OAI.PeriodicLattice.Profiles.selector_contDiff line 120
  23. theorem OAI.PeriodicLattice.Profiles.other_bump_zero line 129
  24. theorem OAI.PeriodicLattice.Profiles.selector_plateau line 141
  25. theorem OAI.PeriodicLattice.Profiles.selector_shift line 147
  26. theorem OAI.PeriodicLattice.Profiles.selector_single line 160
  27. theorem OAI.PeriodicLattice.Profiles.selector_eventually_single line 178
  28. theorem OAI.PeriodicLattice.Profiles.latticeBump_iteratedDeriv line 186
  29. theorem OAI.PeriodicLattice.Profiles.selector_iteratedDeriv line 199
  30. theorem OAI.PeriodicLattice.Profiles.selector_derivative_bound line 207
  31. def OAI.PeriodicLattice.Profiles.shiftedClock line 224
  32. def OAI.PeriodicLattice.Profiles.pulse line 226
  33. theorem OAI.PeriodicLattice.Profiles.shiftedClock_contDiff line 228
  34. theorem OAI.PeriodicLattice.Profiles.pulse_contDiff line 231
  35. theorem OAI.PeriodicLattice.Profiles.shiftedClock_hasDerivAt line 234
  36. theorem OAI.PeriodicLattice.Profiles.pulse_eq_zero line 239
  37. theorem OAI.PeriodicLattice.Profiles.pulse_support line 246
  38. theorem OAI.PeriodicLattice.Profiles.time_tails_locallyFinite line 255
  39. theorem OAI.PeriodicLattice.Profiles.shiftedClock_locallyFinite line 264
  40. theorem OAI.PeriodicLattice.Profiles.pulse_locallyFinite line 272
  41. theorem OAI.PeriodicLattice.Profiles.other_pulse_zero line 279
  42. def OAI.PeriodicLattice.Profiles.schedule line 288
  43. theorem OAI.PeriodicLattice.Profiles.schedule_contDiff line 291
  44. theorem OAI.PeriodicLattice.Profiles.schedule_on_slot line 303
  45. theorem OAI.PeriodicLattice.Profiles.schedule_zero_at_start line 310
  46. theorem OAI.PeriodicLattice.Profiles.selector_unit_periodic line 315
  47. theorem OAI.PeriodicLattice.Profiles.schedule_eventually_on_slot line 329
  48. def OAI.PeriodicLattice.Profiles.mixedPartial line 346
  49. theorem OAI.PeriodicLattice.Profiles.schedule_mixedPartial line 350
  50. theorem OAI.PeriodicLattice.Profiles.pulse_iteratedDeriv line 363
  51. theorem OAI.PeriodicLattice.Profiles.compact_iteratedDeriv line 367
  52. theorem OAI.PeriodicLattice.Profiles.bump_hasCompactSupport line 373
  53. theorem OAI.PeriodicLattice.Profiles.clock_deriv_hasCompactSupport line 376
  54. theorem OAI.PeriodicLattice.Profiles.profile_derivative_bounds line 382