OAI/Analysis/CircleDomains/Modulus/UngatedBarrier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Choosing both gate target sets to be the whole sphere forces the perturbation region to be empty. Thus the controlled norm is the global norm required for the ungated barrier selection.

  1. theorem OAI.CircleDomainRigidity.CompatibleRealBarrier.penalty_eq_empty_of_univ line 24
  2. theorem OAI.CircleDomainRigidity.CompatibleRealBarrier.controlledSize_of_univ line 31