OAI/Combinatorics/KMedian/Compression/GaussianListMachine.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Gaussian.ListOperation.Frame line 13
  2. abbrev OAI.MetricKMedian.Gaussian.ListOperation.Frames line 14
  3. abbrev OAI.MetricKMedian.Gaussian.ListOperation.Desc line 15
  4. abbrev OAI.MetricKMedian.Gaussian.ListOperation.Up line 16
  5. abbrev OAI.MetricKMedian.Gaussian.ListOperation.State line 17
  6. abbrev OAI.MetricKMedian.Gaussian.ListOperation.efs line 18
  7. abbrev OAI.MetricKMedian.Gaussian.ListOperation.edata line 19
  8. abbrev OAI.MetricKMedian.Gaussian.ListOperation.ed line 20
  9. abbrev OAI.MetricKMedian.Gaussian.ListOperation.eUp line 21
  10. abbrev OAI.MetricKMedian.Gaussian.ListOperation.eState line 22
  11. def OAI.MetricKMedian.Gaussian.ListOperation.down line 24
  12. def OAI.MetricKMedian.Gaussian.ListOperation.up line 34
  13. def OAI.MetricKMedian.Gaussian.ListOperation.body line 40
  14. def OAI.MetricKMedian.Gaussian.ListOperation.downProgram line 42
  15. def OAI.MetricKMedian.Gaussian.ListOperation.upProgram line 64
  16. def OAI.MetricKMedian.Gaussian.ListOperation.bodyProgram line 74