OAI/Combinatorics/KMedianRecovery/Geometry/NearestLeafMachine.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryNearestLeaf.leavesBits line 10
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryNearestLeaf.distance line 11
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryNearestLeaf.distance_computes line 14
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNearestLeaf.distance_pair line 17
5. def OAI.MetricKMedianRecovery.BitMachine.BinaryNearestLeaf.distances line 21
6. def OAI.MetricKMedianRecovery.BitMachine.BinaryNearestLeaf.distances_computes line 22
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNearestLeaf.distances_pair line 23
8. def OAI.MetricKMedianRecovery.BitMachine.BinaryNearestLeaf.empty line 26
9. def OAI.MetricKMedianRecovery.BitMachine.BinaryNearestLeaf.empty_computes line 27
10. def OAI.MetricKMedianRecovery.BitMachine.BinaryNearestLeaf.run line 28
11. def OAI.MetricKMedianRecovery.BitMachine.BinaryNearestLeaf.run_computes line 30
12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNearestLeaf.run_pair line 35