OAI/Analysis/CircleDomains/Sobolev/PlaneCovectorEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The two actual coordinate derivatives control the full covector energy on the physical plane. No measurability of the covector field beyond that of the two given derivatives is needed for this bound.

  1. theorem OAI.CircleDomainRigidity.planeCovector_norm_le line 16
  2. theorem OAI.CircleDomainRigidity.lintegral_planeCovector_sq_lt_top line 38