OAI/Analysis/CircleDomains/Sobolev/ComplexLocalSobolevTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Package actual complex weak directional fields as the physical local Sobolev witness required by the principal-map construction.

  1. lemma OAI.CircleDomainRigidity.complex_memLp_physical_ball line 14
  2. def OAI.CircleDomainRigidity.localWeakComplexOfDirectionalFields line 22
  3. lemma OAI.CircleDomainRigidity.planarDz_of_complex_directions line 38
  4. lemma OAI.CircleDomainRigidity.planarDbar_of_complex_directions line 42