OAI/Analysis/CircleDomains/Selection/LocalizedSmallPerturbation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A local error with small differential gives an actual smooth ambient perturbation, with exact values on the inner disk and compact support.

  1. def OAI.CircleDomainRigidity.localizedPlaneError line 13
  2. lemma OAI.CircleDomainRigidity.localizedPlaneError_eventually_zero line 15
  3. lemma OAI.CircleDomainRigidity.localizedPlaneError_smooth line 20
  4. lemma OAI.CircleDomainRigidity.localizedPlaneError_derivative_bound line 30
  5. lemma OAI.CircleDomainRigidity.exists_localized_smooth_perturbation line 63