OAI/Analysis/CircleDomains/Modulus/NormedAffineLinePayment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Unit affine lines in a real normed space pay through the actual Fréchet derivative. This includes both coordinate directions in a rectangle.

  1. theorem OAI.CircleDomainRigidity.normed_affine_line_increment line 12
  2. theorem OAI.CircleDomainRigidity.smooth_horizontal_increment line 25
  3. theorem OAI.CircleDomainRigidity.smooth_vertical_increment line 35