OAI/Analysis/CircleDomains/Sobolev/WeakPairDifferential.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The joint weak chain rule expressed as an actual linear differential. Its norm is exactly the norm of the scalar weak gradient, so the three-term barrier estimate applies to the constructed Sobolev witness.

  1. def OAI.CircleDomainRigidity.weakPairDifferential line 15
  2. theorem OAI.CircleDomainRigidity.plane_inner_basis line 19
  3. theorem OAI.CircleDomainRigidity.weakPairDifferential_basis line 23
  4. theorem OAI.CircleDomainRigidity.plane_covector_of_basis line 28
  5. theorem OAI.CircleDomainRigidity.weakPairDifferential_chain line 35
  6. theorem OAI.CircleDomainRigidity.weakPairDifferential_chain_norm_sub line 45
  7. theorem OAI.CircleDomainRigidity.localPairChainWitness_gradient line 54