OAI/Geometry/RCD/Harmonic/ProductProjection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full-dimensional product approximations give actual coordinates

The modulus depends only on the dimension and requested error. No ambient Euclidean approximation or residual-factor geometry is assumed.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.product_projection_of_packing line 17