OAI/Geometry/CylinderCovering/Beams/Algebra.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.BeamAlgebra.radial_cancellation_first line 7
  2. theorem OAI.CylinderCovering.BeamAlgebra.radial_cancellation_second line 12
  3. theorem OAI.CylinderCovering.BeamAlgebra.exact_gap_sum line 17
  4. theorem OAI.CylinderCovering.BeamAlgebra.exact_gap_difference line 23
  5. theorem OAI.CylinderCovering.BeamAlgebra.strict_gain_coefficient line 32
  6. theorem OAI.CylinderCovering.BeamAlgebra.hasDerivAt_velocity_first line 37
  7. theorem OAI.CylinderCovering.BeamAlgebra.hasDerivAt_velocity_second line 43
  8. theorem OAI.CylinderCovering.BeamAlgebra.parameter_bounds line 50
  9. theorem OAI.CylinderCovering.BeamAlgebra.sum_and_excess_bounds line 71
  10. theorem OAI.CylinderCovering.BeamAlgebra.radial_parameter_error line 88
  11. theorem OAI.CylinderCovering.BeamAlgebra.quadratic_parameter_error line 108
  12. theorem OAI.CylinderCovering.BeamAlgebra.radial_factor_nonneg line 142
  13. theorem OAI.CylinderCovering.BeamAlgebra.central_strip_lower line 150
  14. theorem OAI.CylinderCovering.BeamAlgebra.central_strip line 169
  15. theorem OAI.CylinderCovering.BeamAlgebra.narrow_strip line 183
  16. theorem OAI.CylinderCovering.BeamAlgebra.explicit_strip_bound line 203