OAI/Analysis/Crouzeix/PhysicalModule.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Physical Module.

  1. lemma OAI.CrouzeixHilbert.Boundary.realCLM_eq_of_matrixLaurent line 19
  2. lemma OAI.CrouzeixHilbert.Boundary.lpLeft_boundaryField line 31
  3. lemma OAI.CrouzeixHilbert.Boundary.lpRight_boundaryField line 41
  4. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.analyticTrace line 59
  5. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCauchy_polynomialTrace line 64
  6. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCauchy_analyticTrace line 83
  7. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.matrixAnalyticTrace line 112
  8. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCauchy_matrixAnalyticTrace line 117
  9. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalRepresentative line 137
  10. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalRepresentative_holomorphic line 140
  11. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalRepresentative_trace line 145
  12. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCauchy_left_module line 152
  13. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCauchy_right_module line 182