HOL-Probability: generalize type of essential supremum
authorhoelzl
Thu Oct 20 18:41:58 2016 +0200 (2016-10-20)
changeset 64319a33bbac43359
parent 64318 1e92b5c35615
child 64320 ba194424b895
HOL-Probability: generalize type of essential supremum
src/HOL/Probability/Essential_Supremum.thy
     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.84  lemma esssup_add:
    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