OAI/Geometry/CylinderCovering/Beams/Radial.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortenedBeam.beam_inner_coord line 12
  2. lemma OAI.ShortenedBeam.velocity_hasDerivAt line 17
  3. lemma OAI.ShortenedBeam.beam_vectors_independent line 30
  4. def OAI.ShortenedBeam.radialData line 46
  5. lemma OAI.ShortenedBeam.point_inner line 73
  6. lemma OAI.ShortenedBeam.radialData_kappa line 83
  7. lemma OAI.ShortenedBeam.radial_point_eq line 88
  8. lemma OAI.ShortenedBeam.radialData_sweep line 96
  9. def OAI.ShortenedBeam.radialDataPlus line 113
  10. lemma OAI.ShortenedBeam.radialDataPlus_kappa line 148
  11. lemma OAI.ShortenedBeam.radial_point_plus_eq line 153
  12. lemma OAI.ShortenedBeam.radialDataPlus_sweep line 161
  13. lemma OAI.ShortenedBeam.radialDataPlus_weightedArea line 178
  14. lemma OAI.ShortenedBeam.velocity_norm_sq line 185
  15. lemma OAI.ShortenedBeam.radialData_scalarBound line 192
  16. lemma OAI.ShortenedBeam.radialData_radialError line 208
  17. lemma OAI.ShortenedBeam.radialData_collar line 215
  18. lemma OAI.ShortenedBeam.beam_denominator_identity line 221
  19. lemma OAI.ShortenedBeam.radialData_direction line 227
  20. lemma OAI.ShortenedBeam.radialDataPlus_direction line 230
  21. lemma OAI.ShortenedBeam.radialData_weightedArea line 233
  22. lemma OAI.ShortenedBeam.radialData_total_weightedArea line 260
  23. lemma OAI.ShortenedBeam.constant_capMax line 267
  24. lemma OAI.ShortenedBeam.radialData_frozenArea line 289