author  nipkow 
Wed, 11 Jul 2018 11:16:26 +0200  
changeset 68751  640386ab99f3 
parent 67226  ec32cdaab97b 
child 69260  0a9688695a1b 
permissions  rwrr 
64293  1 
(* Author: Sébastien Gouëzel sebastien.gouezel@univrennes1.fr 
64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

2 
Author: Johannes Hölzl (TUM)  ported to Limsup 
64293  3 
License: BSD 
4 
*) 

5 

6 
theory Essential_Supremum 

66453
cc19f7ca2ed6
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
64333
diff
changeset

7 
imports "HOLAnalysis.Analysis" 
64293  8 
begin 
9 

64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

10 
lemma ae_filter_eq_bot_iff: "ae_filter M = bot \<longleftrightarrow> emeasure M (space M) = 0" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

11 
by (simp add: AE_iff_measurable trivial_limit_def) 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

12 

67226  13 
section \<open>The essential supremum\<close> 
64293  14 

67226  15 
text \<open>In this paragraph, we define the essential supremum and give its basic properties. The 
64293  16 
essential supremum of a function is its maximum value if one is allowed to throw away a set 
17 
of measure $0$. It is convenient to define it to be infinity for nonmeasurable functions, as 

67226  18 
it allows for neater statements in general. This is a prerequisiste to define the space $L^\infty$.\<close> 
64293  19 

64319
a33bbac43359
HOLProbability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset

20 
definition esssup::"'a measure \<Rightarrow> ('a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology, complete_linorder}) \<Rightarrow> 'b" 
64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

21 
where "esssup M f = (if f \<in> borel_measurable M then Limsup (ae_filter M) f else top)" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

22 

692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

23 
lemma esssup_non_measurable: "f \<notin> M \<rightarrow>\<^sub>M borel \<Longrightarrow> esssup M f = top" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

24 
by (simp add: esssup_def) 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

25 

692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

26 
lemma esssup_eq_AE: 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

27 
assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" shows "esssup M f = Inf {z. AE x in M. f x \<le> z}" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

28 
unfolding esssup_def if_P[OF f] Limsup_def 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

29 
proof (intro antisym INF_greatest Inf_greatest; clarsimp) 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

30 
fix y assume "AE x in M. f x \<le> y" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

31 
then have "(\<lambda>x. f x \<le> y) \<in> {P. AE x in M. P x}" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

32 
by simp 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

33 
then show "(INF P:{P. AE x in M. P x}. SUP x:Collect P. f x) \<le> y" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

34 
by (rule INF_lower2) (auto intro: SUP_least) 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

35 
next 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

36 
fix P assume P: "AE x in M. P x" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

37 
show "Inf {z. AE x in M. f x \<le> z} \<le> (SUP x:Collect P. f x)" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

38 
proof (rule Inf_lower; clarsimp) 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

39 
show "AE x in M. f x \<le> (SUP x:Collect P. f x)" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

40 
using P by (auto elim: eventually_mono simp: SUP_upper) 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

41 
qed 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

42 
qed 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

43 

692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

44 
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}" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

45 
by (auto simp add: esssup_eq_AE not_less[symmetric] AE_iff_measurable[OF _ refl] intro!: arg_cong[where f=Inf]) 
64293  46 

47 
lemma esssup_zero_measure: 

48 
"emeasure M {x \<in> space M. f x > esssup M f} = 0" 

64319
a33bbac43359
HOLProbability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset

49 
proof (cases "esssup M f = top") 
64293  50 
case True 
51 
then show ?thesis by auto 

52 
next 

53 
case False 

64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

54 
then have f[measurable]: "f \<in> M \<rightarrow>\<^sub>M borel" unfolding esssup_def by meson 
64319
a33bbac43359
HOLProbability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset

55 
have "esssup M f < top" using False by (auto simp: less_top) 
64293  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" 

67226  59 
using \<open>z > esssup M f\<close> f by (auto simp: esssup_eq Inf_less_iff) 
64293  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 

67226  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 
64293  63 
show ?thesis using null_sets_subset[OF a _ b] by simp 
64 
qed 

64319
a33bbac43359
HOLProbability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset

65 
obtain u::"nat \<Rightarrow> 'b" where u: "\<And>n. u n > esssup M f" "u \<longlonglongrightarrow> esssup M f" 
67226  66 
using approx_from_above_dense_linorder[OF \<open>esssup M f < top\<close>] by auto 
64293  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 

74 
qed 

75 

64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

76 
lemma esssup_AE: "AE x in M. f x \<le> esssup M f" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

77 
proof (cases "f \<in> M \<rightarrow>\<^sub>M borel") 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

78 
case True then show ?thesis 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

79 
by (intro AE_I[OF _ esssup_zero_measure[of _ f]]) auto 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

80 
qed (simp add: esssup_non_measurable) 
64293  81 

82 
lemma esssup_pos_measure: 

64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

83 
"f \<in> borel_measurable M \<Longrightarrow> z < esssup M f \<Longrightarrow> emeasure M {x \<in> space M. f x > z} > 0" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

84 
using Inf_less_iff mem_Collect_eq not_gr_zero by (force simp: esssup_eq) 
64293  85 

64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

86 
lemma esssup_I [intro]: "f \<in> borel_measurable M \<Longrightarrow> AE x in M. f x \<le> c \<Longrightarrow> esssup M f \<le> c" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

87 
unfolding esssup_def by (simp add: Limsup_bounded) 
64293  88 

64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

89 
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" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

90 
by (auto simp: esssup_def Limsup_mono) 
64293  91 

64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

92 
lemma esssup_mono: "f \<in> borel_measurable M \<Longrightarrow> (\<And>x. f x \<le> g x) \<Longrightarrow> esssup M f \<le> esssup M g" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

93 
by (rule esssup_AE_mono) auto 
64293  94 

95 
lemma esssup_AE_cong: 

64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

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" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

97 
by (auto simp: esssup_def intro!: Limsup_eq) 
64293  98 

64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

99 
lemma esssup_const: "emeasure M (space M) \<noteq> 0 \<Longrightarrow> esssup M (\<lambda>x. c) = c" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

100 
by (simp add: esssup_def Limsup_const ae_filter_eq_bot_iff) 
64293  101 

64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

102 
lemma esssup_cmult: assumes "c > (0::real)" shows "esssup M (\<lambda>x. c * f x::ereal) = c * esssup M f" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

103 
proof  
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

104 
have "(\<lambda>x. ereal c * f x) \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> f \<in> M \<rightarrow>\<^sub>M borel" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

105 
proof (subst measurable_cong) 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

106 
fix \<omega> show "f \<omega> = ereal (1/c) * (ereal c * f \<omega>)" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

107 
using \<open>0 < c\<close> by (cases "f \<omega>") auto 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

108 
qed auto 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

109 
then have "(\<lambda>x. ereal c * f x) \<in> M \<rightarrow>\<^sub>M borel \<longleftrightarrow> f \<in> M \<rightarrow>\<^sub>M borel" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

110 
by(safe intro!: borel_measurable_ereal_times borel_measurable_const) 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

111 
with \<open>0<c\<close> show ?thesis 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

112 
by (cases "ae_filter M = bot") 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

113 
(auto simp: esssup_def bot_ereal_def top_ereal_def Limsup_ereal_mult_left) 
64293  114 
qed 
115 

116 
lemma esssup_add: 

64319
a33bbac43359
HOLProbability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset

117 
"esssup M (\<lambda>x. f x + g x::ereal) \<le> esssup M f + esssup M g" 
64293  118 
proof (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 

68751  122 
using that add_mono by auto 
64293  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 

126 
next 

127 
case False 

64319
a33bbac43359
HOLProbability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset

128 
then have "esssup M f + esssup M g = \<infinity>" unfolding esssup_def top_ereal_def by auto 
64293  129 
then show ?thesis by auto 
130 
qed 

131 

132 
lemma esssup_zero_space: 

64333
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

133 
"emeasure M (space M) = 0 \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> esssup M f = ( \<infinity>::ereal)" 
692a1b317316
HOLProbability: Essential Supremum as Limsup over ae_filter
hoelzl
parents:
64319
diff
changeset

134 
by (simp add: esssup_def ae_filter_eq_bot_iff[symmetric] bot_ereal_def) 
64293  135 

136 
end 

137 