OAI/Geometry/RCD/Metric/EuclideanApproximateMinimizer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sharp local radius control for approximate Euclidean Hopf--Lax minimizers

  1. theorem OAI.RegularPointCoordinates.approximate_hopf_minimizer_radius line 12