OAI/Geometry/CylinderCovering/Physical/Minimum.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RadialPhysical.PhysicalMinimum.canonicalBody line 13
  2. lemma OAI.RadialPhysical.PhysicalMinimum.centered_similarity line 15
  3. lemma OAI.RadialPhysical.PhysicalMinimum.halfheight_similarity line 40
  4. theorem OAI.RadialPhysical.PhysicalMinimum.minimum_modelBody line 69
  5. theorem OAI.RadialPhysical.PhysicalMinimum.shadow_x_modelBody line 84
  6. theorem OAI.RadialPhysical.PhysicalMinimum.minimum_attained line 114
  7. theorem OAI.RadialPhysical.PhysicalMinimum.nonorthonormal_minimum line 121
  8. theorem OAI.RadialPhysical.PhysicalMinimum.halfheight_reference line 148
  9. theorem OAI.RadialPhysical.PhysicalMinimum.centered_reference line 153
  10. lemma OAI.RadialPhysical.PhysicalMinimum.reference_pos line 159
  11. theorem OAI.RadialPhysical.PhysicalMinimum.shadow_lower line 163
  12. theorem OAI.RadialPhysical.PhysicalMinimum.relativeCost_le line 170
  13. theorem OAI.RadialPhysical.PhysicalMinimum.both_half_bounds line 181
  14. theorem OAI.RadialPhysical.PhysicalMinimum.baseRelativeCost_le line 192
  15. lemma OAI.RadialPhysical.PhysicalMinimum.upperAxis_unit line 204
  16. lemma OAI.RadialPhysical.PhysicalMinimum.lowerAxis_unit line 212
  17. theorem OAI.RadialPhysical.PhysicalMinimum.actual_relativeCost_le line 220
  18. theorem OAI.RadialPhysical.PhysicalMinimum.actual_half_bound line 234
  19. theorem OAI.RadialPhysical.PhysicalMinimum.physical_minimum line 245