OAI/Analysis/CircleDomains/Modulus/WeightedTwoEndedSplicing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Two-ended splicing for the actual weighted smooth collars. All short joining arcs, path restrictions, and limiting budgets are constructed.

  1. theorem OAI.CircleDomainRigidity.exists_weighted_twoEnded_splicing line 22