OAI/Analysis/PeriodicLattice/Scales.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Temporal scales, smooth profile parameters and derivative budgets.

  1. def OAI.PeriodicLattice.Scales.width line 16
  2. def OAI.PeriodicLattice.Scales.codeExponent line 18
  3. def OAI.PeriodicLattice.Scales.capacity line 20
  4. def OAI.PeriodicLattice.Scales.exponent line 22
  5. def OAI.PeriodicLattice.Scales.epsilon line 25
  6. def OAI.PeriodicLattice.Scales.beta line 27
  7. theorem OAI.PeriodicLattice.Scales.width_succ line 31
  8. theorem OAI.PeriodicLattice.Scales.codeExponent_zero line 35
  9. theorem OAI.PeriodicLattice.Scales.codeExponent_eq line 39
  10. theorem OAI.PeriodicLattice.Scales.codeExponent_succ line 44
  11. theorem OAI.PeriodicLattice.Scales.exponent_zero line 49
  12. theorem OAI.PeriodicLattice.Scales.exponent_pos line 52
  13. theorem OAI.PeriodicLattice.Scales.exponent_succ line 56
  14. theorem OAI.PeriodicLattice.Scales.growthFactor_ge_four line 63
  15. theorem OAI.PeriodicLattice.Scales.four_mul_exponent_le line 68
  16. theorem OAI.PeriodicLattice.Scales.exponent_strictMono line 73
  17. theorem OAI.PeriodicLattice.Scales.exponent_ge_nextCode line 80
  18. theorem OAI.PeriodicLattice.Scales.codeExponent_le_exponent line 91
  19. theorem OAI.PeriodicLattice.Scales.exponent_gap line 96
  20. theorem OAI.PeriodicLattice.Scales.capacity_dvd_inverseScale line 106
  21. theorem OAI.PeriodicLattice.Scales.capacity_dvd_scaleRatio line 110
  22. theorem OAI.PeriodicLattice.Scales.index_le_exponent line 114
  23. theorem OAI.PeriodicLattice.Scales.exponent_ge_thirteen line 122
  24. theorem OAI.PeriodicLattice.Scales.epsilon_pos line 127
  25. theorem OAI.PeriodicLattice.Scales.epsilon_le_one line 132
  26. theorem OAI.PeriodicLattice.Scales.epsilon_antitone line 137
  27. theorem OAI.PeriodicLattice.Scales.plateau_power_bound line 147
  28. theorem OAI.PeriodicLattice.Scales.epsilon_le_small line 173
  29. theorem OAI.PeriodicLattice.Scales.epsilon_cube_lt_quarter line 185
  30. theorem OAI.PeriodicLattice.Scales.plateau_bound line 193
  31. theorem OAI.PeriodicLattice.Scales.epsilon_le_geometric line 203
  32. theorem OAI.PeriodicLattice.Scales.beta_zero line 214
  33. theorem OAI.PeriodicLattice.Scales.beta_succ line 216
  34. theorem OAI.PeriodicLattice.Scales.beta_pos line 219
  35. theorem OAI.PeriodicLattice.Scales.beta_strictAnti line 225
  36. theorem OAI.PeriodicLattice.Scales.beta_le_quarter line 236
  37. theorem OAI.PeriodicLattice.Scales.growthFactor_ge_index line 239
  38. theorem OAI.PeriodicLattice.Scales.differentiated_record_bound line 248
  39. def OAI.PeriodicLattice.Scales.slotSize line 262
  40. theorem OAI.PeriodicLattice.Scales.slotSize_le line 266
  41. def OAI.PeriodicLattice.Scales.weightBound line 278
  42. theorem OAI.PeriodicLattice.Scales.polynomial_geometric_bound line 280
  43. theorem OAI.PeriodicLattice.Scales.weighted_slotSize_bound line 315