OAI/Combinatorics/KMedianRecovery/Recovery/LowCandidate.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedianRecovery.IntegralCandidates.low_candidate line 12
2. def OAI.MetricKMedianRecovery.IntegralAssembly.gamma line 60
3. lemma OAI.MetricKMedianRecovery.IntegralAssembly.gamma_pos line 62
4. lemma OAI.MetricKMedianRecovery.IntegralAssembly.gamma_le_coarse line 67
5. lemma OAI.MetricKMedianRecovery.IntegralAssembly.gamma_le_strict line 68
6. lemma OAI.MetricKMedianRecovery.IntegralAssembly.gamma_lt_one line 69
7. theorem OAI.MetricKMedianRecovery.IntegralAssembly.finite_experiment line 71