OAI/Geometry/RCD/Transport/LocalFeatureSpace.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The vector space generated by local squared-distance coordinates

  1. theorem OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.zero_in_image line 15
  2. def OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.localFeatureSpace line 21
  3. structure OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.FeatureRepresentation line 25
  4. theorem OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.exists_featureRepresentation line 33
  5. def OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.featureRepresentation line 40
  6. def OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.featureTestPoint line 44
  7. theorem OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.representation_eval line 47
  8. def OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.localInner line 55
  9. theorem OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.localInner_symm line 60
  10. theorem OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.localInner_self line 70