OAI/Combinatorics/KMedianRecovery/Recovery/Next.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.next line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.interval line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.Bracket line 16
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.initial_bracket line 18
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.next_bracket line 27
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.interval_bracket line 37
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.next_width line 41
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.interval_width line 47
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.interval_correct line 56
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.pack line 65
  11. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.low line 66
  12. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.high line 67
  13. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.low_computes line 68
  14. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.high_computes line 69
  15. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.middle line 71
  16. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.middle_computes line 72
  17. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.leftCase line 77
  18. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.rightCase line 78
  19. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.leftCase_computes line 79
  20. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.rightCase_computes line 81
  21. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.step line 83
  22. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.step_computes line 85
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.step_pack line 90
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.iterate_pack line 94
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.length_pack line 99
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.iterate_length line 102
  27. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.startWords line 111
  28. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.startWords_computes line 112
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.startWords_bits line 117
  30. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.run line 121
  31. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.run_computes line 123
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.run_bits line 126
  33. def OAI.MetricKMedianRecovery.BitMachine.BinarySqrt.sqrt line 141