OAI/Analysis/MatrixSigning/Matrices/OperatorNorm.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Hermitian.operatorNorm line 18
2. lemma OAI.CurrentKS.Hermitian.operatorNorm_nonneg line 20
3. lemma OAI.CurrentKS.Hermitian.operatorNorm_eq_matrix line 22
4. lemma OAI.CurrentKS.Hermitian.scalarOne_eq_algebraMap line 24
5. lemma OAI.CurrentKS.Hermitian.operatorNorm_le_of_bounds line 28
6. lemma OAI.CurrentKS.Hermitian.le_operatorNorm_smul_one line 48
7. lemma OAI.CurrentKS.Hermitian.operatorNorm_le_of_psd_le line 54
8. lemma OAI.CurrentKS.Hermitian.operatorNorm_eq_zero_iff line 61
9. lemma OAI.CurrentKS.Hermitian.operatorNorm_smul line 65
10. lemma OAI.CurrentKS.Hermitian.operatorNorm_le_frobenius line 77
11. lemma OAI.CurrentKS.Hermitian.scalar_one_mono_frob line 88
12. lemma OAI.CurrentKS.Hermitian.le_norm_smul_one line 96
13. lemma OAI.CurrentKS.Hermitian.neg_norm_smul_one_le line 99
14. lemma OAI.CurrentKS.Hermitian.ball_order_bounds line 106