OAI/Geometry/RCD/Harmonic/QuadraticDistanceFeature.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Linear features from quadratic squared distances

Polarization about a fixed point embeds the space into real functions. The exact squared-distance law makes every geodesic affine in these functions. No inner-product or Euclidean structure is presumed.

  1. def OAI.RegularPointCoordinates.quadraticDistanceFeature line 17
  2. theorem OAI.RegularPointCoordinates.quadraticDistanceFeature_self line 20
  3. theorem OAI.RegularPointCoordinates.quadraticDistanceFeature_diag line 24
  4. theorem OAI.RegularPointCoordinates.quadraticDistanceFeature_symm line 29
  5. theorem OAI.RegularPointCoordinates.quadraticDistanceFeature_injective line 35
  6. theorem OAI.RegularPointCoordinates.QuadraticGeodesicGeometry.feature_path line 48
  7. theorem OAI.RegularPointCoordinates.QuadraticGeodesicGeometry.feature_radial line 59