OAI/Analysis/CircleDomains/Rigidity/PrincipalRealBeltramiProof.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact compactly supported real-coefficient principal Beltrami input, constructed from the L2 conductivity contraction and smooth principal maps. No generalized Beltrami existence theorem is assumed.

  1. lemma OAI.CircleDomainRigidity.principalRealBeltrami line 18