OAI/Analysis/CircleDomains/Sobolev/LocalSobolevJacobianReplacement.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local Sobolev Jacobians are unchanged by compact interior replacements. A common compact cutoff reduces the assertion to the proved whole-plane null Lagrangian, while its plateau preserves all four original gradients.

  1. theorem OAI.CircleDomainRigidity.local_sobolev_jacobian_integral_locality line 13
  2. theorem OAI.CircleDomainRigidity.volume_restrict_closedBall_eq_ball line 63
  3. theorem OAI.CircleDomainRigidity.local_sobolev_jacobian_ball_replacement line 79