OAI/Geometry/CylinderCovering/Angular/Cubic.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AngularCubic.endpoint_left line 7
  2. lemma OAI.AngularCubic.endpoint_right line 10
  3. lemma OAI.AngularCubic.square_le_one line 13
  4. lemma OAI.AngularCubic.product_error line 17
  5. lemma OAI.AngularCubic.mixed_quartic_bound line 24
  6. lemma OAI.AngularCubic.coarse_excess_bound line 38
  7. lemma OAI.AngularCubic.sharpen_excess_bound line 51
  8. lemma OAI.AngularCubic.final_excess_bound line 66
  9. lemma OAI.AngularCubic.abs_mul_le_one line 78
  10. lemma OAI.AngularCubic.three_factor_bound line 83
  11. lemma OAI.AngularCubic.refined_term_bound line 89
  12. lemma OAI.AngularCubic.excess_identity line 111
  13. lemma OAI.AngularCubic.excess_inequality line 124
  14. theorem OAI.AngularCubic.radial_restrictions line 147