OAI/Geometry/RCD/Harmonic/DirectionalToGramError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recovering all Gram entries from directional L1 errors

  1. theorem OAI.RegularPointCoordinates.directional_error_implies_gram line 14