summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Probability/Giry_Monad.thy

changeset 59978 | c2dc7856e2e5 |

parent 59778 | fe5b796d6b2a |

child 60067 | f1a5bcf5658f |

equal
deleted
inserted
replaced

59977:ad2d1cd53877 | 59978:c2dc7856e2e5 |
---|---|

322 also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M" |
322 also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M" |

323 by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq) |
323 by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq) |

324 finally show ?thesis . |
324 finally show ?thesis . |

325 qed |
325 qed |

326 |
326 |

327 (* TODO: Rename. This name is too general – Manuel *) |
327 (* TODO: Rename. This name is too general -- Manuel *) |

328 lemma measurable_pair_measure: |
328 lemma measurable_pair_measure: |

329 assumes f: "f \<in> measurable M (subprob_algebra N)" |
329 assumes f: "f \<in> measurable M (subprob_algebra N)" |

330 assumes g: "g \<in> measurable M (subprob_algebra L)" |
330 assumes g: "g \<in> measurable M (subprob_algebra L)" |

331 shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))" |
331 shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))" |

332 proof (rule measurable_subprob_algebra) |
332 proof (rule measurable_subprob_algebra) |