src/HOL/Probability/Essential_Supremum.thy
 changeset 68751 640386ab99f3 parent 67226 ec32cdaab97b child 69260 0a9688695a1b
equal inserted replaced
68750:7087748996af 68751:640386ab99f3
`   117   "esssup M (\<lambda>x. f x + g x::ereal) \<le> esssup M f + esssup M g"`
`   117   "esssup M (\<lambda>x. f x + g x::ereal) \<le> esssup M f + esssup M g"`
`   118 proof (cases "f \<in> borel_measurable M \<and> g \<in> borel_measurable M")`
`   118 proof (cases "f \<in> borel_measurable M \<and> g \<in> borel_measurable M")`
`   119   case True`
`   119   case True`
`   120   then have [measurable]: "(\<lambda>x. f x + g x) \<in> borel_measurable M" by auto`
`   120   then have [measurable]: "(\<lambda>x. f x + g x) \<in> borel_measurable M" by auto`
`   121   have "f x + g x \<le> esssup M f + esssup M g" if "f x \<le> esssup M f" "g x \<le> esssup M g" for x`
`   121   have "f x + g x \<le> esssup M f + esssup M g" if "f x \<le> esssup M f" "g x \<le> esssup M g" for x`
`   122     using that ereal_add_mono by auto`
`   122     using that add_mono by auto`
`   123   then have "AE x in M. f x + g x \<le> esssup M f + esssup M g"`
`   123   then have "AE x in M. f x + g x \<le> esssup M f + esssup M g"`
`   124     using esssup_AE[of f M] esssup_AE[of g M] by auto`
`   124     using esssup_AE[of f M] esssup_AE[of g M] by auto`
`   125   then show ?thesis using esssup_I by auto`
`   125   then show ?thesis using esssup_I by auto`
`   126 next`
`   126 next`
`   127   case False`
`   127   case False`