OAI/Probability/SKRatio/Matrices/EntryLM.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.ComplexMatrix.entryLM line 41
2. def OAI.SKRatioGaussian.ComplexMatrix.entryCLM line 46
3. lemma OAI.SKRatioGaussian.ComplexMatrix.integral_entry line 48
4. def OAI.SKRatioGaussian.ComplexMatrix.conjugate line 52
5. def OAI.SKRatioGaussian.ComplexMatrix.conjugateCLM line 55
6. lemma OAI.SKRatioGaussian.ComplexMatrix.conjugate_exp line 58
7. lemma OAI.SKRatioGaussian.ComplexMatrix.conjugate_imaginary line 62
8. lemma OAI.SKRatioGaussian.ComplexMatrix.kernelMatrix_conjugate line 66
9. lemma OAI.SKRatioGaussian.ComplexMatrix.kernelMatrix_diagonal line 79
10. def OAI.SKRatioGaussian.ComplexMatrix.schwartzMatrix line 98
11. lemma OAI.SKRatioGaussian.ComplexMatrix.fourier_scalar_inverse line 101
12. lemma OAI.SKRatioGaussian.ComplexMatrix.schwartzMatrix_diagonal line 115
13. lemma OAI.SKRatioGaussian.ComplexMatrix.schwartzMatrix_conjugate line 125
14. lemma OAI.SKRatioGaussian.ComplexMatrix.schwartzMatrix_spectral line 133