OAI/Combinatorics/KMedian/Sparse/SparseBundleEncoding.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.SparseBundleEncoding.encode line 14
  2. def OAI.MetricKMedian.SparseBundleEncoding.decode line 18
  3. theorem OAI.MetricKMedian.SparseBundleEncoding.decode_encode line 22
  4. def OAI.MetricKMedian.SparseBundleEncoding.law line 29
  5. theorem OAI.MetricKMedian.SparseBundleEncoding.expectation line 33
  6. theorem OAI.MetricKMedian.SparseBundleEncoding.support line 43
  7. theorem OAI.MetricKMedian.SparseBundleEncoding.mean line 52
  8. theorem OAI.MetricKMedian.SparseBundleEncoding.pair line 60
  9. theorem OAI.MetricKMedian.SparseBundleEncoding.variance line 76
  10. def OAI.MetricKMedian.SparseRescaledInner.encodedLaw line 92
  11. def OAI.MetricKMedian.SparseRescaledInner.encodedCount line 96
  12. theorem OAI.MetricKMedian.SparseRescaledInner.encoded_pieces line 100
  13. theorem OAI.MetricKMedian.SparseRescaledInner.cast_scaled_piece line 114
  14. theorem OAI.MetricKMedian.SparseRescaledInner.encoded_mean line 121
  15. theorem OAI.MetricKMedian.SparseRescaledInner.encoded_pair line 134
  16. theorem OAI.MetricKMedian.SparseRescaledInner.encoded_variance line 154