OAI/Analysis/CircleDomains/Modulus/ProtrusionBarrierObstruction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A genuine marked-end protrusion forces a positive lower bound for the localized norm of every retained real barrier with the prescribed zero anchor.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.width_le_local_barrier_norm line 21
  2. def OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.barrierThreshold line 42
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.barrierThreshold_pos line 44
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.barrierThreshold_le_norm line 49