OAI/Combinatorics/KMedianRecovery/Sampling/SeedTensor.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.product line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.product_computes line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.shape line 17
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySeed.shape_tail line 18
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySeed.product_shape line 20
  6. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.width line 25
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.width_computes line 26
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.chunk line 28
  9. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.chunk_computes line 31
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.child line 34
  11. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.child_computes line 36
  12. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.indices line 38
  13. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.indices_computes line 39
  14. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.nest line 41
  15. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.nest_computes line 44
  16. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.Tensor line 53
  17. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.raw line 56
  18. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.parsed line 59
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySeed.raw_length line 62
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySeed.chunk_tensor line 72
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySeed.nest_tensor line 83