OAI/Combinatorics/KMedianRecovery/Machines/SensitiveMachine.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.pack line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.jf line 16
  3. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.jf_computes line 17
  4. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.isFree line 18
  5. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.isFree_computes line 19
  6. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.common line 21
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.common_computes line 22
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.small line 23
  9. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.small_computes line 24
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.large line 25
  11. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.large_computes line 26
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.views_pack line 27
  13. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.opened line 36
  14. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.opened_computes line 37
  15. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.base line 39
  16. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.base_computes line 40
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.base_pack line 41
  18. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.nextQ line 53
  19. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.nextQ_computes line 54
  20. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.context line 55
  21. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.context_computes line 56
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.context_pack line 69
  23. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.searchInput line 79
  24. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.searchInput_computes line 80
  25. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.atZero line 90
  26. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.atZero_computes line 91
  27. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.earlyEqual line 92
  28. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.earlyEqual_computes line 93
  29. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.early line 95
  30. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.early_computes line 96
  31. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.run line 99
  32. def OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.run_computes line 100
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySensitive.run_pack line 102
  34. lemma OAI.MetricKMedianRecovery.PhaseHistoryTransfer.History.phase_bound line 127
  35. lemma OAI.MetricKMedianRecovery.PhaseHistoryTransfer.History.flatten_bound line 141