OAI/Analysis/CircleDomains/Selection/ScaledExteriorBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exterior bounds at a prescribed physical radius

Scaling a principally normalized exterior map to the unit exterior preserves its normalization. The coefficient-area input then bounds its deviation from the identity outside twice the prescribed radius.

  1. theorem OAI.CircleDomainRigidity.principal_remainder_rescale line 20
  2. theorem OAI.CircleDomainRigidity.ExteriorCoefficientAreaTheorem.scaled_exterior_bound line 33