OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCircleProjection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Nested resolvent circles

The product identity is obtained from the resolvent identity and two scalar Cauchy integrals. It supplies idempotence once nearby resolvent circles are identified by the annulus theorem.

  1. theorem OAI.DefocusingNLS.circleIntegral_inverse_left_outside line 18
  2. theorem OAI.DefocusingNLS.finiteDimensional_range_of_compact_projection line 39
  3. theorem OAI.DefocusingNLS.resolvent_continuousOn_circle line 55
  4. theorem OAI.DefocusingNLS.circleResolventOperator_mul_nested line 62
  5. theorem OAI.DefocusingNLS.circleResolventOperator_idempotent_of_annulus line 158
  6. theorem OAI.DefocusingNLS.exists_resolvent_annulus line 173

    Source documentation

    A compact spectrum disjoint from a circle is disjoint from a slightly larger closed annulus as well.

    theorem exists_resolvent_annulus (T : E →L[ℂ] E) {r : ℝ}
    (hres : ∀ z : ℂ, ‖z‖ = r → z ∈ resolventSet ℂ T) :
    ∃ R : ℝ, r < R ∧
      ∀ z : ℂ, r ≤ ‖z‖ → ‖z‖ ≤ R → z ∈ resolventSet ℂ T := by
…
  7. theorem OAI.DefocusingNLS.circleResolventOperator_idempotent line 191