OAI/Analysis/CircleDomains/Sobolev/JordanSignedArea.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The absolute signed area of a regular Jordan curve is the actual area of its bounded component. This is a direct specialization of the remaining signed Green input, with no analytic area theorem assumed.

  1. lemma OAI.CircleDomainRigidity.regular_jordan_signed_area line 15
  2. lemma OAI.CircleDomainRigidity.regular_jordan_signed_area_ne_zero line 37