OAI/Analysis/CircleDomains/Sobolev/PrincipalSmoothApproximation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smooth principal maps whose actual densities converge strongly to a specified compact-coefficient L2 solution. The common coefficient support will give uniform exterior estimates for the maps.

  1. lemma OAI.CircleDomainRigidity.density_operator_equation line 15
  2. structure OAI.CircleDomainRigidity.PrincipalSmoothApproximation line 27
  3. lemma OAI.CircleDomainRigidity.exists_principal_smooth_approximation_with_coefficient line 43
  4. lemma OAI.CircleDomainRigidity.exists_principal_smooth_approximation line 84