OAI/Analysis/CircleDomains/Sobolev/SobolevJacobianLocality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact Sobolev replacements agreeing outside a closed region have the same Jacobian integral over that region. This is the interior replacement step in the conductivity area computation.

  1. theorem OAI.CircleDomainRigidity.weakGradient_eq_on_open line 14
  2. theorem OAI.CircleDomainRigidity.sobolev_jacobian_integral_locality line 25