OAI/Analysis/CircleDomains/Selection/ExteriorDecay.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A uniform principal remainder estimate

The same coefficient-area input gives decay at infinity, uniformly in the finite model. This is stronger than a uniform bounded remainder and preserves the zero constant term when passing to a limit.

  1. theorem OAI.CircleDomainRigidity.norm_exterior_series_le_two_inv line 20
  2. theorem OAI.CircleDomainRigidity.ExteriorCoefficientAreaTheorem.exterior_decay line 40
  3. theorem OAI.CircleDomainRigidity.ExteriorCoefficientAreaTheorem.scaled_exterior_decay line 50