OAI/Analysis/CircleDomains/Sobolev/ZeroWeakGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A compactly supported planar Sobolev function whose weak gradient vanishes is zero, by positive mollification.

  1. theorem OAI.CircleDomainRigidity.zero_of_compact_support_zero_weak_gradient line 13