OAI/Analysis/CircleDomains/Modulus/OuterBarrierMargin.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Strict separation from every trace center on the fixed outer source collar, from the genuine exterior and vertical error estimates.

  1. theorem OAI.CircleDomainRigidity.outer_pair_margin line 13