OAI/Combinatorics/KMedianRecovery/Encoding/RationalInflatedShape.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.Ellipsoid.rational_symm_of_real line 12
  2. lemma OAI.MetricKMedianRecovery.Ellipsoid.real_smul_matrix line 18
  3. def OAI.MetricKMedianRecovery.Ellipsoid.rationalInflatedShape line 23
  4. def OAI.MetricKMedianRecovery.Ellipsoid.rationalStepShape line 26
  5. def OAI.MetricKMedianRecovery.Ellipsoid.rationalStepCenter line 29
  6. lemma OAI.MetricKMedianRecovery.Ellipsoid.real_inflatedShape line 33
  7. lemma OAI.MetricKMedianRecovery.Ellipsoid.real_stepCenter line 40
  8. lemma OAI.MetricKMedianRecovery.Ellipsoid.realVector_ne_zero line 51
  9. lemma OAI.MetricKMedianRecovery.Ellipsoid.stepShape_pos_bounds line 58
  10. lemma OAI.MetricKMedianRecovery.Ellipsoid.rational_step_contains line 80
  11. lemma OAI.MetricKMedianRecovery.Ellipsoid.rational_step_growth line 109