OAI/Combinatorics/KMedianRecovery/Strictness/NormalizedDual.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Ellipsoid.hermitian_vecMul line 12
2. lemma OAI.MetricKMedianRecovery.Ellipsoid.rank_one_shape_inverse line 17
3. def OAI.MetricKMedianRecovery.Ellipsoid.normalizedDual line 34
4. lemma OAI.MetricKMedianRecovery.Ellipsoid.dual_normal_properties line 37
5. def OAI.MetricKMedianRecovery.Ellipsoid.cutShape line 54
6. lemma OAI.MetricKMedianRecovery.Ellipsoid.cutShape_inverse line 57