OAI/Analysis/CircleDomains/Rigidity/ConductivityFlux.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual weak conductivity height has the principal boundary flux. The interior correction is constructed, its derivative integral vanishes, and the smooth Green calculation retains the exact exterior values.

  1. theorem OAI.CircleDomainRigidity.holomorphic_physical_im_smooth line 16
  2. theorem OAI.CircleDomainRigidity.PlaneLocalWeakComplex.vertical_flux_boundary line 30
  3. theorem OAI.CircleDomainRigidity.PlaneLocalWeakComplex.vertical_flux_limit line 59