OAI/Analysis/CircleDomains/Sobolev/ComplexCovectorEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The complex-chart differential norm is exactly the two-coordinate Euclidean energy used by the finite transfer.

  1. theorem OAI.CircleDomainRigidity.complexCovector_norm_sq line 18
  2. theorem OAI.CircleDomainRigidity.circleFDeriv_complex_norm_sq line 51
  3. theorem OAI.CircleDomainRigidity.integral_circleFDeriv_complex_norm_sq line 62
  4. theorem OAI.CircleDomainRigidity.memLp_circleFDeriv_complex line 77