OAI/Analysis/C0Absorption/Angles.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.boundedAngle line 14
  2. theorem OAI.C0Absorption.boundedAngle_zero line 17
  3. theorem OAI.C0Absorption.boundedAngle_last line 18
  4. theorem OAI.C0Absorption.boundedAngle_inner line 20
  5. theorem OAI.C0Absorption.boundedAngle_range line 23
  6. theorem OAI.C0Absorption.boundedAngle_dichotomy line 31
  7. def OAI.C0Absorption.thetaLog line 40
  8. theorem OAI.C0Absorption.thetaLog_mul line 43
  9. theorem OAI.C0Absorption.thetaLog_nonneg line 47
  10. theorem OAI.C0Absorption.thetaLog_le_one line 56
  11. theorem OAI.C0Absorption.thetaLog_sq line 61
  12. theorem OAI.C0Absorption.sum_range_differences line 69
  13. theorem OAI.C0Absorption.thetaLog_squares line 75
  14. theorem OAI.C0Absorption.transitionAngle_unique line 80
  15. theorem OAI.C0Absorption.thetaLog_sum_formula line 93
  16. theorem OAI.C0Absorption.thetaLog_sum_le line 116
  17. theorem OAI.C0Absorption.boundedAngle_difference_sum line 140
  18. theorem OAI.C0Absorption.thetaLog_distance line 160
  19. def OAI.C0Absorption.theta line 186
  20. theorem OAI.C0Absorption.theta_nonneg line 189
  21. theorem OAI.C0Absorption.theta_le_one line 193
  22. theorem OAI.C0Absorption.theta_squares line 197
  23. theorem OAI.C0Absorption.theta_sum_le line 206
  24. theorem OAI.C0Absorption.log_radius_lower line 216
  25. theorem OAI.C0Absorption.boundedAngle_full_of_small line 221
  26. theorem OAI.C0Absorption.theta_terminal line 228
  27. theorem OAI.C0Absorption.boundedAngle_continuous line 244
  28. theorem OAI.C0Absorption.thetaLog_continuous line 251
  29. theorem OAI.C0Absorption.theta_continuous line 254
  30. theorem OAI.C0Absorption.theta_upper_support line 267
  31. theorem OAI.C0Absorption.theta_lower_support line 277
  32. theorem OAI.C0Absorption.min_mul_log_distance line 290
  33. theorem OAI.C0Absorption.theta_weighted_distance line 307