OAI/Analysis/MatrixSigning/Matrices/JordanCLM.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Hermitian.jordanCLM line 20
2. lemma OAI.CurrentKS.Hermitian.jordanCLM_val line 23
3. lemma OAI.CurrentKS.Hermitian.jordanCLM_symmetric line 30
4. lemma OAI.CurrentKS.Hermitian.jordanCLM_quadratic line 36
5. lemma OAI.CurrentKS.Hermitian.sandwich_mono line 50
6. lemma OAI.CurrentKS.Hermitian.inner_mono_right line 55
7. lemma OAI.CurrentKS.Hermitian.inner_mono_left line 61
8. lemma OAI.CurrentKS.Hermitian.trace_square_norm line 65
9. lemma OAI.CurrentKS.Hermitian.jordanCLM_lower line 69
10. lemma OAI.CurrentKS.Hermitian.jordanCLM_upper line 81