Commit 2025-04-22 13:17 3e8a6659

feat(Geometry/Euclidean/Basic): make orthogonalProjection a continuous affine map (#23715) Change EuclideanGeometry.orthogonalProjection from a bundled AffineMap to a bundled ContinuousAffineMap (I think I'll end up wanting continuity for some things related to incenter). Note 1: I think the new import is reasonable in the context for anything much doing Euclidean geometry / using orthogonal projections, but we'll see from CI how many imports it adds. Note 2: this now means the previous orthogonalProjection is a private definition orthogonalProjectionAux, in order for the continuity proof using AffineMap.continuous_linear_iff to work. Is there a better way to refer directly to a structure projection to a parent within the where definition without having such an extra definition of the parent structure? I couldn't get it to work without the extra definition. Note 3: the actual motivation is to make signedDist a bundled continuous affine map. I've left that change to be done separately (a) to avoid conflicts with #23646 and (b) because I think it will need a few other definitions elsewhere in mathlib to be set up (not everything in the definition of signedDist has analogues for ContinuousAffineMap at present). Note 4: I think it would be a good idea to refactor orthogonal projections further so there is only one definition, orthogonalProjection set up directly as a composition of continuous affine maps (move to vector space via an arbitrary choice of base point, apply the orthogonal projection there, move back to affine space), without needing either orthogonalProjectionFn or orthogonalProjectionAux (and then orthogonalProjectionFn would be deprecated with a view to removal). But that composition also requires a few new definitions not currently in mathlib (including but not limited to ContinuousAffineEquiv.vaddConst from #22583). Since we've had orthogonalProjectionFn for a long time, I don't think that cleanup is particularly urgent.