OAI/Probability/MatroidProphet/Reverse/SquareSum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatroidProphet.reverseCost_add_steps line 10
2. lemma OAI.MatroidProphet.reverseCost_eq_sum line 25
3. def OAI.MatroidProphet.pathExitSquare line 38
4. lemma OAI.MatroidProphet.reverse_square_eq_path_sum line 45
5. theorem OAI.MatroidProphet.path_squared_exit_mass line 69