OAI/Analysis/CircleDomains/Rigidity/SmoothReplacementFlux.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The genuine compact Sobolev correction has zero derivative integral. Consequently a smooth exterior replacement preserves the finite-ball vertical flux of the original weak coordinate.

  1. theorem OAI.CircleDomainRigidity.integral_weakGradient_eq_smooth_replacement line 14