author | hoelzl |
Thu, 20 Oct 2016 18:41:58 +0200 | |
changeset 64319 | a33bbac43359 |
parent 64293 | 256298544491 |
child 64333 | 692a1b317316 |
permissions | -rw-r--r-- |
64293 | 1 |
(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr |
2 |
License: BSD |
|
3 |
*) |
|
4 |
||
5 |
theory Essential_Supremum |
|
6 |
imports "../Analysis/Analysis" |
|
7 |
begin |
|
8 |
||
9 |
section {*The essential supremum*} |
|
10 |
||
11 |
text {*In this paragraph, we define the essential supremum and give its basic properties. The |
|
12 |
essential supremum of a function is its maximum value if one is allowed to throw away a set |
|
13 |
of measure $0$. It is convenient to define it to be infinity for non-measurable functions, as |
|
14 |
it allows for neater statements in general. This is a prerequisiste to define the space $L^\infty$.*} |
|
15 |
||
64319
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
16 |
definition esssup::"'a measure \<Rightarrow> ('a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology, complete_linorder}) \<Rightarrow> 'b" |
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
17 |
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)" |
64293 | 18 |
|
19 |
lemma esssup_zero_measure: |
|
20 |
"emeasure M {x \<in> space M. f x > esssup M f} = 0" |
|
64319
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
21 |
proof (cases "esssup M f = top") |
64293 | 22 |
case True |
23 |
then show ?thesis by auto |
|
24 |
next |
|
25 |
case False |
|
26 |
then have [measurable]: "f \<in> borel_measurable M" unfolding esssup_def by meson |
|
64319
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
27 |
have "esssup M f < top" using False by (auto simp: less_top) |
64293 | 28 |
have *: "{x \<in> space M. f x > z} \<in> null_sets M" if "z > esssup M f" for z |
29 |
proof - |
|
30 |
have "\<exists>w. w < z \<and> emeasure M {x \<in> space M. f x > w} = 0" |
|
31 |
using `z > esssup M f` unfolding esssup_def apply auto |
|
32 |
by (metis (mono_tags, lifting) Inf_less_iff mem_Collect_eq) |
|
33 |
then obtain w where "w < z" "emeasure M {x \<in> space M. f x > w} = 0" by auto |
|
34 |
then have a: "{x \<in> space M. f x > w} \<in> null_sets M" by auto |
|
35 |
have b: "{x \<in> space M. f x > z} \<subseteq> {x \<in> space M. f x > w}" using `w < z` by auto |
|
36 |
show ?thesis using null_sets_subset[OF a _ b] by simp |
|
37 |
qed |
|
64319
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
38 |
obtain u::"nat \<Rightarrow> 'b" where u: "\<And>n. u n > esssup M f" "u \<longlonglongrightarrow> esssup M f" |
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
39 |
using approx_from_above_dense_linorder[OF `esssup M f < top`] by auto |
64293 | 40 |
have "{x \<in> space M. f x > esssup M f} = (\<Union>n. {x \<in> space M. f x > u n})" |
41 |
using u apply auto |
|
42 |
apply (metis (mono_tags, lifting) order_tendsto_iff eventually_mono LIMSEQ_unique) |
|
43 |
using less_imp_le less_le_trans by blast |
|
44 |
also have "... \<in> null_sets M" |
|
45 |
using *[OF u(1)] by auto |
|
46 |
finally show ?thesis by auto |
|
47 |
qed |
|
48 |
||
49 |
lemma esssup_AE: |
|
50 |
"AE x in M. f x \<le> esssup M f" |
|
51 |
proof (cases "f \<in> borel_measurable M") |
|
52 |
case True |
|
53 |
show ?thesis |
|
54 |
apply (rule AE_I[OF _ esssup_zero_measure[of _ f]]) using True by auto |
|
55 |
next |
|
56 |
case False |
|
64319
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
57 |
then have "esssup M f = top" unfolding esssup_def by auto |
64293 | 58 |
then show ?thesis by auto |
59 |
qed |
|
60 |
||
61 |
lemma esssup_pos_measure: |
|
62 |
assumes "f \<in> borel_measurable M" "z < esssup M f" |
|
63 |
shows "emeasure M {x \<in> space M. f x > z} > 0" |
|
64 |
using assms Inf_less_iff mem_Collect_eq not_gr_zero unfolding esssup_def by force |
|
65 |
||
66 |
lemma esssup_non_measurable: |
|
67 |
assumes "f \<notin> borel_measurable M" |
|
64319
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
68 |
shows "esssup M f = top" |
64293 | 69 |
using assms unfolding esssup_def by auto |
70 |
||
71 |
lemma esssup_I [intro]: |
|
72 |
assumes "f \<in> borel_measurable M" "AE x in M. f x \<le> c" |
|
73 |
shows "esssup M f \<le> c" |
|
74 |
proof - |
|
75 |
have "emeasure M {x \<in> space M. \<not> f x \<le> c} = 0" |
|
76 |
apply (rule AE_E2[OF assms(2)]) using assms(1) by simp |
|
77 |
then have *: "emeasure M {x \<in> space M. f x > c} = 0" |
|
78 |
by (metis (mono_tags, lifting) Collect_cong not_less) |
|
79 |
show ?thesis unfolding esssup_def using assms apply simp by (rule Inf_lower, simp add: *) |
|
80 |
qed |
|
81 |
||
82 |
lemma esssup_AE_mono: |
|
83 |
assumes "f \<in> borel_measurable M" "AE x in M. f x \<le> g x" |
|
84 |
shows "esssup M f \<le> esssup M g" |
|
85 |
proof (cases "g \<in> borel_measurable M") |
|
86 |
case False |
|
87 |
then show ?thesis unfolding esssup_def by auto |
|
88 |
next |
|
89 |
case True |
|
90 |
have "AE x in M. f x \<le> esssup M g" |
|
91 |
using assms(2) esssup_AE[of g M] by auto |
|
92 |
then show ?thesis using esssup_I assms(1) by auto |
|
93 |
qed |
|
94 |
||
95 |
lemma esssup_mono: |
|
96 |
assumes "f \<in> borel_measurable M" "\<And>x. f x \<le> g x" |
|
97 |
shows "esssup M f \<le> esssup M g" |
|
98 |
apply (rule esssup_AE_mono) using assms by auto |
|
99 |
||
100 |
lemma esssup_AE_cong: |
|
101 |
assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" |
|
102 |
and "AE x in M. f x = g x" |
|
103 |
shows "esssup M f = esssup M g" |
|
104 |
proof - |
|
105 |
have "esssup M f \<le> esssup M g" |
|
106 |
using esssup_AE_mono[OF assms(1), of g] assms(3) by (simp add: eq_iff) |
|
107 |
moreover have "esssup M g \<le> esssup M f" |
|
108 |
using esssup_AE_mono[OF assms(2), of f] assms(3) by (simp add: eq_iff) |
|
109 |
ultimately show ?thesis by simp |
|
110 |
qed |
|
111 |
||
112 |
lemma esssup_const: |
|
113 |
assumes "emeasure M (space M) \<noteq> 0" |
|
114 |
shows "esssup M (\<lambda>x. c) = c" |
|
115 |
proof - |
|
116 |
have "emeasure M {x \<in> space M. (\<lambda>x. c) x > z} = (if c > z then emeasure M (space M) else 0)" for z |
|
117 |
by auto |
|
118 |
then have "{z. emeasure M {x \<in> space M. (\<lambda>x. c) x > z} = 0} = {c..}" using assms by auto |
|
119 |
then have "esssup M (\<lambda>x. c) = Inf {c..}" unfolding esssup_def by auto |
|
120 |
then show ?thesis by auto |
|
121 |
qed |
|
122 |
||
123 |
lemma esssup_cmult: |
|
124 |
assumes "c > (0::real)" |
|
64319
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
125 |
shows "esssup M (\<lambda>x. c * f x::ereal) = c * esssup M f" |
64293 | 126 |
proof (cases "f \<in> borel_measurable M") |
127 |
case True |
|
128 |
then have a [measurable]: "f \<in> borel_measurable M" by simp |
|
129 |
then have b [measurable]: "(\<lambda>x. c * f x) \<in> borel_measurable M" by simp |
|
130 |
have a: "{x \<in> space M. c * z < c * f x} = {x \<in> space M. z < f x}" for z::ereal |
|
131 |
by (meson assms ereal_less(2) ereal_mult_left_mono ereal_mult_strict_left_mono less_ereal.simps(4) less_imp_le not_less) |
|
132 |
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}" |
|
133 |
proof (auto) |
|
134 |
fix y assume *: "emeasure M {x \<in> space M. y < c * f x} = 0" |
|
135 |
define z where "z = y / c" |
|
136 |
have **: "y = c * z" unfolding z_def using assms by (simp add: ereal_mult_divide) |
|
137 |
then have "y = c * z \<and> emeasure M {x \<in> space M. z < f x} = 0" |
|
138 |
using * unfolding ** unfolding a by auto |
|
139 |
then show "\<exists>z. y = ereal c * z \<and> emeasure M {x \<in> space M. z < f x} = 0" |
|
140 |
by auto |
|
141 |
next |
|
142 |
fix z assume *: "emeasure M {x \<in> space M. z < f x} = 0" |
|
143 |
then show "emeasure M {x \<in> space M. c * z < c * f x} = 0" |
|
144 |
using a by auto |
|
145 |
qed |
|
146 |
have "esssup M (\<lambda>x. c * f x) = Inf {z::ereal. emeasure M {x \<in> space M. c * f x > z} = 0}" |
|
147 |
unfolding esssup_def using b by auto |
|
148 |
also have "... = Inf {c * z| z::ereal. emeasure M {x \<in> space M. f x > z} = 0}" |
|
149 |
using * by auto |
|
150 |
also have "... = ereal c * Inf {z. emeasure M {x \<in> space M. f x > z} = 0}" |
|
151 |
apply (rule ereal_Inf_cmult) using assms by auto |
|
152 |
also have "... = c * esssup M f" |
|
153 |
unfolding esssup_def by auto |
|
154 |
finally show ?thesis by simp |
|
155 |
next |
|
156 |
case False |
|
64319
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
157 |
have "esssup M f = top" using False unfolding esssup_def by auto |
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
158 |
then have *: "c * esssup M f = \<infinity>" using assms by (simp add: ennreal_mult_eq_top_iff top_ereal_def) |
64293 | 159 |
have "(\<lambda>x. c * f x) \<notin> borel_measurable M" |
160 |
proof (rule ccontr) |
|
161 |
assume "\<not> (\<lambda>x. c * f x) \<notin> borel_measurable M" |
|
162 |
then have [measurable]: "(\<lambda>x. c * f x) \<in> borel_measurable M" by simp |
|
163 |
then have "(\<lambda>x. (1/c) * (c * f x)) \<in> borel_measurable M" by measurable |
|
164 |
moreover have "(1/c) * (c * f x) = f x" for x |
|
165 |
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) |
|
166 |
ultimately show False using False by auto |
|
167 |
qed |
|
64319
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
168 |
then have "esssup M (\<lambda>x. c * f x) = \<infinity>" unfolding esssup_def by (simp add: top_ereal_def) |
64293 | 169 |
then show ?thesis using * by auto |
170 |
qed |
|
171 |
||
172 |
lemma esssup_add: |
|
64319
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
173 |
"esssup M (\<lambda>x. f x + g x::ereal) \<le> esssup M f + esssup M g" |
64293 | 174 |
proof (cases "f \<in> borel_measurable M \<and> g \<in> borel_measurable M") |
175 |
case True |
|
176 |
then have [measurable]: "(\<lambda>x. f x + g x) \<in> borel_measurable M" by auto |
|
177 |
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 |
|
178 |
using that ereal_add_mono by auto |
|
179 |
then have "AE x in M. f x + g x \<le> esssup M f + esssup M g" |
|
180 |
using esssup_AE[of f M] esssup_AE[of g M] by auto |
|
181 |
then show ?thesis using esssup_I by auto |
|
182 |
next |
|
183 |
case False |
|
64319
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
184 |
then have "esssup M f + esssup M g = \<infinity>" unfolding esssup_def top_ereal_def by auto |
64293 | 185 |
then show ?thesis by auto |
186 |
qed |
|
187 |
||
188 |
lemma esssup_zero_space: |
|
189 |
assumes "emeasure M (space M) = 0" |
|
190 |
"f \<in> borel_measurable M" |
|
64319
a33bbac43359
HOL-Probability: generalize type of essential supremum
hoelzl
parents:
64293
diff
changeset
|
191 |
shows "esssup M f = (- \<infinity>::ereal)" |
64293 | 192 |
proof - |
193 |
have "emeasure M {x \<in> space M. f x > - \<infinity>} = 0" |
|
194 |
using assms(1) emeasure_mono emeasure_eq_0 by fastforce |
|
195 |
then show ?thesis unfolding esssup_def using assms(2) Inf_eq_MInfty by auto |
|
196 |
qed |
|
197 |
||
198 |
end |
|
199 |