# HG changeset patch
# User hoelzl
# Date 1477040556 -7200
# Node ID 692a1b317316400fefef68ccc79d8335866cf562
# Parent  76a3e0f894fd27b6a79bbd0313f90f628468482f
HOL-Probability: Essential Supremum as Limsup over ae_filter

diff -r 76a3e0f894fd -r 692a1b317316 src/HOL/Probability/Essential_Supremum.thy
--- a/src/HOL/Probability/Essential_Supremum.thy	Fri Oct 21 11:45:35 2016 +0200
+++ b/src/HOL/Probability/Essential_Supremum.thy	Fri Oct 21 11:02:36 2016 +0200
@@ -1,4 +1,5 @@
 (*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
+    Author:  Johannes Hölzl (TUM) -- ported to Limsup
     License: BSD
 *)
 
@@ -6,6 +7,9 @@
 imports "../Analysis/Analysis"
 begin
 
+lemma ae_filter_eq_bot_iff: "ae_filter M = bot \<longleftrightarrow> emeasure M (space M) = 0"
+  by (simp add: AE_iff_measurable trivial_limit_def)
+
 section {*The essential supremum*}
 
 text {*In this paragraph, we define the essential supremum and give its basic properties. The
@@ -14,7 +18,31 @@
 it allows for neater statements in general. This is a prerequisiste to define the space $L^\infty$.*}
 
 definition esssup::"'a measure \<Rightarrow> ('a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology, complete_linorder}) \<Rightarrow> 'b"
-  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)"
+  where "esssup M f = (if f \<in> borel_measurable M then Limsup (ae_filter M) f else top)"
+
+lemma esssup_non_measurable: "f \<notin> M \<rightarrow>\<^sub>M borel \<Longrightarrow> esssup M f = top"
+  by (simp add: esssup_def)
+
+lemma esssup_eq_AE:
+  assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" shows "esssup M f = Inf {z. AE x in M. f x \<le> z}"
+  unfolding esssup_def if_P[OF f] Limsup_def
+proof (intro antisym INF_greatest Inf_greatest; clarsimp)
+  fix y assume "AE x in M. f x \<le> y"
+  then have "(\<lambda>x. f x \<le> y) \<in> {P. AE x in M. P x}"
+    by simp
+  then show "(INF P:{P. AE x in M. P x}. SUP x:Collect P. f x) \<le> y"
+    by (rule INF_lower2) (auto intro: SUP_least)
+next
+  fix P assume P: "AE x in M. P x"
+  show "Inf {z. AE x in M. f x \<le> z} \<le> (SUP x:Collect P. f x)"
+  proof (rule Inf_lower; clarsimp)
+    show "AE x in M. f x \<le> (SUP x:Collect P. f x)"
+      using P by (auto elim: eventually_mono simp: SUP_upper)
+  qed
+qed
+
+lemma esssup_eq: "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> esssup M f = Inf {z. emeasure M {x \<in> space M. f x > z} = 0}"
+  by (auto simp add: esssup_eq_AE not_less[symmetric] AE_iff_measurable[OF _ refl] intro!: arg_cong[where f=Inf])
 
 lemma esssup_zero_measure:
   "emeasure M {x \<in> space M. f x > esssup M f} = 0"
@@ -23,13 +51,12 @@
   then show ?thesis by auto
 next
   case False
-  then have [measurable]: "f \<in> borel_measurable M" unfolding esssup_def by meson
+  then have f[measurable]: "f \<in> M \<rightarrow>\<^sub>M borel" unfolding esssup_def by meson
   have "esssup M f < top" using False by (auto simp: less_top)
   have *: "{x \<in> space M. f x > z} \<in> null_sets M" if "z > esssup M f" for z
   proof -
     have "\<exists>w. w < z \<and> emeasure M {x \<in> space M. f x > w} = 0"
-      using `z > esssup M f` unfolding esssup_def apply auto
-      by (metis (mono_tags, lifting) Inf_less_iff mem_Collect_eq)
+      using `z > esssup M f` f by (auto simp: esssup_eq Inf_less_iff)
     then obtain w where "w < z" "emeasure M {x \<in> space M. f x > w} = 0" by auto
     then have a: "{x \<in> space M. f x > w} \<in> null_sets M" by auto
     have b: "{x \<in> space M. f x > z} \<subseteq> {x \<in> space M. f x > w}" using `w < z` by auto
@@ -46,127 +73,44 @@
   finally show ?thesis by auto
 qed
 
-lemma esssup_AE:
-  "AE x in M. f x \<le> esssup M f"
-proof (cases "f \<in> borel_measurable M")
-  case True
-  show ?thesis
-    apply (rule AE_I[OF _ esssup_zero_measure[of _ f]]) using True by auto
-next
-  case False
-  then have "esssup M f = top" unfolding esssup_def by auto
-  then show ?thesis by auto
-qed
+lemma esssup_AE: "AE x in M. f x \<le> esssup M f"
+proof (cases "f \<in> M \<rightarrow>\<^sub>M borel")
+  case True then show ?thesis
+    by (intro AE_I[OF _ esssup_zero_measure[of _ f]]) auto
+qed (simp add: esssup_non_measurable)
 
 lemma esssup_pos_measure:
-  assumes "f \<in> borel_measurable M" "z < esssup M f"
-  shows "emeasure M {x \<in> space M. f x > z} > 0"
-using assms Inf_less_iff mem_Collect_eq not_gr_zero unfolding esssup_def by force
+  "f \<in> borel_measurable M \<Longrightarrow> z < esssup M f \<Longrightarrow> emeasure M {x \<in> space M. f x > z} > 0"
+  using Inf_less_iff mem_Collect_eq not_gr_zero by (force simp: esssup_eq)
 
-lemma esssup_non_measurable:
-  assumes "f \<notin> borel_measurable M"
-  shows "esssup M f = top"
-using assms unfolding esssup_def by auto
+lemma esssup_I [intro]: "f \<in> borel_measurable M \<Longrightarrow> AE x in M. f x \<le> c \<Longrightarrow> esssup M f \<le> c"
+  unfolding esssup_def by (simp add: Limsup_bounded)
 
-lemma esssup_I [intro]:
-  assumes "f \<in> borel_measurable M" "AE x in M. f x \<le> c"
-  shows "esssup M f \<le> c"
-proof -
-  have "emeasure M {x \<in> space M. \<not> f x \<le> c} = 0"
-    apply (rule AE_E2[OF assms(2)]) using assms(1) by simp
-  then have *: "emeasure M {x \<in> space M. f x > c} = 0"
-    by (metis (mono_tags, lifting) Collect_cong not_less)
-  show ?thesis unfolding esssup_def using assms apply simp by (rule Inf_lower, simp add: *)
-qed
+lemma esssup_AE_mono: "f \<in> borel_measurable M \<Longrightarrow> AE x in M. f x \<le> g x \<Longrightarrow> esssup M f \<le> esssup M g"
+  by (auto simp: esssup_def Limsup_mono)
 
-lemma esssup_AE_mono:
-  assumes "f \<in> borel_measurable M" "AE x in M. f x \<le> g x"
-  shows "esssup M f \<le> esssup M g"
-proof (cases "g \<in> borel_measurable M")
-  case False
-  then show ?thesis unfolding esssup_def by auto
-next
-  case True
-  have "AE x in M. f x \<le> esssup M g"
-    using assms(2) esssup_AE[of g M] by auto
-  then show ?thesis using esssup_I assms(1) by auto
-qed
-
-lemma esssup_mono:
-  assumes "f \<in> borel_measurable M" "\<And>x. f x \<le> g x"
-  shows "esssup M f \<le> esssup M g"
-apply (rule esssup_AE_mono) using assms by auto
+lemma esssup_mono: "f \<in> borel_measurable M \<Longrightarrow> (\<And>x. f x \<le> g x) \<Longrightarrow> esssup M f \<le> esssup M g"
+  by (rule esssup_AE_mono) auto
 
 lemma esssup_AE_cong:
-  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
-      and "AE x in M. f x = g x"
-  shows "esssup M f = esssup M g"
-proof -
-  have "esssup M f \<le> esssup M g"
-    using esssup_AE_mono[OF assms(1), of g] assms(3) by (simp add: eq_iff)
-  moreover have "esssup M g \<le> esssup M f"
-    using esssup_AE_mono[OF assms(2), of f] assms(3) by (simp add: eq_iff)
-  ultimately show ?thesis by simp
-qed
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow> esssup M f = esssup M g"
+  by (auto simp: esssup_def intro!: Limsup_eq)
 
-lemma esssup_const:
-  assumes "emeasure M (space M) \<noteq> 0"
-  shows "esssup M (\<lambda>x. c) = c"
-proof -
-  have "emeasure M {x \<in> space M. (\<lambda>x. c) x > z} = (if c > z then emeasure M (space M) else 0)" for z
-    by auto
-  then have "{z. emeasure M {x \<in> space M. (\<lambda>x. c) x > z} = 0} = {c..}" using assms by auto
-  then have "esssup M (\<lambda>x. c) = Inf {c..}" unfolding esssup_def by auto
-  then show ?thesis by auto
-qed
+lemma esssup_const: "emeasure M (space M) \<noteq> 0 \<Longrightarrow> esssup M (\<lambda>x. c) = c"
+  by (simp add: esssup_def Limsup_const ae_filter_eq_bot_iff)
 
-lemma esssup_cmult:
-  assumes "c > (0::real)"
-  shows "esssup M (\<lambda>x. c * f x::ereal) = c * esssup M f"
-proof (cases "f \<in> borel_measurable M")
-  case True
-  then have a [measurable]: "f \<in> borel_measurable M" by simp
-  then have b [measurable]: "(\<lambda>x. c * f x) \<in> borel_measurable M" by simp
-  have a: "{x \<in> space M. c * z < c * f x} = {x \<in> space M. z < f x}" for z::ereal
-    by (meson assms ereal_less(2) ereal_mult_left_mono ereal_mult_strict_left_mono less_ereal.simps(4) less_imp_le not_less)
-  have *: "{z::ereal. emeasure M {x \<in> space M. ereal c * f x > z} = 0} = {c * z| z::ereal. emeasure M {x \<in> space M. f x > z} = 0}"
-  proof (auto)
-    fix y assume *: "emeasure M {x \<in> space M. y < c * f x} = 0"
-    define z where "z = y / c"
-    have **: "y = c * z" unfolding z_def using assms by (simp add: ereal_mult_divide)
-    then have "y = c * z \<and> emeasure M {x \<in> space M. z < f x} = 0"
-      using * unfolding ** unfolding a by auto
-    then show "\<exists>z. y = ereal c * z \<and> emeasure M {x \<in> space M. z < f x} = 0"
-      by auto
-  next
-    fix z assume *: "emeasure M {x \<in> space M. z < f x} = 0"
-    then show "emeasure M {x \<in> space M. c * z < c * f x} = 0"
-        using a by auto
-  qed
-  have "esssup M (\<lambda>x. c * f x) = Inf {z::ereal. emeasure M {x \<in> space M. c * f x > z} = 0}"
-    unfolding esssup_def using b by auto
-  also have "... = Inf {c * z| z::ereal. emeasure M {x \<in> space M. f x > z} = 0}"
-    using * by auto
-  also have "... = ereal c * Inf {z. emeasure M {x \<in> space M. f x > z} = 0}"
-    apply (rule ereal_Inf_cmult) using assms by auto
-  also have "... = c * esssup M f"
-    unfolding esssup_def by auto
-  finally show ?thesis by simp
-next
-  case False
-  have "esssup M f = top" using False unfolding esssup_def by auto
-  then have *: "c * esssup M f = \<infinity>" using assms by (simp add: ennreal_mult_eq_top_iff top_ereal_def)
-  have "(\<lambda>x. c * f x) \<notin> borel_measurable M"
-  proof (rule ccontr)
-    assume "\<not> (\<lambda>x. c * f x) \<notin> borel_measurable M"
-    then have [measurable]: "(\<lambda>x. c * f x) \<in> borel_measurable M" by simp
-    then have "(\<lambda>x. (1/c) * (c * f x)) \<in> borel_measurable M" by measurable
-    moreover have "(1/c) * (c * f x) = f x" for x
-      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)
-    ultimately show False using False by auto
-  qed
-  then have "esssup M (\<lambda>x. c * f x) = \<infinity>" unfolding esssup_def by (simp add: top_ereal_def)
-  then show ?thesis using * by auto
+lemma esssup_cmult: assumes "c > (0::real)" shows "esssup M (\<lambda>x. c * f x::ereal) = c * esssup M f"
+proof -
+  have "(\<lambda>x. ereal c * f x) \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> f \<in> M \<rightarrow>\<^sub>M borel"
+  proof (subst measurable_cong)
+    fix \<omega> show "f \<omega> = ereal (1/c) * (ereal c * f \<omega>)"
+      using \<open>0 < c\<close> by (cases "f \<omega>") auto
+  qed auto
+  then have "(\<lambda>x. ereal c * f x) \<in> M \<rightarrow>\<^sub>M borel \<longleftrightarrow> f \<in> M \<rightarrow>\<^sub>M borel"
+    by(safe intro!: borel_measurable_ereal_times borel_measurable_const)
+  with \<open>0<c\<close> show ?thesis
+    by (cases "ae_filter M = bot")
+       (auto simp: esssup_def bot_ereal_def top_ereal_def Limsup_ereal_mult_left)
 qed
 
 lemma esssup_add:
@@ -186,14 +130,8 @@
 qed
 
 lemma esssup_zero_space:
-  assumes "emeasure M (space M) = 0"
-          "f \<in> borel_measurable M"
-  shows "esssup M f = (- \<infinity>::ereal)"
-proof -
-  have "emeasure M {x \<in> space M. f x > - \<infinity>} = 0"
-    using assms(1) emeasure_mono emeasure_eq_0 by fastforce
-  then show ?thesis unfolding esssup_def using assms(2) Inf_eq_MInfty by auto
-qed
+  "emeasure M (space M) = 0 \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> esssup M f = (- \<infinity>::ereal)"
+  by (simp add: esssup_def ae_filter_eq_bot_iff[symmetric] bot_ereal_def)
 
 end