OAI/Combinatorics/KMedian/Sparse/SparseHistories.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.SparseHistories.History line 12
2. def OAI.MetricKMedian.SparseHistories.extend line 14
3. def OAI.MetricKMedian.SparseHistories.branch line 16
4. def OAI.MetricKMedian.SparseHistories.tree line 19
5. theorem OAI.MetricKMedian.SparseHistories.tree_length line 23
6. theorem OAI.MetricKMedian.SparseHistories.tree_property line 31
7. theorem OAI.MetricKMedian.SparseHistories.past_length line 46
8. theorem OAI.MetricKMedian.SparseHistories.physical_invariant line 51
9. theorem OAI.MetricKMedian.SparseHistories.expectation_step line 57