OAI/Analysis/CircleDomains/Sobolev/WeakPairL2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Two scalar weak-gradient errors control the actual joint linear map, without any extra integrability assumption on that map.

  1. theorem OAI.CircleDomainRigidity.weakPairDifferential_norm_le line 12
  2. theorem OAI.CircleDomainRigidity.weakPairDifferential_sub line 19
  3. theorem OAI.CircleDomainRigidity.continuous_weakPairDifferential line 26
  4. theorem OAI.CircleDomainRigidity.weakPairDifferential_memLp line 33
  5. theorem OAI.CircleDomainRigidity.weakPairDifferential_error_memLp line 49