OAI/Probability/SKRatio/Matrices/MatrixEntryCLM.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatioGaussian.matrix_entry_le_frobenius line 22
2. def OAI.SKRatioGaussian.matrixEntryCLM line 30
3. lemma OAI.SKRatioGaussian.matrixEntry_lipschitz line 36
4. lemma OAI.SKRatioGaussian.matrixEntry_derivative line 43
5. lemma OAI.SKRatioGaussian.matrix_inverse_diff_bound line 48
6. def OAI.SKRatioGaussian.diagonalVector line 58
7. lemma OAI.SKRatioGaussian.diagonalVector_norm_le line 61
8. lemma OAI.SKRatioGaussian.abs_trace_le_frobenius line 70
9. lemma OAI.SKRatioGaussian.matrixTrace_mul_lipschitz line 81