OAI/Probability/SKRatio/Matrices/LinCLM.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.ComplexMatrix.linCLM line 40
2. lemma OAI.SKRatioGaussian.ComplexMatrix.opNorm_kernelMatrix line 43
3. lemma OAI.SKRatioGaussian.ComplexMatrix.schwartzMatrix_opNorm line 61
4. lemma OAI.SKRatioGaussian.ComplexMatrix.schwartzMatrix_eq_inverse line 65
5. lemma OAI.SKRatioGaussian.ComplexMatrix.schwartzMatrix_hermitian line 83