OAI/Analysis/CircleDomains/Modulus/RealBarrierSize.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The constructed ungated barrier controls the ordinary gradient-plus-band norm used by the limiting line-payment estimate.

  1. theorem OAI.CircleDomainRigidity.CompatibleRealBarrier.controlledSize_ne_top line 25
  2. theorem OAI.CircleDomainRigidity.CompatibleRealBarrier.ordinary_norm_le_controlledSize line 32