OAI/Analysis/CircleDomains/Sobolev/WeakPartialLocality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Weak partial derivatives are local on an open plane domain. The proof decomposes each compact test into finitely many actual smooth partition products; it does not assume a global Sobolev gluing theorem.

  1. theorem OAI.CircleDomainRigidity.weakPartial_test_on_superset line 14
  2. theorem OAI.CircleDomainRigidity.weakPartial_test_finite_sum line 35
  3. theorem OAI.CircleDomainRigidity.weakPartial_of_local line 64