OAI/Combinatorics/KMedian/Compression/GaussianListSize.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Gaussian.ListOperation.rowBound line 13
  2. def OAI.MetricKMedian.Gaussian.ListOperation.matrixBound line 14
  3. def OAI.MetricKMedian.Gaussian.ListOperation.frameBound line 15
  4. def OAI.MetricKMedian.Gaussian.ListOperation.framesBound line 16
  5. def OAI.MetricKMedian.Gaussian.ListOperation.stateBound line 17
  6. def OAI.MetricKMedian.Gaussian.ListOperation.FrameValid line 19
  7. def OAI.MetricKMedian.Gaussian.ListOperation.FramesValid line 21
  8. def OAI.MetricKMedian.Gaussian.ListOperation.kernelList line 23
  9. def OAI.MetricKMedian.Gaussian.ListOperation.Audit line 26
  10. theorem OAI.MetricKMedian.Gaussian.ListOperation.slots_size line 31
  11. theorem OAI.MetricKMedian.Gaussian.ListOperation.row_size line 36
  12. theorem OAI.MetricKMedian.Gaussian.ListOperation.frame_size line 41
  13. theorem OAI.MetricKMedian.Gaussian.ListOperation.frames_size line 48
  14. theorem OAI.MetricKMedian.Gaussian.ListOperation.matrix_size line 53
  15. theorem OAI.MetricKMedian.Gaussian.ListOperation.desc_size line 65
  16. theorem OAI.MetricKMedian.Gaussian.ListOperation.up_size line 74
  17. theorem OAI.MetricKMedian.Gaussian.ListOperation.audit_head line 84