OAI/Analysis/CircleDomains/Sobolev/CompactSobolevJacobian.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The integral of the Jacobian of two compact Sobolev scalars is zero. Only one scalar is mollified. Its two differentiated test functions have commuting mixed derivatives, and strong L2 convergence passes the pairing to the original gradients.

  1. theorem OAI.CircleDomainRigidity.tendsto_integral_mul_of_L2 line 18
  2. theorem OAI.CircleDomainRigidity.smooth_partial_commute line 30
  3. theorem OAI.CircleDomainRigidity.integral_compact_sobolev_jacobian_zero line 41