OAI/Analysis/CircleDomains/Modulus/LevelBarrierLocalizedNorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The constructed compatible real barrier controls the localized norm used by the open map exclusion. Enlarging the omitted penalty set only decreases its Dirichlet payment.

  1. theorem OAI.CircleDomainRigidity.CompatibleLevelBarrier.controlledSize_ne_top line 25
  2. theorem OAI.CircleDomainRigidity.CompatibleLevelBarrier.localized_norm_le_controlledSize line 29
  3. theorem OAI.CircleDomainRigidity.CompatibleLevelBarrier.real_band_norm_le line 55