OAI/Analysis/NumericalRange/BoundaryCalculus.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CompleteCrouzeix.AdmissibleDomain.kernel line 15
2. lemma OAI.CompleteCrouzeix.AdmissibleDomain.outside_imp line 18
3. lemma OAI.CompleteCrouzeix.AdmissibleDomain.inner_maps line 20
4. def OAI.CompleteCrouzeix.AdmissibleDomain.cauchy line 24
5. def OAI.CompleteCrouzeix.AdmissibleDomain.trace line 25
6. lemma OAI.CompleteCrouzeix.AdmissibleDomain.fourier_cauchy line 29
7. def OAI.CompleteCrouzeix.AdmissibleDomain.resolventField line 68
8. lemma OAI.CompleteCrouzeix.AdmissibleDomain.curve_continuous line 71
9. lemma OAI.CompleteCrouzeix.AdmissibleDomain.normal_continuous line 74
10. lemma OAI.CompleteCrouzeix.AdmissibleDomain.resolvent_continuous line 78
11. lemma OAI.CompleteCrouzeix.AdmissibleDomain.fourier_resolvent_eval line 82
12. lemma OAI.CompleteCrouzeix.AdmissibleDomain.positive_representation line 97