OAI/Analysis/CircleDomains/Modulus/ModelPairBarrier.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual compact target barrier is built from two continued model coordinates. Its gradient vanishes almost everywhere on every model hole.

  1. def OAI.CircleDomainRigidity.CompactScalarModel.pairBarrier line 16
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.pairBarrier_continuous line 21
  3. theorem OAI.CircleDomainRigidity.CompactScalarModel.pairBarrier_pullback line 27
  4. theorem OAI.CircleDomainRigidity.CompactScalarModel.pairBarrier_witness line 41