OAI/Geometry/CylinderCovering/Angular/Endpoint.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AngularEndpoint.node_zero line 9
  2. lemma OAI.AngularEndpoint.node_last line 11
  3. lemma OAI.AngularEndpoint.node_succ line 17
  4. lemma OAI.AngularEndpoint.node_bounds line 21
  5. lemma OAI.AngularEndpoint.boundary_zero line 33
  6. lemma OAI.AngularEndpoint.boundary_last line 35
  7. lemma OAI.AngularEndpoint.boundary_interior line 37
  8. lemma OAI.AngularEndpoint.left_boundary line 48
  9. lemma OAI.AngularEndpoint.right_boundary line 55
  10. lemma OAI.AngularEndpoint.node_in_sector line 62
  11. lemma OAI.AngularEndpoint.sector_width_pos line 74
  12. lemma OAI.AngularEndpoint.sector_distance line 87
  13. lemma OAI.AngularEndpoint.boundary_bounds line 106
  14. lemma OAI.AngularEndpoint.sector_point_bounds line 118
  15. lemma OAI.AngularEndpoint.coefficient_compatibility line 124
  16. lemma OAI.AngularEndpoint.coefficient_outer_left line 132
  17. lemma OAI.AngularEndpoint.coefficient_outer_right line 136
  18. lemma OAI.AngularEndpoint.beta_error line 141
  19. lemma OAI.AngularEndpoint.alpha_error line 151
  20. lemma OAI.AngularEndpoint.profile_nonneg line 167
  21. lemma OAI.AngularEndpoint.profile_lipschitz line 171
  22. lemma OAI.AngularEndpoint.radius_error line 191
  23. lemma OAI.AngularEndpoint.radius_pos line 205
  24. lemma OAI.AngularEndpoint.first_sector_width line 210
  25. lemma OAI.AngularEndpoint.last_sector_width line 216
  26. lemma OAI.AngularEndpoint.interior_sector_width line 221
  27. lemma OAI.AngularEndpoint.sector_width_le line 226
  28. lemma OAI.AngularEndpoint.reciprocal_square line 239
  29. theorem OAI.AngularEndpoint.reciprocal_mesh_errors line 243
  30. lemma OAI.AngularEndpoint.intercept_sampling_error line 264