OAI/Probability/SKRatio/Matrices/GaussianSupport.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKRatioGaussian.GaussianRegression.law_eq_of_mean_covariance line 17
  2. def OAI.SKRatioGaussian.GaussianRegression.matrixCLM line 52
  3. lemma OAI.SKRatioGaussian.GaussianRegression.matrixCLM_apply line 55
  4. theorem OAI.SKRatioGaussian.GaussianRegression.residual_independent line 58
  5. lemma OAI.SKRatioGaussian.coordinate_hasLaw line 89
  6. lemma OAI.SKRatioGaussian.coordinates_gaussian line 94
  7. lemma OAI.SKRatioGaussian.coordinate_covariance line 99
  8. lemma OAI.SKRatioGaussian.linear_gaussian_mean line 111
  9. lemma OAI.SKRatioGaussian.linear_gaussian_covariance line 116
  10. lemma OAI.SKRatioGaussian.matrix_sample_gaussian line 125
  11. lemma OAI.SKRatioGaussian.matrix_sample_covariance line 129
  12. def OAI.SKRatioGaussian.goeEntryCoeff line 146
  13. lemma OAI.SKRatioGaussian.goeEntryCoeff_sample line 150
  14. lemma OAI.SKRatioGaussian.goe_matrix_gaussian line 156
  15. lemma OAI.SKRatioGaussian.goe_mean_zero line 162
  16. lemma OAI.SKRatioGaussian.goe_entry_cov line 166
  17. def OAI.SKRatioGaussian.goeDisorder line 202
  18. lemma OAI.SKRatioGaussian.goeDisorder_gaussian line 205
  19. lemma OAI.SKRatioGaussian.goeDisorder_mean line 209
  20. lemma OAI.SKRatioGaussian.goeDisorder_cov line 213
  21. lemma OAI.SKRatioGaussian.goeDisorder_hasLaw line 227
  22. lemma OAI.SKRatioGaussian.goe_actual_disorder_hasLaw line 239
  23. lemma OAI.SKRatioGaussian.coupling_goeDisorder line 244
  24. lemma OAI.SKRatioGaussian.goe_row_gaussian line 266
  25. lemma OAI.SKRatioGaussian.goe_row_cov line 274
  26. lemma OAI.SKRatioGaussian.goe_row_hasLaw line 285