OAI/Probability/SKGap/Localization/EntryLM.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.ComplexMatrix.entryLM line 36
2. def OAI.SKGap.ComplexMatrix.entryCLM line 41
3. lemma OAI.SKGap.ComplexMatrix.integral_entry line 43
4. def OAI.SKGap.ComplexMatrix.conjugate line 47
5. def OAI.SKGap.ComplexMatrix.conjugateCLM line 50
6. lemma OAI.SKGap.ComplexMatrix.conjugate_exp line 53
7. lemma OAI.SKGap.ComplexMatrix.conjugate_imaginary line 57
8. lemma OAI.SKGap.ComplexMatrix.kernelMatrix_conjugate line 61
9. lemma OAI.SKGap.ComplexMatrix.kernelMatrix_diagonal line 74
10. def OAI.SKGap.ComplexMatrix.schwartzMatrix line 93
11. lemma OAI.SKGap.ComplexMatrix.fourier_scalar_inverse line 96
12. lemma OAI.SKGap.ComplexMatrix.schwartzMatrix_diagonal line 110
13. lemma OAI.SKGap.ComplexMatrix.schwartzMatrix_conjugate line 120
14. lemma OAI.SKGap.ComplexMatrix.schwartzMatrix_spectral line 128
15. def OAI.SKGap.ComplexMatrix.linCLM line 144
16. lemma OAI.SKGap.ComplexMatrix.opNorm_kernelMatrix line 147
17. lemma OAI.SKGap.ComplexMatrix.schwartzMatrix_opNorm line 164
18. lemma OAI.SKGap.ComplexMatrix.schwartzMatrix_eq_inverse line 168
19. lemma OAI.SKGap.ComplexMatrix.schwartzMatrix_hermitian line 186