OAI/Analysis/CircleDomains/Modulus/CollarConcatenationCost.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual allowed collar concatenation with its complete cost identity. Summable cost and a positive density supply the required physical finiteness.

  1. theorem OAI.CircleDomainRigidity.exists_allowed_collar_of_summable_cost line 21