OAI/Analysis/CircleDomains/Sobolev/CompactWeakDerivativeIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact Sobolev perturbations contribute zero total first derivative. The support and integrability of the actual weak derivative are proved, so the boundary-flux replacement does not assume an unproved trace fact.

  1. theorem OAI.CircleDomainRigidity.compact_weakGradient_zero_off line 13
  2. theorem OAI.CircleDomainRigidity.compact_weakGradient_integrable line 25
  3. theorem OAI.CircleDomainRigidity.integral_compact_weakGradient_eq_zero line 36