CircleSmoothingTolerance.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Circle smoothing with a prescribed continuous positive pointwise error. The same choice controls all local derivative errors and preserves interval bounds on each sampling patch.

theorem OAI.CircleDomainRigidity.exists_circle_smoothing_with_tolerance line 16