OAI/Combinatorics/KMedianRecovery/Encoding/CutMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.Ellipsoid.cutMatrix line 11
2. def OAI.MetricKMedianRecovery.Ellipsoid.quad line 14
3. lemma OAI.MetricKMedianRecovery.Ellipsoid.cutMatrix_pos line 17
4. lemma OAI.MetricKMedianRecovery.Ellipsoid.quad_cutMatrix line 26
5. lemma OAI.MetricKMedianRecovery.Ellipsoid.bilinear_symm line 35
6. lemma OAI.MetricKMedianRecovery.Ellipsoid.quad_add_scaled line 41
7. lemma OAI.MetricKMedianRecovery.Ellipsoid.quad_nonneg line 49
8. lemma OAI.MetricKMedianRecovery.Ellipsoid.matrix_cut_contains line 54
9. lemma OAI.MetricKMedianRecovery.Ellipsoid.rank_one_det line 74
10. lemma OAI.MetricKMedianRecovery.Ellipsoid.cutMatrix_det line 90