OAI/Analysis/CircleDomains/Sobolev/PriorityDerivativeError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The horizontal interpolation differs from the original derivative only by its cutoff-gradient error and the original gradient on the union of cutoff supports.

  1. theorem OAI.CircleDomainRigidity.priorityInfiniteValue_derivative_error line 14