UniformDistanceTransfer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform measured plane comparison transfers distance estimates from one affine plane to another. A small-norm point on the joint fits anchors the comparison, giving an additive error controlled by the fit scale and the normalized distance from the origin.

theorem OAI.RieszRectifiability.exists_uniform_measured_distance_transfer line 20