OAI/Analysis/CircleDomains/Modulus/LocalizedNormalGreen.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Green's identity for a smooth form supported in one normal chart on the inward-left side of a regular Jordan circuit.

  1. lemma OAI.CircleDomainRigidity.planar_curl_zero_off_support line 14
  2. lemma OAI.CircleDomainRigidity.localized_normal_green_upper line 21