OAI/MathematicalPhysics/AlternatingFlow/Scales.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AlternatingNS.Scales.K line 10
  2. def OAI.AlternatingNS.Scales.s line 12
  3. def OAI.AlternatingNS.Scales.ε line 14
  4. lemma OAI.AlternatingNS.Scales.exponent_succ line 16
  5. lemma OAI.AlternatingNS.Scales.s_succ line 19
  6. lemma OAI.AlternatingNS.Scales.pow_lower line 23
  7. lemma OAI.AlternatingNS.Scales.s_lower line 31
  8. lemma OAI.AlternatingNS.Scales.capacity_lt line 35
  9. lemma OAI.AlternatingNS.Scales.K_add_one_lt line 40
  10. lemma OAI.AlternatingNS.Scales.s_pos line 44
  11. lemma OAI.AlternatingNS.Scales.strictMono_s line 48
  12. lemma OAI.AlternatingNS.Scales.scale_gap line 55
  13. lemma OAI.AlternatingNS.Scales.old_scale_gap line 62
  14. lemma OAI.AlternatingNS.Scales.derivative_gap line 69
  15. lemma OAI.AlternatingNS.Scales.s_zero_add line 78
  16. lemma OAI.AlternatingNS.Scales.n_le_s line 86
  17. lemma OAI.AlternatingNS.Scales.ε_pos line 90
  18. lemma OAI.AlternatingNS.Scales.ε_nonneg line 94
  19. lemma OAI.AlternatingNS.Scales.ε_strictAnti line 97
  20. lemma OAI.AlternatingNS.Scales.ε_le_geometric line 104
  21. lemma OAI.AlternatingNS.Scales.ε_le_initial_geometric line 114
  22. lemma OAI.AlternatingNS.Scales.summable_ε line 126
  23. lemma OAI.AlternatingNS.Scales.total_memory_le line 131
  24. lemma OAI.AlternatingNS.Scales.initial_memory_small line 142
  25. lemma OAI.AlternatingNS.Scales.derivative_cost_bound line 154
  26. lemma OAI.AlternatingNS.Scales.summable_weighted_ε line 164
  27. lemma OAI.AlternatingNS.Scales.weighted_ε_tendsto_zero line 178
  28. lemma OAI.AlternatingNS.Scales.weighted_ε_bounded line 183