OAI/Analysis/CircleDomains/Sobolev/PartitionWeakGradient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual global weak gradients from local Sobolev witnesses. Uniqueness on overlaps identifies the partition sum with each local gradient, and finite test decomposition proves the global weak identity.

  1. theorem OAI.CircleDomainRigidity.partition_gradient_eq_local line 16
  2. theorem OAI.CircleDomainRigidity.exists_partition_weak_gradient line 42