OAI/MathematicalPhysics/RapidForcing/Scales.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RapidForcing.ScaleData.C_pos line 14
  2. lemma OAI.RapidForcing.ScaleData.one_le_C line 18
  3. lemma OAI.RapidForcing.ScaleData.L_zero_le_C line 20
  4. lemma OAI.RapidForcing.ScaleData.slope_le_C line 24
  5. lemma OAI.RapidForcing.ScaleData.L_eq line 28
  6. lemma OAI.RapidForcing.ScaleData.L_le line 32
  7. lemma OAI.RapidForcing.ScaleData.power_square_lower line 37
  8. lemma OAI.RapidForcing.ScaleData.s_lower line 45
  9. lemma OAI.RapidForcing.ScaleData.C_le_s line 50
  10. lemma OAI.RapidForcing.ScaleData.s_pos line 54
  11. lemma OAI.RapidForcing.ScaleData.sixteen_le_s line 56
  12. lemma OAI.RapidForcing.ScaleData.s_mono line 61
  13. lemma OAI.RapidForcing.ScaleData.s_succ line 66
  14. lemma OAI.RapidForcing.ScaleData.s_succ_lower line 72
  15. lemma OAI.RapidForcing.ScaleData.small_motion_exponents line 83
  16. lemma OAI.RapidForcing.ScaleData.old_record_exponents line 92
  17. lemma OAI.RapidForcing.ScaleData.L_le_s line 103
  18. lemma OAI.RapidForcing.ScaleData.memory_exponents line 108
  19. lemma OAI.RapidForcing.ScaleData.capacity_pos line 114
  20. lemma OAI.RapidForcing.ScaleData.D_pos line 117
  21. lemma OAI.RapidForcing.ScaleData.delta_pos line 120
  22. lemma OAI.RapidForcing.ScaleData.delta_nonneg line 124
  23. lemma OAI.RapidForcing.ScaleData.delta_le_one line 126
  24. lemma OAI.RapidForcing.ScaleData.delta_eq_inv_D line 129
  25. lemma OAI.RapidForcing.ScaleData.delta_capacity line 132
  26. lemma OAI.RapidForcing.ScaleData.delta_capacity_le line 142
  27. lemma OAI.RapidForcing.ScaleData.delta_le_sixteen line 149
  28. lemma OAI.RapidForcing.ScaleData.delta_lt_one line 152
  29. lemma OAI.RapidForcing.ScaleData.delta_le_geometric line 157
  30. lemma OAI.RapidForcing.ScaleData.b_pos line 163
  31. lemma OAI.RapidForcing.ScaleData.b_le_delta_pow line 166
  32. lemma OAI.RapidForcing.ScaleData.b_lt_delta_div_eight line 174
  33. lemma OAI.RapidForcing.ScaleData.capacity_dvd_old_weight line 186
  34. lemma OAI.RapidForcing.ScaleData.delta_ratio line 192
  35. lemma OAI.RapidForcing.ScaleData.memory_majorant_eq line 207
  36. lemma OAI.RapidForcing.ScaleData.memory_majorant_summable line 211
  37. lemma OAI.RapidForcing.ScaleData.memory_majorant_sum line 217
  38. lemma OAI.RapidForcing.ScaleData.memory_summable line 225
  39. lemma OAI.RapidForcing.ScaleData.total_memory_le line 231
  40. lemma OAI.RapidForcing.ScaleData.total_memory_lt_one line 236
  41. def OAI.RapidForcing.ScaleData.addressIndex line 240
  42. def OAI.RapidForcing.ScaleData.history line 243
  43. lemma OAI.RapidForcing.ScaleData.history_nonneg line 246
  44. lemma OAI.RapidForcing.ScaleData.history_lt_one line 251
  45. lemma OAI.RapidForcing.ScaleData.history_eq_address line 266
  46. lemma OAI.RapidForcing.ScaleData.address_lt_D line 278
  47. lemma OAI.RapidForcing.ScaleData.address_mod_capacity line 285
  48. theorem OAI.RapidForcing.ScaleData.read_newest_record line 297