OAI/Analysis/StructuralCrouzeix/Main.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic domains, optimal similarities and matrix-valued boundary representations.

  1. lemma OAI.StructuralCrouzeix.IsAdmissible.compact_closure line 18
  2. lemma OAI.StructuralCrouzeix.IsAdmissible.sided_boundary line 22
  3. theorem OAI.StructuralCrouzeix.IsAdmissible.coordinates line 28
  4. def OAI.StructuralCrouzeix.bundleDomain line 38
  5. lemma OAI.StructuralCrouzeix.bundleDomain_boundaryPoint line 50
  6. lemma OAI.StructuralCrouzeix.bundleDomain_maximum line 55
  7. theorem OAI.StructuralCrouzeix.fullEndpoint line 60