OAI/Analysis/CircleDomains/Modulus/LocalPlateauPayment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A local quotient plateau, with zero value on the source anchor, pays for the fixed positive transverse width near a protrusion. The inner contour is selected inside Lean.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.local_plateau_norm_bound line 21