OAI/Analysis/CircleDomains/Selection/PriorityInterpolation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite priority interpolation of a horizontal coordinate. Overlaps of the cutoff supports are allowed; the derivative estimate is uniform in the number of cutoffs.

  1. def OAI.CircleDomainRigidity.priorityBlend line 17
  2. def OAI.CircleDomainRigidity.priorityResidual line 21
  3. theorem OAI.CircleDomainRigidity.priorityBlend_norm_le line 26
  4. theorem OAI.CircleDomainRigidity.priorityResidual_unit line 45
  5. theorem OAI.CircleDomainRigidity.priorityBlend_differentiableAt line 56
  6. theorem OAI.CircleDomainRigidity.priorityBlend_derivative_bound line 66