OAI/Analysis/LipschitzEquivalence/SlowAngles.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.SlowAngles.warp line 15
  2. def OAI.LipschitzCounterexample.SlowAngles.inverseWarp line 16
  3. theorem OAI.LipschitzCounterexample.SlowAngles.warp_pos line 18
  4. theorem OAI.LipschitzCounterexample.SlowAngles.warp_lt_one line 19
  5. theorem OAI.LipschitzCounterexample.SlowAngles.warp_strictAnti line 20
  6. theorem OAI.LipschitzCounterexample.SlowAngles.inverseWarp_warp line 24
  7. theorem OAI.LipschitzCounterexample.SlowAngles.inverseWarp_hasDerivAt line 27
  8. theorem OAI.LipschitzCounterexample.SlowAngles.inverseWarp_le_iff line 38
  9. theorem OAI.LipschitzCounterexample.SlowAngles.le_inverseWarp_iff line 44
  10. theorem OAI.LipschitzCounterexample.SlowAngles.transition_derivative_bound line 50
  11. def OAI.LipschitzCounterexample.SlowAngles.transitionBound line 70
  12. theorem OAI.LipschitzCounterexample.SlowAngles.transitionBound_nonneg line 72
  13. theorem OAI.LipschitzCounterexample.SlowAngles.deriv_transition_le line 74
  14. def OAI.LipschitzCounterexample.SlowAngles.width line 77
  15. theorem OAI.LipschitzCounterexample.SlowAngles.width_pos line 79
  16. def OAI.LipschitzCounterexample.SlowAngles.angleFormula line 85
  17. def OAI.LipschitzCounterexample.SlowAngles.angle line 88
  18. theorem OAI.LipschitzCounterexample.SlowAngles.angle_small line 92
  19. theorem OAI.LipschitzCounterexample.SlowAngles.angle_large line 105
  20. theorem OAI.LipschitzCounterexample.SlowAngles.angle_between line 118
  21. theorem OAI.LipschitzCounterexample.SlowAngles.angleFormula_contDiffAt line 133
  22. theorem OAI.LipschitzCounterexample.SlowAngles.angle_eventually_formula line 139
  23. theorem OAI.LipschitzCounterexample.SlowAngles.angle_eventually_small line 145
  24. theorem OAI.LipschitzCounterexample.SlowAngles.angle_eventually_large line 150
  25. theorem OAI.LipschitzCounterexample.SlowAngles.angle_contDiff line 155
  26. theorem OAI.LipschitzCounterexample.SlowAngles.angleFormula_hasDerivAt line 170
  27. theorem OAI.LipschitzCounterexample.SlowAngles.warp_below_cutoff line 178
  28. theorem OAI.LipschitzCounterexample.SlowAngles.width_budget line 191
  29. theorem OAI.LipschitzCounterexample.SlowAngles.angle_deriv_bound line 199
  30. theorem OAI.LipschitzCounterexample.SlowAngles.warp_tendsto line 236
  31. theorem OAI.LipschitzCounterexample.SlowAngles.warp_denominator_tendsto line 242
  32. theorem OAI.LipschitzCounterexample.SlowAngles.exists_parameter line 247
  33. def OAI.LipschitzCounterexample.SlowAngles.chooseParameter line 262
  34. theorem OAI.LipschitzCounterexample.SlowAngles.chooseParameter_spec line 265
  35. def OAI.LipschitzCounterexample.SlowAngles.parameters line 271
  36. theorem OAI.LipschitzCounterexample.SlowAngles.parameters_ge_three line 276
  37. theorem OAI.LipschitzCounterexample.SlowAngles.parameters_step line 282
  38. theorem OAI.LipschitzCounterexample.SlowAngles.parameters_scale line 286
  39. theorem OAI.LipschitzCounterexample.SlowAngles.parameters_budget line 292
  40. def OAI.LipschitzCounterexample.SlowAngles.lower line 298
  41. def OAI.LipschitzCounterexample.SlowAngles.upper line 300
  42. def OAI.LipschitzCounterexample.SlowAngles.theta line 302
  43. theorem OAI.LipschitzCounterexample.SlowAngles.lower_pos line 305
  44. theorem OAI.LipschitzCounterexample.SlowAngles.lower_lt_upper line 307
  45. theorem OAI.LipschitzCounterexample.SlowAngles.upper_lt_cutoff line 312
  46. theorem OAI.LipschitzCounterexample.SlowAngles.interval_separation line 315
  47. theorem OAI.LipschitzCounterexample.SlowAngles.stage_budget line 320
  48. theorem OAI.LipschitzCounterexample.SlowAngles.theta_contDiff line 325
  49. theorem OAI.LipschitzCounterexample.SlowAngles.theta_deriv_bound line 328
  50. theorem OAI.LipschitzCounterexample.SlowAngles.theta_small_eventually line 332
  51. theorem OAI.LipschitzCounterexample.SlowAngles.theta_large_eventually line 337
  52. theorem OAI.LipschitzCounterexample.SlowAngles.pulledAngle_contDiff line 354
  53. theorem OAI.LipschitzCounterexample.SlowAngles.pulledAngle_deriv_bound line 364