OAI/Probability/BinarySweep/Trajectories/PathExtension.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BinaryCoordinateSweeps.PathExtension line 12
2. def OAI.BinaryCoordinateSweeps.PathExtension.lineEmbedding line 21
3. lemma OAI.BinaryCoordinateSweeps.PathExtension.lineInput_eq line 29
4. lemma OAI.BinaryCoordinateSweeps.PathExtension.lineOutput_eq line 35
5. lemma OAI.BinaryCoordinateSweeps.PathExtension.pathEvent_mono line 41
6. lemma OAI.BinaryCoordinateSweeps.PathExtension.card_le line 46
7. lemma OAI.BinaryCoordinateSweeps.localPathWeight_pos_comparison line 51
8. lemma OAI.BinaryCoordinateSweeps.lineExtension_log_bound line 70
9. lemma OAI.BinaryCoordinateSweeps.log_gridSize line 92
10. lemma OAI.BinaryCoordinateSweeps.sum_lineHoles_sub line 99
11. lemma OAI.BinaryCoordinateSweeps.pathCost_eq_sum line 104
12. theorem OAI.BinaryCoordinateSweeps.pathExtension_log_ratio line 107
13. def OAI.BinaryCoordinateSweeps.conditionalEventWeight line 139
14. lemma OAI.BinaryCoordinateSweeps.pathExtension_event_ratio line 143
15. lemma OAI.BinaryCoordinateSweeps.gridSize_pos line 165
16. theorem OAI.BinaryCoordinateSweeps.pathExtension_probability_bound line 169