OAI/Analysis/MatrixSigning/Potential/Normalizer.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.normalizer line 14
2. def OAI.CurrentKS.normalizedMatrix line 16
3. lemma OAI.CurrentKS.normalizer_nonneg line 19
4. lemma OAI.CurrentKS.normalizer_pos line 22
5. lemma OAI.CurrentKS.normalizedMatrix_posSemidef line 29
6. lemma OAI.CurrentKS.normalizedMatrix_rank line 37
7. lemma OAI.CurrentKS.normalized_trace_sum line 48
8. lemma OAI.CurrentKS.reconstruct_matrix line 53
9. lemma OAI.CurrentKS.normalized_square line 62
10. lemma OAI.CurrentKS.normalized_variance line 70
11. lemma OAI.CurrentKS.reconstruct_signed_sum line 75
12. lemma OAI.CurrentKS.normalizedMatrix_eq_zero_iff line 85