1(* Author: S��bastien Gou��zel sebastien.gouezel@univ-rennes1.fr 2 Author: Johannes H��lzl (TUM) -- ported to Limsup 3 License: BSD 4*) 5 6theory Essential_Supremum 7imports "HOL-Analysis.Analysis" 8begin 9 10lemma ae_filter_eq_bot_iff: "ae_filter M = bot \<longleftrightarrow> emeasure M (space M) = 0" 11 by (simp add: AE_iff_measurable trivial_limit_def) 12 13section \<open>The essential supremum\<close> 14 15text \<open>In this paragraph, we define the essential supremum and give its basic properties. The 16essential supremum of a function is its maximum value if one is allowed to throw away a set 17of measure $0$. It is convenient to define it to be infinity for non-measurable functions, as 18it allows for neater statements in general. This is a prerequisiste to define the space $L^\infty$.\<close> 19 20definition esssup::"'a measure \<Rightarrow> ('a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology, complete_linorder}) \<Rightarrow> 'b" 21 where "esssup M f = (if f \<in> borel_measurable M then Limsup (ae_filter M) f else top)" 22 23lemma esssup_non_measurable: "f \<notin> M \<rightarrow>\<^sub>M borel \<Longrightarrow> esssup M f = top" 24 by (simp add: esssup_def) 25 26lemma esssup_eq_AE: 27 assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" shows "esssup M f = Inf {z. AE x in M. f x \<le> z}" 28 unfolding esssup_def if_P[OF f] Limsup_def 29proof (intro antisym INF_greatest Inf_greatest; clarsimp) 30 fix y assume "AE x in M. f x \<le> y" 31 then have "(\<lambda>x. f x \<le> y) \<in> {P. AE x in M. P x}" 32 by simp 33 then show "(INF P\<in>{P. AE x in M. P x}. SUP x\<in>Collect P. f x) \<le> y" 34 by (rule INF_lower2) (auto intro: SUP_least) 35next 36 fix P assume P: "AE x in M. P x" 37 show "Inf {z. AE x in M. f x \<le> z} \<le> (SUP x\<in>Collect P. f x)" 38 proof (rule Inf_lower; clarsimp) 39 show "AE x in M. f x \<le> (SUP x\<in>Collect P. f x)" 40 using P by (auto elim: eventually_mono simp: SUP_upper) 41 qed 42qed 43 44lemma 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}" 45 by (auto simp add: esssup_eq_AE not_less[symmetric] AE_iff_measurable[OF _ refl] intro!: arg_cong[where f=Inf]) 46 47lemma esssup_zero_measure: 48 "emeasure M {x \<in> space M. f x > esssup M f} = 0" 49proof (cases "esssup M f = top") 50 case True 51 then show ?thesis by auto 52next 53 case False 54 then have f[measurable]: "f \<in> M \<rightarrow>\<^sub>M borel" unfolding esssup_def by meson 55 have "esssup M f < top" using False by (auto simp: less_top) 56 have *: "{x \<in> space M. f x > z} \<in> null_sets M" if "z > esssup M f" for z 57 proof - 58 have "\<exists>w. w < z \<and> emeasure M {x \<in> space M. f x > w} = 0" 59 using \<open>z > esssup M f\<close> f by (auto simp: esssup_eq Inf_less_iff) 60 then obtain w where "w < z" "emeasure M {x \<in> space M. f x > w} = 0" by auto 61 then have a: "{x \<in> space M. f x > w} \<in> null_sets M" by auto 62 have b: "{x \<in> space M. f x > z} \<subseteq> {x \<in> space M. f x > w}" using \<open>w < z\<close> by auto 63 show ?thesis using null_sets_subset[OF a _ b] by simp 64 qed 65 obtain u::"nat \<Rightarrow> 'b" where u: "\<And>n. u n > esssup M f" "u \<longlonglongrightarrow> esssup M f" 66 using approx_from_above_dense_linorder[OF \<open>esssup M f < top\<close>] by auto 67 have "{x \<in> space M. f x > esssup M f} = (\<Union>n. {x \<in> space M. f x > u n})" 68 using u apply auto 69 apply (metis (mono_tags, lifting) order_tendsto_iff eventually_mono LIMSEQ_unique) 70 using less_imp_le less_le_trans by blast 71 also have "... \<in> null_sets M" 72 using *[OF u(1)] by auto 73 finally show ?thesis by auto 74qed 75 76lemma esssup_AE: "AE x in M. f x \<le> esssup M f" 77proof (cases "f \<in> M \<rightarrow>\<^sub>M borel") 78 case True then show ?thesis 79 by (intro AE_I[OF _ esssup_zero_measure[of _ f]]) auto 80qed (simp add: esssup_non_measurable) 81 82lemma esssup_pos_measure: 83 "f \<in> borel_measurable M \<Longrightarrow> z < esssup M f \<Longrightarrow> emeasure M {x \<in> space M. f x > z} > 0" 84 using Inf_less_iff mem_Collect_eq not_gr_zero by (force simp: esssup_eq) 85 86lemma esssup_I [intro]: "f \<in> borel_measurable M \<Longrightarrow> AE x in M. f x \<le> c \<Longrightarrow> esssup M f \<le> c" 87 unfolding esssup_def by (simp add: Limsup_bounded) 88 89lemma 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" 90 by (auto simp: esssup_def Limsup_mono) 91 92lemma esssup_mono: "f \<in> borel_measurable M \<Longrightarrow> (\<And>x. f x \<le> g x) \<Longrightarrow> esssup M f \<le> esssup M g" 93 by (rule esssup_AE_mono) auto 94 95lemma esssup_AE_cong: 96 "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" 97 by (auto simp: esssup_def intro!: Limsup_eq) 98 99lemma esssup_const: "emeasure M (space M) \<noteq> 0 \<Longrightarrow> esssup M (\<lambda>x. c) = c" 100 by (simp add: esssup_def Limsup_const ae_filter_eq_bot_iff) 101 102lemma esssup_cmult: assumes "c > (0::real)" shows "esssup M (\<lambda>x. c * f x::ereal) = c * esssup M f" 103proof - 104 have "(\<lambda>x. ereal c * f x) \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> f \<in> M \<rightarrow>\<^sub>M borel" 105 proof (subst measurable_cong) 106 fix \<omega> show "f \<omega> = ereal (1/c) * (ereal c * f \<omega>)" 107 using \<open>0 < c\<close> by (cases "f \<omega>") auto 108 qed auto 109 then have "(\<lambda>x. ereal c * f x) \<in> M \<rightarrow>\<^sub>M borel \<longleftrightarrow> f \<in> M \<rightarrow>\<^sub>M borel" 110 by(safe intro!: borel_measurable_ereal_times borel_measurable_const) 111 with \<open>0<c\<close> show ?thesis 112 by (cases "ae_filter M = bot") 113 (auto simp: esssup_def bot_ereal_def top_ereal_def Limsup_ereal_mult_left) 114qed 115 116lemma esssup_add: 117 "esssup M (\<lambda>x. f x + g x::ereal) \<le> esssup M f + esssup M g" 118proof (cases "f \<in> borel_measurable M \<and> g \<in> borel_measurable M") 119 case True 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 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" 124 using esssup_AE[of f M] esssup_AE[of g M] by auto 125 then show ?thesis using esssup_I by auto 126next 127 case False 128 then have "esssup M f + esssup M g = \<infinity>" unfolding esssup_def top_ereal_def by auto 129 then show ?thesis by auto 130qed 131 132lemma esssup_zero_space: 133 "emeasure M (space M) = 0 \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> esssup M f = (- \<infinity>::ereal)" 134 by (simp add: esssup_def ae_filter_eq_bot_iff[symmetric] bot_ereal_def) 135 136end 137 138