OAI/Analysis/CircleDomains/Rigidity/ExteriorMaskReplacement.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Values outside a closed mask can be replaced by a constant on a closed set separated from that mask and the retained core. This supplies honest real branches for absent coordinates without changing any masked differential, any masked cutoff cost, or any retained value.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.exteriorMaskReplacement line 16
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.exteriorMaskReplacement_eventuallyEq line 20
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.exteriorMaskReplacement_smooth line 30
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.exteriorMaskReplacement_gradient line 41
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.exteriorMaskReplacement_memLp line 48
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.exteriorMaskReplacement_cutoff_gradient line 59
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.exteriorMaskReplacement_masked_wedges line 70