OAI/Analysis/CircleDomains/Sobolev/ThreeL2WeakLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A common weakly convergent subsequence for one scalar and its two differential components, allowing the scalar measure to be spherical.

  1. theorem OAI.CircleDomainRigidity.exists_three_L2_weak_limits line 12