OAI/Probability/SKRatio/Matrices/GOERegression.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatioClock.Regression.standardArrayLaw line 19
  2. instance OAI.SKRatioClock.Regression.(instance at line 22) line 22
  3. lemma OAI.SKRatioClock.Regression.coordinate_hasLaw line 26
  4. lemma OAI.SKRatioClock.Regression.coordinates_independent line 30
  5. lemma OAI.SKRatioClock.Regression.coordinates_gaussian line 34
  6. lemma OAI.SKRatioClock.Regression.coordinate_covariance line 38
  7. def OAI.SKRatioClock.Regression.linearTest line 50
  8. lemma OAI.SKRatioClock.Regression.linearTest_apply line 53
  9. lemma OAI.SKRatioClock.Regression.linearTest_covariance line 56
  10. def OAI.SKRatioClock.Regression.goe line 65
  11. lemma OAI.SKRatioClock.Regression.goe_symmetric line 68
  12. def OAI.SKRatioClock.Regression.goeCLM line 72
  13. lemma OAI.SKRatioClock.Regression.goeCLM_apply line 76
  14. lemma OAI.SKRatioClock.Regression.goe_gaussian line 82
  15. lemma OAI.SKRatioClock.Regression.goe_entry_memLp line 89
  16. lemma OAI.SKRatioClock.Regression.goe_entry_covariance line 93
  17. def OAI.SKRatioClock.Regression.sandwichCLM line 116
  18. lemma OAI.SKRatioClock.Regression.sandwichCLM_apply line 124
  19. def OAI.SKRatioClock.Regression.residualProjection line 128
  20. lemma OAI.SKRatioClock.Regression.residualProjection_symmetric line 131
  21. lemma OAI.SKRatioClock.Regression.residualProjection_mul line 135
  22. lemma OAI.SKRatioClock.Regression.mul_residualProjection line 139
  23. lemma OAI.SKRatioClock.Regression.regression_decomposition line 143
  24. lemma OAI.SKRatioClock.Regression.goe_entry_sandwich_covariance line 152
  25. lemma OAI.SKRatioClock.Regression.goe_sandwich_covariance line 174
  26. lemma OAI.SKRatioClock.Regression.residual_answer_covariance line 208
  27. def OAI.SKRatioClock.Regression.entryCLM line 218
  28. lemma OAI.SKRatioClock.Regression.entryCLM_apply line 223
  29. def OAI.SKRatioClock.Regression.regressionCLM line 226
  30. lemma OAI.SKRatioClock.Regression.regressionCLM_apply line 236
  31. lemma OAI.SKRatioClock.Regression.residual_answer_independent line 246
  32. def OAI.SKRatioClock.Regression.revealedCompletion line 257
  33. lemma OAI.SKRatioClock.Regression.revealedCompletion_answer line 261
  34. lemma OAI.SKRatioClock.Regression.revealedCompletion_symmetric line 269
  35. lemma OAI.SKRatioClock.Regression.revealedCompletion_residual line 278
  36. lemma OAI.SKRatioClock.Regression.revealedCompletion_unique line 289
  37. lemma OAI.SKRatioClock.Regression.regression_factorization line 295
  38. lemma OAI.SKRatioClock.Regression.coordinate_mean line 309
  39. lemma OAI.SKRatioClock.Regression.goe_entry_mean line 313
  40. lemma OAI.SKRatioClock.Regression.sandwich_entry_mean line 320
  41. def OAI.SKRatioClock.Regression.queryColumn line 340
  42. def OAI.SKRatioClock.Regression.queryComplement line 342
  43. lemma OAI.SKRatioClock.Regression.queryColumn_unit line 345
  44. lemma OAI.SKRatioClock.Regression.gaussian_add_constant line 353
  45. lemma OAI.SKRatioClock.Regression.piGaussian_coordinates line 363
  46. lemma OAI.SKRatioClock.Regression.piGaussian_coordinate_mean line 368
  47. lemma OAI.SKRatioClock.Regression.piGaussian_coordinate_covariance line 373
  48. def OAI.SKRatioClock.Regression.sharedGaussianField line 388
  49. def OAI.SKRatioClock.Regression.sharedGaussianFieldCLM line 391
  50. lemma OAI.SKRatioClock.Regression.sharedGaussianField_gaussian line 397
  51. lemma OAI.SKRatioClock.Regression.sharedGaussianField_mean line 407
  52. lemma OAI.SKRatioClock.Regression.sharedGaussianField_covariance line 419