OAI/Analysis/CircleDomains/Sobolev/PrincipalSmoothLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Construct the principal plane homeomorphism with the specified strong L2 density. Retain the actual smooth approximants and both convergences for the subsequent scalar transport application.

  1. structure OAI.CircleDomainRigidity.PrincipalMapLimit line 17
  2. lemma OAI.CircleDomainRigidity.PrincipalSmoothApproximation.exists_principal_limit_data line 34
  3. lemma OAI.CircleDomainRigidity.PrincipalSmoothApproximation.exists_principal_homeomorph_limit line 53