summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Probability_Measure.thy

changeset 56166 | 9a241bc276cd |

parent 54418 | 3b8e33d1a39a |

child 56993 | e5366291d6aa |

1.1 --- a/src/HOL/Probability/Probability_Measure.thy Sat Mar 15 16:54:32 2014 +0100 1.2 +++ b/src/HOL/Probability/Probability_Measure.thy Sun Mar 16 18:09:04 2014 +0100 1.3 @@ -159,7 +159,7 @@ 1.4 moreover 1.5 { fix y assume y: "y \<in> I" 1.6 with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y" 1.7 - by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) } 1.8 + by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open simp del: Sup_image_eq Inf_image_eq) } 1.9 ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)" 1.10 by simp 1.11 also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"