OAI/Geometry/CylinderCovering/Barycentric/Metric.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderBarycentricMetric.sqrt_two_sq line 11
  2. theorem OAI.CylinderBarycentricMetric.sqrt_two_pos line 12
  3. theorem OAI.CylinderBarycentricMetric.sqrt_two_ne line 13
  4. theorem OAI.CylinderBarycentricMetric.embedding_sum line 15
  5. theorem OAI.CylinderBarycentricMetric.embedding_norm line 19
  6. def OAI.CylinderBarycentricMetric.embeddingIsometry line 28
  7. theorem OAI.CylinderBarycentricMetric.inverse_embedding line 31
  8. theorem OAI.CylinderBarycentricMetric.embedding_inverse line 37
  9. theorem OAI.CylinderBarycentricMetric.inverse_norm line 44
  10. theorem OAI.CylinderBarycentricMetric.fromPhysical_point line 48
  11. theorem OAI.CylinderBarycentricMetric.fromPhysical_image line 56
  12. theorem OAI.CylinderBarycentricMetric.embedding_inner line 81
  13. theorem OAI.CylinderBarycentricMetric.embedding_projection line 85
  14. theorem OAI.CylinderBarycentricMetric.projection_add line 89
  15. theorem OAI.CylinderBarycentricMetric.projection_smul line 94
  16. theorem OAI.CylinderBarycentricMetric.projection_fromPhysical line 98
  17. theorem OAI.CylinderBarycentricMetric.shadow_image line 104
  18. theorem OAI.CylinderBarycentricMetric.shadowArea_embedding line 114
  19. theorem OAI.CylinderBarycentricMetric.physical_shadow_eq_abs_embedding line 128
  20. theorem OAI.CylinderBarycentricMetric.shadowArea_formula line 163
  21. theorem OAI.CylinderBarycentricMetric.shadowArea_lower_bound line 173
  22. theorem OAI.CylinderBarycentricMetric.shadowArea_isLeast line 178
  23. theorem OAI.CylinderBarycentricMetric.projectionStatement line 190