OAI/Analysis/CircleDomains/Rigidity/ConductivityGlobalEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Passage from the exact finite-ball conductivity identity to its whole-plane version. The two geometric inputs remain separately visible: the Jacobian area defect tends to zero, and the vertical flux defect tends to minus pi times the real Laurent coefficient.

  1. theorem OAI.CircleDomainRigidity.PlaneLocalWeakComplex.imag_energy_integrableOn_compact line 16
  2. theorem OAI.CircleDomainRigidity.PlaneLocalWeakComplex.conductivity_global_energy line 24