OAI/Combinatorics/KMedianRecovery/Recovery/RecoveryContext.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.pack line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.choiceBits line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.qbits line 14
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.cbits line 15
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.bbits line 16
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.qbits_computes line 17
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.cbits_computes line 18
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.bbits_computes line 19
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.src line 20
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.src_computes line 21
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.cword line 22
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.bword line 23
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.cword_computes line 25
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.bword_computes line 26
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.zeros line 27
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.zeros_computes line 29
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.labels line 34
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.labels_computes line 35
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.context line 36
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.context_computes line 39
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.zeroContext line 45
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.zeroContext_computes line 47
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.qbits_pack line 57
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.cbits_pack line 58
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.bbits_pack line 59
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.cword_pack line 60
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.bword_pack line 64
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.zeros_pack line 68
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.labels_pack line 72
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.context_pack line 75
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.zeroContext_pack line 82