OAI/Combinatorics/KMedianRecovery/Recovery/FormTrans.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Ellipsoid.form_le_trans line 14
2. lemma OAI.MetricKMedianRecovery.Ellipsoid.form_le_smul line 21
3. lemma OAI.MetricKMedianRecovery.Ellipsoid.form_scalar_mono line 26
4. lemma OAI.MetricKMedianRecovery.Ellipsoid.cutShape_lower line 30
5. lemma OAI.MetricKMedianRecovery.Ellipsoid.inflatedShape_lower line 41
6. lemma OAI.MetricKMedianRecovery.Ellipsoid.stepShape_lower line 54
7. lemma OAI.MetricKMedianRecovery.Ellipsoid.stepShape_pos line 68
8. lemma OAI.MetricKMedianRecovery.Ellipsoid.stepShape_upper line 76
9. def OAI.MetricKMedianRecovery.Ellipsoid.gridDenominator line 99
10. lemma OAI.MetricKMedianRecovery.Ellipsoid.gridDenominator_pos line 101
11. lemma OAI.MetricKMedianRecovery.Ellipsoid.gridDenominator_precision line 105
12. lemma OAI.MetricKMedianRecovery.Ellipsoid.iterate_lower line 113
13. lemma OAI.MetricKMedianRecovery.Ellipsoid.inflatedShape_precision line 124
14. lemma OAI.MetricKMedianRecovery.Ellipsoid.gridDenominator_size line 135