author hoelzl Thu Oct 20 18:41:58 2016 +0200 (2016-10-20) changeset 64319 a33bbac43359 parent 64318 1e92b5c35615 child 64320 ba194424b895
HOL-Probability: generalize type of essential supremum
     1.1 --- a/src/HOL/Probability/Essential_Supremum.thy	Thu Oct 20 17:28:09 2016 +0200
1.2 +++ b/src/HOL/Probability/Essential_Supremum.thy	Thu Oct 20 18:41:58 2016 +0200
1.3 @@ -13,18 +13,18 @@
1.4  of measure $0$. It is convenient to define it to be infinity for non-measurable functions, as
1.5  it allows for neater statements in general. This is a prerequisiste to define the space $L^\infty$.*}
1.6
1.7 -definition esssup::"'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal"
1.8 -  where "esssup M f = (if f \<in> borel_measurable M then Inf {z. emeasure M {x \<in> space M. f x > z} = 0} else \<infinity>)"
1.9 +definition esssup::"'a measure \<Rightarrow> ('a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology, complete_linorder}) \<Rightarrow> 'b"
1.10 +  where "esssup M f = (if f \<in> borel_measurable M then Inf {z. emeasure M {x \<in> space M. f x > z} = 0} else top)"
1.11
1.12  lemma esssup_zero_measure:
1.13    "emeasure M {x \<in> space M. f x > esssup M f} = 0"
1.14 -proof (cases "esssup M f = \<infinity>")
1.15 +proof (cases "esssup M f = top")
1.16    case True
1.17    then show ?thesis by auto
1.18  next
1.19    case False
1.20    then have [measurable]: "f \<in> borel_measurable M" unfolding esssup_def by meson
1.21 -  have "esssup M f < \<infinity>" using False by auto
1.22 +  have "esssup M f < top" using False by (auto simp: less_top)
1.23    have *: "{x \<in> space M. f x > z} \<in> null_sets M" if "z > esssup M f" for z
1.24    proof -
1.25      have "\<exists>w. w < z \<and> emeasure M {x \<in> space M. f x > w} = 0"
1.26 @@ -35,8 +35,8 @@
1.27      have b: "{x \<in> space M. f x > z} \<subseteq> {x \<in> space M. f x > w}" using w < z by auto
1.28      show ?thesis using null_sets_subset[OF a _ b] by simp
1.29    qed
1.30 -  obtain u::"nat \<Rightarrow> ereal" where u: "\<And>n. u n > esssup M f" "u \<longlonglongrightarrow> esssup M f"
1.31 -    using approx_from_above_dense_linorder[OF esssup M f < \<infinity>] by auto
1.32 +  obtain u::"nat \<Rightarrow> 'b" where u: "\<And>n. u n > esssup M f" "u \<longlonglongrightarrow> esssup M f"
1.33 +    using approx_from_above_dense_linorder[OF esssup M f < top] by auto
1.34    have "{x \<in> space M. f x > esssup M f} = (\<Union>n. {x \<in> space M. f x > u n})"
1.35      using u apply auto
1.36      apply (metis (mono_tags, lifting) order_tendsto_iff eventually_mono LIMSEQ_unique)
1.37 @@ -54,7 +54,7 @@
1.38      apply (rule AE_I[OF _ esssup_zero_measure[of _ f]]) using True by auto
1.39  next
1.40    case False
1.41 -  then have "esssup M f = \<infinity>" unfolding esssup_def by auto
1.42 +  then have "esssup M f = top" unfolding esssup_def by auto
1.43    then show ?thesis by auto
1.44  qed
1.45
1.46 @@ -65,7 +65,7 @@
1.47
1.48  lemma esssup_non_measurable:
1.49    assumes "f \<notin> borel_measurable M"
1.50 -  shows "esssup M f = \<infinity>"
1.51 +  shows "esssup M f = top"
1.52  using assms unfolding esssup_def by auto
1.53
1.54  lemma esssup_I [intro]:
1.55 @@ -122,7 +122,7 @@
1.56
1.57  lemma esssup_cmult:
1.58    assumes "c > (0::real)"
1.59 -  shows "esssup M (\<lambda>x. c * f x) = c * esssup M f"
1.60 +  shows "esssup M (\<lambda>x. c * f x::ereal) = c * esssup M f"
1.61  proof (cases "f \<in> borel_measurable M")
1.62    case True
1.63    then have a [measurable]: "f \<in> borel_measurable M" by simp
1.64 @@ -154,8 +154,8 @@
1.65    finally show ?thesis by simp
1.66  next
1.67    case False
1.68 -  have "esssup M f = \<infinity>" using False unfolding esssup_def by auto
1.69 -  then have *: "c * esssup M f = \<infinity>" using assms by (simp add: ennreal_mult_eq_top_iff)
1.70 +  have "esssup M f = top" using False unfolding esssup_def by auto
1.71 +  then have *: "c * esssup M f = \<infinity>" using assms by (simp add: ennreal_mult_eq_top_iff top_ereal_def)
1.72    have "(\<lambda>x. c * f x) \<notin> borel_measurable M"
1.73    proof (rule ccontr)
1.74      assume "\<not> (\<lambda>x. c * f x) \<notin> borel_measurable M"
1.75 @@ -165,12 +165,12 @@
1.76        by (metis "*" PInfty_neq_ereal(1) divide_inverse divide_self_if ereal_zero_mult mult.assoc mult.commute mult.left_neutral one_ereal_def times_ereal.simps(1) zero_ereal_def)
1.77      ultimately show False using False by auto
1.78    qed
1.79 -  then have "esssup M (\<lambda>x. c * f x) = \<infinity>" unfolding esssup_def by simp
1.80 +  then have "esssup M (\<lambda>x. c * f x) = \<infinity>" unfolding esssup_def by (simp add: top_ereal_def)
1.81    then show ?thesis using * by auto
1.82  qed
1.83
1.85 -  "esssup M (\<lambda>x. f x + g x) \<le> esssup M f + esssup M g"
1.86 +  "esssup M (\<lambda>x. f x + g x::ereal) \<le> esssup M f + esssup M g"
1.87  proof (cases "f \<in> borel_measurable M \<and> g \<in> borel_measurable M")
1.88    case True
1.89    then have [measurable]: "(\<lambda>x. f x + g x) \<in> borel_measurable M" by auto
1.90 @@ -181,14 +181,14 @@
1.91    then show ?thesis using esssup_I by auto
1.92  next
1.93    case False
1.94 -  then have "esssup M f + esssup M g = \<infinity>" unfolding esssup_def by auto
1.95 +  then have "esssup M f + esssup M g = \<infinity>" unfolding esssup_def top_ereal_def by auto
1.96    then show ?thesis by auto
1.97  qed
1.98
1.99  lemma esssup_zero_space:
1.100    assumes "emeasure M (space M) = 0"
1.101            "f \<in> borel_measurable M"
1.102 -  shows "esssup M f = - \<infinity>"
1.103 +  shows "esssup M f = (- \<infinity>::ereal)"
1.104  proof -
1.105    have "emeasure M {x \<in> space M. f x > - \<infinity>} = 0"
1.106      using assms(1) emeasure_mono emeasure_eq_0 by fastforce