OAI/Analysis/CircleDomains/Sobolev/CirclePartitionGradient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The derivative of every local branch of the smoothed circle map. The integer transition derivatives vanish and the partition derivatives sum to zero, leaving one global scalar derivative expression.

  1. theorem OAI.CircleDomainRigidity.OpenPlanePartition.adjustedCircleMix_contDiffAt line 20
  2. theorem OAI.CircleDomainRigidity.OpenPlanePartition.adjustedCircleMix_derivative line 44
  3. theorem OAI.CircleDomainRigidity.OpenPlanePartition.circleMix_derivative line 138