OAI/Analysis/CircleDomains/Sobolev/ArgumentCircleIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The normalized angular form has integral one on a positively traversed round circle. Both the form and its tangent are actual derivatives.

  1. def OAI.CircleDomainRigidity.centeredArgument line 15
  2. lemma OAI.CircleDomainRigidity.smoothCircleOn_centeredArgument line 17
  3. lemma OAI.CircleDomainRigidity.circleFDeriv_centeredArgument line 23
  4. lemma OAI.CircleDomainRigidity.circleFormIntegral_eq_covector line 34
  5. lemma OAI.CircleDomainRigidity.unitCircleParam_hasDerivAt_centered line 44
  6. lemma OAI.CircleDomainRigidity.unitCircleParam_ne_center line 54
  7. lemma OAI.CircleDomainRigidity.centeredArgument_round_integral line 57