OAI/Analysis/CircleDomains/Modulus/WeightedTwoEndedLevelTolls.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_of_level_toll_zero line 22