ScalarCollarData.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Construct the scalar angle data from a local calibrated collar and an interior target in the open unit disk. The cutoffs are actual smooth functions.