changeset 36649 | bfd8c550faa6 |
parent 35977 | 30d42bfd0174 |
child 38656 | d5d342611edb |
36648:43b66dcd9266 | 36649:bfd8c550faa6 |
---|---|
1 theory Product_Measure |
1 theory Product_Measure |
2 imports "~~/src/HOL/Probability/Lebesgue" |
2 imports Lebesgue |
3 begin |
3 begin |
4 |
4 |
5 definition |
5 definition |
6 "prod_measure M M' = (\<lambda>a. measure_space.integral M (\<lambda>s0. measure M' ((\<lambda>s1. (s0, s1)) -` a)))" |
6 "prod_measure M M' = (\<lambda>a. measure_space.integral M (\<lambda>s0. measure M' ((\<lambda>s1. (s0, s1)) -` a)))" |
7 |
7 |