OAI/Combinatorics/KMedianRecovery/Sampling/RealizedKernel.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MetricKMedianRecovery.Guided.Realized.Draw line 11
2. def OAI.MetricKMedianRecovery.Guided.Realized.actions line 14
3. theorem OAI.MetricKMedianRecovery.Guided.Realized.actions_average line 18
4. lemma OAI.MetricKMedianRecovery.Guided.Realized.actions_probability line 40
5. def OAI.MetricKMedianRecovery.Guided.Realized.canonical line 47
6. lemma OAI.MetricKMedianRecovery.Guided.Realized.canonical_law line 51
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.zipIdx_ofFn_nat line 60
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.finEnum_perm line 66
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.canonical_run line 70
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.canonical_average line 80
11. def OAI.MetricKMedianRecovery.RationalSampling.entries line 92
12. lemma OAI.MetricKMedianRecovery.RationalSampling.mem_entries line 96
13. lemma OAI.MetricKMedianRecovery.RationalSampling.entries_nodup line 101
14. def OAI.MetricKMedianRecovery.RationalSampling.clients line 111
15. lemma OAI.MetricKMedianRecovery.RationalSampling.clients_nodup line 112
16. lemma OAI.MetricKMedianRecovery.RationalSampling.mem_clients line 113
17. def OAI.MetricKMedianRecovery.RationalSampling.actions line 114
18. lemma OAI.MetricKMedianRecovery.RationalSampling.actions_nodup line 117
19. lemma OAI.MetricKMedianRecovery.RationalSampling.mem_actions line 125
20. lemma OAI.MetricKMedianRecovery.RationalSampling.actions_perm line 132
21. def OAI.MetricKMedianRecovery.RationalSampling.entryCode line 135
22. lemma OAI.MetricKMedianRecovery.RationalSampling.entry_weight line 139
23. def OAI.MetricKMedianRecovery.RationalSampling.actionCode line 142