OAI/Probability/GaussianRegression/Gram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Gram determinants, orthogonal distances, and product integration.

  1. lemma OAI.NoiselessRegression.gram_linear_combination line 22
  2. def OAI.NoiselessRegression.gsUpper line 36
  3. lemma OAI.NoiselessRegression.gsUpper_expansion line 40
  4. lemma OAI.NoiselessRegression.gsUpper_det line 51
  5. lemma OAI.NoiselessRegression.gram_gramSchmidt_diagonal line 59
  6. theorem OAI.NoiselessRegression.det_gram_eq_prod_gramSchmidt line 68
  7. lemma OAI.NoiselessRegression.sub_gramSchmidt_mem_span line 82
  8. lemma OAI.NoiselessRegression.gramSchmidt_mem_span_orthogonal line 91
  9. lemma OAI.NoiselessRegression.gramSchmidt_eq_sub_starProjection line 103
  10. lemma OAI.NoiselessRegression.norm_gramSchmidt_eq_infDist line 111
  11. lemma OAI.NoiselessRegression.infDist_affine_mk' line 118
  12. lemma OAI.NoiselessRegression.norm_gramSchmidt_sub_eq_affine_infDist line 132
  13. lemma OAI.NoiselessRegression.image_Iio_castSucc line 139
  14. lemma OAI.NoiselessRegression.image_Iio_last line 150
  15. lemma OAI.NoiselessRegression.gramSchmidt_castSucc line 159
  16. lemma OAI.NoiselessRegression.measurable_gramSchmidt line 165
  17. lemma OAI.NoiselessRegression.lintegral_pi_snoc line 186