OAI/Analysis/CircleDomains/Selection/PrincipalLeadingBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Size, derivative and smoothness bounds for the leading principal curve. These estimates isolate its contribution from the analytic remainder.

  1. theorem OAI.CircleDomainRigidity.principalLeadingCurve_norm line 12
  2. theorem OAI.CircleDomainRigidity.principalLeadingCurve_deriv_norm line 25
  3. theorem OAI.CircleDomainRigidity.principalLeadingCurve_smooth line 46