OAI/Analysis/CircleDomains/Sobolev/BarrierDifferentialError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Pointwise differential comparison used by the saved barriers. The exceptional set allows unrestricted horizontal displacement, while its energy contribution is charged only on that set.

  1. theorem OAI.CircleDomainRigidity.composition_covector_error line 14
  2. theorem OAI.CircleDomainRigidity.barrier_differential_error line 27