OAI/Analysis/CircleDomains/Rigidity/ConductivityEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact global conductivity energy identity follows from the constructed principal solution and the proved boundary limits. No area, flux or energy estimate is an additional input.

  1. theorem OAI.CircleDomainRigidity.PlaneLocalWeakComplex.conductivity_energy_of_principal_expansion line 14
  2. theorem OAI.CircleDomainRigidity.exists_principal_conductivity_energy line 34