OAI/Analysis/CircleDomains/Sobolev/SmoothCurveImage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A smooth scalar image is paid by the integral of the differential against curve length. This bound is proved directly by local Lipschitz covers and therefore needs no additional published input.

  1. theorem OAI.CircleDomainRigidity.smooth_curve_image_add_error line 15
  2. theorem OAI.CircleDomainRigidity.smooth_curve_image_bound line 54