OAI/Combinatorics/KMedianRecovery/Recovery/SqNorm.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Ellipsoid.sqNorm line 13
  2. lemma OAI.MetricKMedianRecovery.Ellipsoid.quad_one line 15
  3. lemma OAI.MetricKMedianRecovery.Ellipsoid.quad_sub_matrix line 19
  4. lemma OAI.MetricKMedianRecovery.Ellipsoid.quad_entry_perturb line 23
  5. lemma OAI.MetricKMedianRecovery.Ellipsoid.posSemidef_of_quad line 45
  6. def OAI.MetricKMedianRecovery.Ellipsoid.lowerRound line 50
  7. lemma OAI.MetricKMedianRecovery.Ellipsoid.lowerRound_bounds line 53
  8. lemma OAI.MetricKMedianRecovery.Ellipsoid.lowerRound_relative line 72
  9. lemma OAI.MetricKMedianRecovery.Ellipsoid.lowerRound_pos line 89
  10. lemma OAI.MetricKMedianRecovery.Ellipsoid.lowerRound_det line 99
  11. lemma OAI.MetricKMedianRecovery.Ellipsoid.posDef_mul_inverse_vec line 116
  12. lemma OAI.MetricKMedianRecovery.Ellipsoid.quad_inverse_vec line 120
  13. lemma OAI.MetricKMedianRecovery.Ellipsoid.inverse_antitone line 125
  14. lemma OAI.MetricKMedianRecovery.Ellipsoid.inv_smul_real line 138