OAI/Probability/SKGap/Matrix/StaticCovarianceMatrix.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.staticCovarianceMatrix line 180
2. lemma OAI.SKGapCutoff.staticCovarianceMatrix_diag line 183
3. lemma OAI.SKGapCutoff.staticCovarianceMatrix_trace line 187
4. lemma OAI.SKGapCutoff.trace_mul_staticCovarianceMatrix line 191
5. def OAI.SKGapCutoff.normalizedStaticCovarianceTrace line 205
6. lemma OAI.SKGapCutoff.normalizedStaticCovarianceTrace_self line 208
7. lemma OAI.SKGapCutoff.normalizedStaticCovarianceTrace_square line 215
8. lemma OAI.SKGapCutoff.normalizedStaticCovarianceTrace_one line 242
9. lemma OAI.SKGapCutoff.normalizedStaticCovarianceTrace_smul line 247
10. lemma OAI.SKGapCutoff.normalizedStaticCovarianceTrace_sub line 251
11. theorem OAI.SKGapCutoff.staticCovariance_P1_limit line 256
12. theorem OAI.SKGapCutoff.staticCovariance_P2_limit line 272