OAI/Probability/PosteriorReplicas/Regression/GramDistances.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorRegression.sub_gramSchmidt_mem_span line 16
2. lemma OAI.PosteriorRegression.gramSchmidt_mem_span_orthogonal line 25
3. lemma OAI.PosteriorRegression.gramSchmidt_eq_sub_starProjection line 37
4. lemma OAI.PosteriorRegression.norm_gramSchmidt_eq_infDist line 45
5. lemma OAI.PosteriorRegression.infDist_affine_mk' line 52
6. lemma OAI.PosteriorRegression.norm_gramSchmidt_sub_eq_affine_infDist line 66
7. lemma OAI.PosteriorRegression.image_Iio_castSucc line 73
8. lemma OAI.PosteriorRegression.image_Iio_last line 84
9. lemma OAI.PosteriorRegression.gramSchmidt_castSucc line 93
10. lemma OAI.PosteriorRegression.measurable_gramSchmidt line 99