OAI/Probability/FreeIsing/Trees/ColoredPathAverage.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.ColoredPathAverage.Path line 10
2. instance OAI.Problem367.ColoredPathAverage.pathFintype line 14
3. def OAI.Problem367.ColoredPathAverage.colors line 21
4. theorem OAI.Problem367.ColoredPathAverage.colors_length line 25
5. theorem OAI.Problem367.ColoredPathAverage.colors_head? line 31
6. theorem OAI.Problem367.ColoredPathAverage.colors_isChain line 35
7. def OAI.Problem367.ColoredPathAverage.pathValue line 51
8. theorem OAI.Problem367.ColoredPathAverage.pathValue_zero line 56
9. theorem OAI.Problem367.ColoredPathAverage.pathValue_succ line 60
10. theorem OAI.Problem367.ColoredPathAverage.forwardOperator_pow_apply line 64