OAI/Probability/SKRatio/Matrices/SandShift.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.ComplexMatrix.sandShift line 36
2. lemma OAI.SKRatioGaussian.ComplexMatrix.sandShift_hermitian line 39
3. lemma OAI.SKRatioGaussian.ComplexMatrix.sandShift_sub line 43
4. lemma OAI.SKRatioGaussian.ComplexMatrix.sandShift_lipschitz line 46
5. lemma OAI.SKRatioGaussian.ComplexMatrix.sandShift_parameter line 51
6. lemma OAI.SKRatioGaussian.ComplexMatrix.sandShift_four_point line 62
7. lemma OAI.SKRatioGaussian.ComplexMatrix.schwartzMatrix_sandShift_lipschitz line 70
8. lemma OAI.SKRatioGaussian.ComplexMatrix.schwartzMatrix_sandShift_four_point line 79