OAI/Analysis/CircleDomains/Rigidity/ConductivityHeightLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The continuous height limit and its actual weak derivatives, with the original error budget and zero gradient on the conductivity support.

  1. theorem OAI.CircleDomainRigidity.exists_conductivity_height_limit line 13