OAI/Combinatorics/KMedian/Compression/GaussianListOperations.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Gaussian.ListOperation.Row line 14
  2. abbrev OAI.MetricKMedian.Gaussian.ListOperation.Rows line 15
  3. def OAI.MetricKMedian.Gaussian.ListOperation.erase line 17
  4. def OAI.MetricKMedian.Gaussian.ListOperation.insert line 19
  5. def OAI.MetricKMedian.Gaussian.ListOperation.pivot line 21
  6. def OAI.MetricKMedian.Gaussian.ListOperation.coefficients line 23
  7. def OAI.MetricKMedian.Gaussian.ListOperation.reduce line 25
  8. def OAI.MetricKMedian.Gaussian.ListOperation.residual line 28
  9. def OAI.MetricKMedian.Gaussian.ListOperation.lift line 31
  10. def OAI.MetricKMedian.Gaussian.ListOperation.basis line 34
  11. def OAI.MetricKMedian.Gaussian.ListOperation.matrix line 37
  12. theorem OAI.MetricKMedian.Gaussian.ListOperation.erase_eq line 40
  13. theorem OAI.MetricKMedian.Gaussian.ListOperation.erase_ofFn line 43
  14. theorem OAI.MetricKMedian.Gaussian.ListOperation.get_ofFn line 60
  15. theorem OAI.MetricKMedian.Gaussian.ListOperation.zip_ofFn line 65
  16. theorem OAI.MetricKMedian.Gaussian.ListOperation.coefficients_ofFn line 71
  17. theorem OAI.MetricKMedian.Gaussian.ListOperation.reduce_ofFn line 76
  18. theorem OAI.MetricKMedian.Gaussian.ListOperation.residual_matrix line 81
  19. theorem OAI.MetricKMedian.Gaussian.ListOperation.insert_eq line 87
  20. theorem OAI.MetricKMedian.Gaussian.ListOperation.insert_ofFn line 102
  21. theorem OAI.MetricKMedian.Gaussian.ListOperation.lift_ofFn line 131
  22. theorem OAI.MetricKMedian.Gaussian.ListOperation.basis_ofFn line 135