OAI/Analysis/Steinitz/GaussianProcess.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Stationary Gaussian autoregressive rows and covariance identities.

  1. def OAI.GaussianAR.row line 13
  2. lemma OAI.GaussianAR.row_support line 17
  3. lemma OAI.GaussianAR.row_initial line 22
  4. lemma OAI.GaussianAR.row_diag line 27
  5. lemma OAI.GaussianAR.row_dot_step line 30
  6. lemma OAI.GaussianAR.row_norm line 39
  7. lemma OAI.GaussianAR.row_covariance line 59
  8. lemma OAI.GaussianAR.row_norm_fin line 74
  9. lemma OAI.GaussianAR.row_covariance_fin line 79
  10. lemma OAI.GaussianAR.one_sub_pow_le line 84
  11. lemma OAI.GaussianTail.trace_covariance line 103
  12. lemma OAI.GaussianTail.squareMass_mul_covariance line 106
  13. lemma OAI.GaussianTail.squareMass_add_le line 112
  14. lemma OAI.GaussianTail.squareMass_neg line 122
  15. def OAI.GaussianAR.evaluation line 130
  16. lemma OAI.GaussianAR.evaluation_mul_transpose line 133
  17. lemma OAI.GaussianAR.evaluation_coisometry line 150
  18. lemma OAI.GaussianAR.evaluation_cross_symmetric line 156
  19. lemma OAI.GaussianAR.evaluation_difference_covariance line 169
  20. lemma OAI.GaussianAR.squareMass_evaluation line 181
  21. lemma OAI.GaussianAR.trace_weighted_square line 186
  22. lemma OAI.GaussianAR.squareMass_time_le line 196