OAI/Analysis/C0Absorption/Weights.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.eta line 14
  2. def OAI.C0Absorption.scheduleH line 15
  3. theorem OAI.C0Absorption.eta_pos line 17
  4. theorem OAI.C0Absorption.scheduleH_pos line 18
  5. theorem OAI.C0Absorption.schedule_speed line 19
  6. theorem OAI.C0Absorption.bandL_pos line 24
  7. def OAI.C0Absorption.rho line 30
  8. theorem OAI.C0Absorption.rho_pos line 34
  9. theorem OAI.C0Absorption.rho_step line 41
  10. theorem OAI.C0Absorption.rho_half_step line 45
  11. theorem OAI.C0Absorption.rho_bound line 50
  12. theorem OAI.C0Absorption.rho_lt_one line 58
  13. theorem OAI.C0Absorption.rho_lip_budget line 63
  14. theorem OAI.C0Absorption.rho_tendsto line 70
  15. def OAI.C0Absorption.ell line 75
  16. theorem OAI.C0Absorption.ell_pos line 77
  17. theorem OAI.C0Absorption.ell_tendsto line 78
  18. theorem OAI.C0Absorption.log_rho_step line 82
  19. def OAI.C0Absorption.transitionAngle line 87
  20. theorem OAI.C0Absorption.transitionAngle_nonneg line 90
  21. theorem OAI.C0Absorption.transitionAngle_le line 95
  22. theorem OAI.C0Absorption.transitionAngle_zero line 102
  23. theorem OAI.C0Absorption.transitionAngle_full line 107
  24. theorem OAI.C0Absorption.transitionAngle_dichotomy line 114
  25. def OAI.C0Absorption.transitionInterval line 120
  26. theorem OAI.C0Absorption.log_rho_antitone line 122
  27. theorem OAI.C0Absorption.transitionInterval_disjoint line 127
  28. theorem OAI.C0Absorption.finite_variation_sum_lipschitz line 147
  29. def OAI.C0Absorption.angleSpeed line 181
  30. theorem OAI.C0Absorption.transitionAngle_lipschitz line 183
  31. theorem OAI.C0Absorption.transitionAngle_antitone line 196
  32. theorem OAI.C0Absorption.transitionAngle_locally_constant line 201
  33. theorem OAI.C0Absorption.angle_sum_distance line 216