OAI/Analysis/MatrixSigning/Matrices/NormRetractH.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Hermitian.norm_retractH_le line 26
2. lemma OAI.CurrentKS.Hermitian.norm_subtypeH_le line 29
3. lemma OAI.CurrentKS.Hermitian.norm_psd_of_scalar_bound line 35
4. lemma OAI.CurrentKS.Hermitian.invH_norm_of_scalar_lower line 49
5. lemma OAI.CurrentKS.Hermitian.jetBound_invH_linear line 55
6. lemma OAI.CurrentKS.Hermitian.norm_sandwichCLM_le line 84