OAI/Analysis/CircleDomains/Topology/CirclePartitionError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The intrinsic differential of the glued circle coordinate differs from the partition of local weak derivatives by exactly the selected summable approximation errors.

  1. theorem OAI.CircleDomainRigidity.OpenPlanePartition.circleMix_gradient_error_identity line 19
  2. theorem OAI.CircleDomainRigidity.exists_positive_circle_smoothing line 67