OAI/Analysis/CircleDomains/Sobolev/PrincipalWeakDirections.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The strong principal density limit supplies the actual directional weak derivatives of the locally uniform homeomorphism limit.

  1. def OAI.CircleDomainRigidity.principalDirectionalCorrection line 15
  2. lemma OAI.CircleDomainRigidity.principalDirectionalCorrection_ae line 18
  3. lemma OAI.CircleDomainRigidity.principalDirectionalCorrection_tendsto line 26
  4. lemma OAI.CircleDomainRigidity.PrincipalSmoothApproximation.directional_derivative_ae line 35
  5. lemma OAI.CircleDomainRigidity.PrincipalSmoothApproximation.limit_weak_direction line 46