OAI/Combinatorics/KMedianRecovery/Recovery/RealVector.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Ellipsoid.realVector line 14
  2. def OAI.MetricKMedianRecovery.Ellipsoid.rationalQuad line 16
  3. def OAI.MetricKMedianRecovery.Ellipsoid.rationalCutShape line 18
  4. def OAI.MetricKMedianRecovery.Ellipsoid.rationalRootUpper line 21
  5. lemma OAI.MetricKMedianRecovery.Ellipsoid.rationalRootUpper_bounds line 23
  6. lemma OAI.MetricKMedianRecovery.Ellipsoid.real_mulVec line 38
  7. lemma OAI.MetricKMedianRecovery.Ellipsoid.real_quad line 44
  8. lemma OAI.MetricKMedianRecovery.Ellipsoid.real_cutShape line 50
  9. lemma OAI.MetricKMedianRecovery.Ellipsoid.sqrt_ratio line 60
  10. lemma OAI.MetricKMedianRecovery.Ellipsoid.quad_single line 83
  11. lemma OAI.MetricKMedianRecovery.Ellipsoid.entry_bound_of_diagonal line 86
  12. lemma OAI.MetricKMedianRecovery.Ellipsoid.det_bound_of_diameters line 97
  13. lemma OAI.MetricKMedianRecovery.Ellipsoid.cutMatrix_grows line 112
  14. lemma OAI.MetricKMedianRecovery.Ellipsoid.block_growth line 119
  15. lemma OAI.MetricKMedianRecovery.Ellipsoid.sequence_growth line 125