OAI/Analysis/CircleDomains/Rigidity/ExactTraceSobolevError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact-trace smoothing has a global Sobolev difference. Thus changing a test to its smooth representative preserves its original boundary trace and changes its global gradient by an arbitrarily small amount.

  1. theorem OAI.CircleDomainRigidity.zeroTraceWitness_component_eLpNorm line 15
  2. theorem OAI.CircleDomainRigidity.exists_exact_trace_smoothing_global_error line 34