OAI/Analysis/Crouzeix/ResolventMoments.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Resolvent Moments.

  1. lemma OAI.CrouzeixHilbert.contourEval_circleIntegral line 22
  2. lemma OAI.CrouzeixHilbert.ringInverse_neg line 39
  3. lemma OAI.CrouzeixHilbert.contourEval_sub_inv line 46
  4. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryMap_not_mem line 64
  5. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundary_difference_ne_zero line 67
  6. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.operatorResolvent line 70
  7. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.operatorResolvent_add_star_nonneg line 76
  8. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.integral_operatorResolvent_moment line 87