OAI/Analysis/CircleDomains/Sobolev/FilledScalarSliceDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual line derivatives of the finite filling agree almost everywhere with its ordinary planar partials. Circular boundaries are the only exclusions.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.transferred_contDiffOn line 20
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.horizontal_derivative_ae line 30