OAI/Combinatorics/KMedianRecovery/Sampling/SamplerLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Guided.Realized.adaptive_actions line 9
2. lemma OAI.MetricKMedianRecovery.Guided.Realized.adaptive_list line 16
3. lemma OAI.MetricKMedianRecovery.RationalSampling.next_real line 26
4. lemma OAI.MetricKMedianRecovery.RationalSampling.adaptive_real line 36
5. lemma OAI.MetricKMedianRecovery.RationalSampling.canonical_average line 44
6. lemma OAI.MetricKMedianRecovery.Guided.states_map line 65
7. lemma OAI.MetricKMedianRecovery.Guided.states_list line 74
8. lemma OAI.MetricKMedianRecovery.Guided.Realized.states_actions line 86
9. lemma OAI.MetricKMedianRecovery.RationalSampling.trace_average line 102
10. lemma OAI.MetricKMedianRecovery.RationalSampling.trace_probability line 121