OAI/Probability/SpanningForest/USTFiniteTilt.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336.USTResponse.observationField line 10
2. def OAI.Problem336.USTResponse.finiteTilt line 14
3. lemma OAI.Problem336.USTResponse.finiteTilt_of_mem line 18
4. lemma OAI.Problem336.USTResponse.finiteTilt_of_not_mem line 23
5. lemma OAI.Problem336.USTResponse.finiteTilt_mem_Icc line 28
6. lemma OAI.Problem336.USTResponse.continuous_observationField line 37
7. lemma OAI.Problem336.USTResponse.continuous_finiteTilt line 44
8. lemma OAI.Problem336.USTResponse.measurable_finiteTilt line 53
9. lemma OAI.Problem336.USTResponse.finiteTilt_eq_zero_of_no_trees line 58
10. lemma OAI.Problem336.USTResponse.continuous_finiteTilt_unconditional line 66
11. lemma OAI.Problem336.USTResponse.measurable_finiteTilt_unconditional line 74
12. lemma OAI.Problem336.USTResponse.measurable_finiteTilt_joint line 79
13. theorem OAI.Problem336.USTResponse.finiteTilt_response_of_response line 87
14. theorem OAI.Problem336.USTResponse.finiteTilt_response line 104
15. lemma OAI.Problem336.USTResponse.observationField_zero line 120
16. lemma OAI.Problem336.USTResponse.observationField_empty line 125
17. lemma OAI.Problem336.USTResponse.finiteTilt_empty_eq_zero_field line 130
18. lemma OAI.Problem336.USTResponse.finiteTilt_zero_eq_ustCylinder_of_mem line 135