OAI/Probability/SKValue/GroundState/RandomColumn.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValueG.measurable_finiteMaximum line 14
2. lemma OAI.SKValueG.integrable_randomMaximum line 19
3. lemma OAI.SKValueG.random_linear_integrable line 28
4. lemma OAI.SKValueG.measurable_quadraticValue line 43
5. lemma OAI.SKValueG.random_quadratic_integrable line 54
6. lemma OAI.SKValueG.columnVector_coord_bound line 70
7. theorem OAI.SKValueG.random_column_identity line 74
8. abbrev OAI.SKValueG.ColumnHistory line 112
9. def OAI.SKValueG.columnHistoryLaw line 113
10. instance OAI.SKValueG.(instance at line 115) line 115
11. def OAI.SKValueG.historyInit line 118
12. def OAI.SKValueG.historySplit line 120
13. lemma OAI.SKValueG.historySplit_apply line 125
14. lemma OAI.SKValueG.historySplit_preserving line 130
15. lemma OAI.SKValueG.historyInit_measurable line 137
16. lemma OAI.SKValueG.history_integral_succ line 140
17. lemma OAI.SKValueG.history_integrable_succ line 145