OAI/Analysis/NumericalRange/DensityAdjoints.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompleteCrouzeix.densityField_star line 14
2. lemma OAI.CompleteCrouzeix.hsTrace_mean_coefficient line 23
3. lemma OAI.CompleteCrouzeix.hsTrace_mean_zero_iff line 34
4. lemma OAI.CompleteCrouzeix.densityField_mean_zero line 57
5. lemma OAI.CompleteCrouzeix.densityField_mean_nonzero line 64
6. lemma OAI.CompleteCrouzeix.left_adjoint_of_ae line 75
7. lemma OAI.CompleteCrouzeix.right_adjoint_of_ae line 89