OAI/Combinatorics/KMedian/Process/GeneratorAverage.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.GeneratorAverage.inside line 14
2. def OAI.MetricKMedian.GeneratorAverage.outside line 16
3. def OAI.MetricKMedian.GeneratorAverage.external line 19
4. theorem OAI.MetricKMedian.GeneratorAverage.inside_mean line 25
5. theorem OAI.MetricKMedian.GeneratorAverage.mass_mean line 46
6. theorem OAI.MetricKMedian.GeneratorAverage.cost_mean line 52
7. theorem OAI.MetricKMedian.GeneratorAverage.external_mean_split line 59
8. theorem OAI.MetricKMedian.GeneratorAverage.drift_decomposition line 103