OAI/Probability/SKRatio/Matrices/QuadraticCoeff.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.quadraticCoeff line 55
2. def OAI.SKRatioGaussian.linearCoeff line 59
3. lemma OAI.SKRatioGaussian.sum_coord_sq line 63
4. lemma OAI.SKRatioGaussian.sum_outer_sq line 66
5. lemma OAI.SKRatioGaussian.quadraticCoeff_increment line 76
6. lemma OAI.SKRatioGaussian.linearCoeff_increment line 92
7. theorem OAI.SKRatioGaussian.quadratic_linear_increment_difference line 110
8. theorem OAI.SKRatioGaussian.quadratic_linear_increment_le line 119
9. lemma OAI.SKRatioGaussian.quadratic_linear_orthogonal line 128
10. lemma OAI.SKRatioGaussian.continuous_quadraticCoeff line 136
11. lemma OAI.SKRatioGaussian.continuous_linearCoeff line 145