OAI/Analysis/CircleDomains/Sobolev/ComplexWeakGradient.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The complex chart preserves covector norms, including differences, and identifies the gradients used by the physical Sobolev witnesses.

  1. theorem OAI.CircleDomainRigidity.complex_plane_covector_norm line 14
  2. theorem OAI.CircleDomainRigidity.complexLocalScalarWitness_gradient line 24
  3. theorem OAI.CircleDomainRigidity.complex_weak_gradient_ae line 34
  4. theorem OAI.CircleDomainRigidity.complex_weak_gradient_difference_norm line 57
  5. theorem OAI.CircleDomainRigidity.complex_weak_gradient_difference_L2 line 71