OAI/Analysis/CircleDomains/Sobolev/PrincipalScalarWeakLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The retained actual smooth principal maps transport the positive mollifications of a continuous compact Sobolev scalar to an actual weak Sobolev limit on the image plane.

  1. def OAI.CircleDomainRigidity.principalScalarApproximation line 21
  2. lemma OAI.CircleDomainRigidity.PrincipalMapLimit.inverse_physical_tendsto line 25
  3. lemma OAI.CircleDomainRigidity.PrincipalMapLimit.scalar_approximation_smooth line 33
  4. lemma OAI.CircleDomainRigidity.PrincipalMapLimit.scalar_approximation_compact line 39
  5. lemma OAI.CircleDomainRigidity.PrincipalMapLimit.scalar_approximation_tendsto line 44
  6. lemma OAI.CircleDomainRigidity.PrincipalMapLimit.scalar_weak_limit line 50