OAI/Geometry/IsometricImmersion/Caps/CapReflectionGeometry.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Flow.Reflection.reflectionMatrix line 16
  2. def OAI.SmoothLocal.Flow.Reflection.reflectPoint line 18
  3. theorem OAI.SmoothLocal.Flow.Reflection.reflectPoint_zero line 20
  4. theorem OAI.SmoothLocal.Flow.Reflection.reflectPoint_one line 23
  5. theorem OAI.SmoothLocal.Flow.Reflection.reflectPoint_twice line 26
  6. theorem OAI.SmoothLocal.Flow.Reflection.reflectPoint_eq_affine line 30
  7. theorem OAI.SmoothLocal.Flow.Reflection.reflectionMatrix_square line 36
  8. theorem OAI.SmoothLocal.Flow.Reflection.reflectionMatrix_det line 41
  9. theorem OAI.SmoothLocal.Flow.Reflection.reflectionMatrix_isUnit line 44
  10. theorem OAI.SmoothLocal.Flow.Reflection.reflectionMatrix_inv line 50
  11. theorem OAI.SmoothLocal.Flow.Reflection.reflectPoint_contDiff line 53
  12. def OAI.SmoothLocal.Flow.Reflection.reflectionIsometry line 57
  13. def OAI.SmoothLocal.Flow.Reflection.reflectedScalar line 76
  14. def OAI.SmoothLocal.Flow.Reflection.reflectedMetric line 78
  15. theorem OAI.SmoothLocal.Flow.Reflection.reflectedScalar_contDiffOn line 81
  16. theorem OAI.SmoothLocal.Flow.Reflection.reflectedDomain_isOpen line 87
  17. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_smoothPositive line 90
  18. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_add line 97
  19. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_entry line 101
  20. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_det line 109
  21. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_curvature line 114
  22. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_hessian line 121
  23. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_hessian_entry line 130
  24. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_hessian_det line 140
  25. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_energy line 148
  26. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_quotient line 158
  27. theorem OAI.SmoothLocal.Flow.Reflection.reflectPoint_mem_symmetricSquare line 166
  28. theorem OAI.SmoothLocal.Flow.Reflection.reflectPoint_mem_modelSquare line 172
  29. theorem OAI.SmoothLocal.Flow.Reflection.reflectedDomain_contains_modelSquare line 175
  30. theorem OAI.SmoothLocal.Flow.Reflection.modelCurvature_reflect line 180
  31. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_model line 185
  32. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_eq_pushforward line 193
  33. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_tsupport line 199
  34. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_support_patch line 204
  35. theorem OAI.SmoothLocal.Flow.Reflection.reflectedScalar_jet_norm line 210
  36. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_entry_jet_norm line 217
  37. theorem OAI.SmoothLocal.Flow.Reflection.reflectedScalar_C8 line 233
  38. theorem OAI.SmoothLocal.Flow.Reflection.reflectedMetric_C8 line 240