OAI/Geometry/CylinderCovering/Angular/Sampling.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AngularSampling.secant_left line 8
  2. lemma OAI.AngularSampling.secant_right line 11
  3. lemma OAI.AngularSampling.sampled_compatibility line 14
  4. lemma OAI.AngularSampling.sampled_outer_left line 18
  5. lemma OAI.AngularSampling.sampled_outer_right line 19
  6. lemma OAI.AngularSampling.cubic_secant_left line 21
  7. lemma OAI.AngularSampling.cubic_secant_right line 24
  8. lemma OAI.AngularSampling.cubic_balance line 27
  9. lemma OAI.AngularSampling.cubic_coarse_bound line 33
  10. lemma OAI.AngularSampling.cubic_error_bound line 40
  11. lemma OAI.AngularSampling.cubic_coefficient_bound line 49
  12. lemma OAI.AngularSampling.cubic_final_bound line 60
  13. lemma OAI.AngularSampling.abs_product_three_le_two line 70
  14. lemma OAI.AngularSampling.abs_product_four_le_two line 82
  15. lemma OAI.AngularSampling.cubic_sampling_error line 92
  16. lemma OAI.AngularSampling.cubic_difference_bound line 104
  17. lemma OAI.AngularSampling.cubic_initial_estimate line 120
  18. lemma OAI.AngularSampling.cubic_refined_term line 138
  19. theorem OAI.AngularSampling.noradial_failure line 162