OAI/Analysis/CircleDomains/Topology/PrincipalCircleRemainder.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Derivatives of the actual analytic remainder on large circles. The bounds will make its contribution to signed area tend to zero.

  1. def OAI.CircleDomainRigidity.principalCircleRemainder line 13
  2. theorem OAI.CircleDomainRigidity.principalCircleRemainder_hasDerivAt line 16
  3. theorem OAI.CircleDomainRigidity.principalCircleRemainder_deriv_bound line 40