OAI/MathematicalPhysics/NavierStokes/Material/Scales.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Alternating.Memory.width line 9
  2. def OAI.Alternating.Memory.scale line 11
  3. def OAI.Alternating.Memory.epsilon line 13
  4. theorem OAI.Alternating.Memory.scale_succ line 15
  5. theorem OAI.Alternating.Memory.exponent_linear_lower line 22
  6. theorem OAI.Alternating.Memory.scale_above_block line 29
  7. theorem OAI.Alternating.Memory.scale_pos line 34
  8. theorem OAI.Alternating.Memory.ratio_lower line 38
  9. theorem OAI.Alternating.Memory.twice_scale_le_succ line 44
  10. theorem OAI.Alternating.Memory.scale_strictMono line 48
  11. theorem OAI.Alternating.Memory.scale_succ_gap line 55
  12. theorem OAI.Alternating.Memory.old_block_gap line 61
  13. theorem OAI.Alternating.Memory.index_le_scale line 65
  14. theorem OAI.Alternating.Memory.derivative_budget line 70
  15. theorem OAI.Alternating.Memory.epsilon_pos line 84
  16. theorem OAI.Alternating.Memory.epsilon_nonneg line 88
  17. theorem OAI.Alternating.Memory.epsilon_succ_le line 91
  18. theorem OAI.Alternating.Memory.epsilon_succ_half line 99
  19. theorem OAI.Alternating.Memory.epsilon_strictAnti line 108
  20. theorem OAI.Alternating.Memory.epsilon_sum_range line 116
  21. theorem OAI.Alternating.Memory.epsilon_sum_range_le line 125
  22. theorem OAI.Alternating.Memory.epsilon_summable line 131
  23. theorem OAI.Alternating.Memory.epsilon_tsum_le line 136
  24. theorem OAI.Alternating.Memory.initial_epsilon_small line 140
  25. theorem OAI.Alternating.Memory.epsilon_tsum_small line 156
  26. theorem OAI.Alternating.Memory.derivative_cost_absorbed line 160
  27. theorem OAI.Alternating.Memory.epsilon_le_geometric line 174
  28. theorem OAI.Alternating.Memory.weighted_geometric_summable line 185
  29. theorem OAI.Alternating.Memory.weighted_epsilon_summable line 201
  30. theorem OAI.Alternating.Memory.weighted_epsilon_bounded line 208
  31. def OAI.Alternating.Memory.slotMajorant line 221
  32. theorem OAI.Alternating.Memory.slotMajorant_nonneg line 225
  33. theorem OAI.Alternating.Memory.slotMajorant_tail line 231
  34. theorem OAI.Alternating.Memory.weighted_slotMajorant_bounded line 237