OAI/Analysis/Crouzeix/BoundaryMoments.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Boundary Moments.

  1. lemma OAI.CrouzeixHilbert.tensorOperator_smul_exchange line 18
  2. lemma OAI.CrouzeixHilbert.matrixHolomorphicEval_scalar line 30
  3. lemma OAI.CrouzeixHilbert.Boundary.circleCoordinate_zpow line 48
  4. lemma OAI.CrouzeixHilbert.Boundary.boundaryStar_matrixLaurentMonomial line 56
  5. lemma OAI.CrouzeixHilbert.Boundary.tensorOperator_matrixLaurentMonomial line 64
  6. lemma OAI.CrouzeixHilbert.Boundary.integral_tensor_star line 74
  7. lemma OAI.CrouzeixHilbert.Boundary.tensorIntegral_add_left line 87
  8. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.matrixResolvent line 102
  9. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.matrixResolvent_operator line 106
  10. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.matrixResolventDensity line 111
  11. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.matrixResolventDensity_posSemidef line 114
  12. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.matrixHolomorphicEval_physicalRepresentative line 129
  13. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.tensorIntegral_matrixResolvent_moment line 142
  14. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.tensorIntegral_matrixResolventDensity line 161
  15. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.tensorIntegral_matrixDensity_trace line 177
  16. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physical_channel_intertwines line 186
  17. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physical_laurent_tests line 200