OAI/Analysis/CircleDomains/Modulus/SmallModelBarrier.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A saved source barrier produces an actual compact global target barrier, with the same small energy and value one on its image contour.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.exists_small_pair_barrier line 14