OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCircleIdentity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The full resolvent contour of the contracting remainder

Outside the norm disk the resolvent contour equals the identity. The proof uses its large-circle limit and the annulus theorem, without assuming a spectral decomposition.

  1. theorem OAI.DefocusingNLS.norm_lt_mem_resolvent line 20
  2. theorem OAI.DefocusingNLS.circleResolventOperator_eq_one line 26