OAI/Probability/SKRatio/Matrices/GaussianRows.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatioGaussian.gaussian_coordinates_norm_mean line 15
2. lemma OAI.SKRatioGaussian.scaled_gaussian_radius_tail line 32
3. lemma OAI.SKRatioGaussian.coupling_goe_row_tight_tail line 76
4. lemma OAI.SKRatioGaussian.coupling_goe_all_rows_tight_tail line 126