OAI/Analysis/CircleDomains/Modulus/InitialWeightedCollar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Initial collar splicing for the actual smooth weighted collars. The local joining arcs are constructed, rather than assumed.

  1. theorem OAI.CircleDomainRigidity.exists_initial_weighted_collar_path line 21