OAI/Combinatorics/KMedianRecovery/Recovery/EvalTrans.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.eval_trans line 9
2. def OAI.MetricKMedianRecovery.BitMachine.MapLeft.parse_phase line 20
3. def OAI.MetricKMedianRecovery.BitMachine.MapLeft.restore_phase line 41
4. def OAI.MetricKMedianRecovery.BitMachine.MapLeft.reverse_phase line 50
5. def OAI.MetricKMedianRecovery.BitMachine.MapLeft.encode_phase line 59
6. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.initial line 69
7. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.final line 78
8. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.run_initial line 87
9. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.run_final line 91
10. def OAI.MetricKMedianRecovery.BitMachine.MapLeft.outputs line 96
11. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.mapLeft line 124