OAI/Analysis/CircleDomains/Sobolev/ComplexGradientError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A smooth approximation is controlled by the two scalar weak-gradient components and their actual coordinate errors.

  1. theorem OAI.CircleDomainRigidity.complexCovector_norm_le_abs line 12
  2. theorem OAI.CircleDomainRigidity.complex_scalar_gradient_error line 18