OAI/Geometry/RCD/Coordinates/QuadraticMetricError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative squared-distance errors for variational test recovery

  1. theorem OAI.RegularPointCoordinates.sq_error_of_abs_sub_le line 11
  2. theorem OAI.RegularPointCoordinates.pointed_square_distance_error line 21
  3. theorem OAI.RegularPointCoordinates.scaled_quadratic_cost line 29