OAI/Combinatorics/KMedian/Compression/GaussianResidualCertificate.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Gaussian.rowValue line 12
  2. theorem OAI.MetricKMedian.Gaussian.rowValue_sub line 15
  3. theorem OAI.MetricKMedian.Gaussian.rowValue_smul line 25
  4. structure OAI.MetricKMedian.Gaussian.ResidualCertificate line 32
  5. theorem OAI.MetricKMedian.Gaussian.ResidualCertificate.decompose line 52
  6. theorem OAI.MetricKMedian.Gaussian.ResidualCertificate.circuit line 66
  7. def OAI.MetricKMedian.Gaussian.ResidualCertificate.initial line 75
  8. def OAI.MetricKMedian.Gaussian.ResidualCertificate.skip line 90
  9. theorem OAI.MetricKMedian.Gaussian.ResidualCertificate.next_row_ne line 108
  10. theorem OAI.MetricKMedian.Gaussian.ResidualCertificate.firstCoeff_next line 112
  11. def OAI.MetricKMedian.Gaussian.ResidualCertificate.pivot line 116