OAI/Probability/BinarySweep/MatrixBounds/BlockTrace.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.TraceHolder.pathProduct line 14
2. lemma OAI.BinaryCoordinateSweeps.TraceHolder.snoc_cons_succ line 18
3. lemma OAI.BinaryCoordinateSweeps.TraceHolder.pathProduct_cons line 27
4. lemma OAI.BinaryCoordinateSweeps.TraceHolder.prod_apply_sum_path line 34
5. lemma OAI.BinaryCoordinateSweeps.TraceHolder.snoc_cycle line 53
6. lemma OAI.BinaryCoordinateSweeps.TraceHolder.trace_prod_eq_sum_cycles line 60
7. def OAI.BinaryCoordinateSweeps.TraceHolder.flattenBlocks line 81
8. lemma OAI.BinaryCoordinateSweeps.TraceHolder.flattenBlocks_mul line 85
9. lemma OAI.BinaryCoordinateSweeps.TraceHolder.flattenBlocks_one line 91
10. def OAI.BinaryCoordinateSweeps.TraceHolder.flattenBlocksHom line 96
11. lemma OAI.BinaryCoordinateSweeps.TraceHolder.trace_flattenBlocks line 102
12. lemma OAI.BinaryCoordinateSweeps.TraceHolder.trace_flatten_prod line 108
13. theorem OAI.BinaryCoordinateSweeps.TraceHolder.block_trace_holder line 118
14. theorem OAI.BinaryCoordinateSweeps.TraceHolder.weighted_block_trace_holder line 133