OAI/Analysis/Crouzeix/SimilarityRepresentation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Similarity Representation.

  1. theorem OAI.CrouzeixHilbert.Endpoint.intertwining_inner line 22
  2. theorem OAI.CrouzeixHilbert.Endpoint.intertwining_adjoint_inner line 38
  3. theorem OAI.CrouzeixHilbert.integral_operator_adjoint line 55
  4. def OAI.CrouzeixHilbert.Boundary.boundaryStar line 64
  5. theorem OAI.CrouzeixHilbert.Boundary.boundaryStar_apply line 67
  6. theorem OAI.CrouzeixHilbert.Boundary.boundaryField_star line 70
  7. def OAI.CrouzeixHilbert.Boundary.tensorIntegral line 78
  8. theorem OAI.CrouzeixHilbert.Boundary.tensorIntegral_star line 82
  9. theorem OAI.CrouzeixHilbert.Boundary.real_inner_densityLp_field line 99
  10. theorem OAI.CrouzeixHilbert.Boundary.real_inner_densityLp_star_field line 106
  11. theorem OAI.CrouzeixHilbert.Boundary.lpStar_inner_right line 113
  12. def OAI.CrouzeixHilbert.Boundary.reflectedBoundaryCauchy line 118
  13. theorem OAI.CrouzeixHilbert.Boundary.reflectedBoundaryCauchy_pairing line 123
  14. theorem OAI.CrouzeixHilbert.Boundary.projected_density_of_laurent_testing line 131