OAI/Combinatorics/KMedian/Process/CountSource.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.SourceBalance.bias line 13
2. theorem OAI.MetricKMedian.SourceBalance.bias_lower line 17
3. theorem OAI.MetricKMedian.SourceBalance.bias_upper line 23
4. theorem OAI.MetricKMedian.SourceBalance.sum_biased_imbalance line 28
5. theorem OAI.MetricKMedian.FixedBatch.graph_mass_sum line 50
6. theorem OAI.MetricKMedian.FixedBatch.masked_mass_sum line 68
7. theorem OAI.MetricKMedian.FixedBatch.masked_opening_sum_le line 80
8. theorem OAI.MetricKMedian.FixedBatch.masked_total_bound line 92
9. theorem OAI.MetricKMedian.FixedBatch.masked_biased_linear_bound line 110