OAI/Analysis/CircleDomains/Rigidity/ConductivityJacobianBoundary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The weak conductivity Jacobian has the signed area of the actual image circle. The two interior replacements are constructed; locality removes their compact errors before applying the smooth Green identity.

  1. theorem OAI.CircleDomainRigidity.holomorphic_physical_re_smooth line 15
  2. theorem OAI.CircleDomainRigidity.PlaneLocalWeakComplex.jacobian_boundary line 29