38656
|
1 |
theory Euclidean_Lebesgue
|
|
2 |
imports Lebesgue_Integration Lebesgue_Measure
|
|
3 |
begin
|
|
4 |
|
|
5 |
lemma simple_function_has_integral:
|
|
6 |
fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
|
|
7 |
assumes f:"lebesgue.simple_function f"
|
|
8 |
and f':"\<forall>x. f x \<noteq> \<omega>"
|
|
9 |
and om:"\<forall>x\<in>range f. lmeasure (f -` {x} \<inter> UNIV) = \<omega> \<longrightarrow> x = 0"
|
|
10 |
shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.simple_integral f))) UNIV"
|
|
11 |
unfolding lebesgue.simple_integral_def
|
|
12 |
apply(subst lebesgue_simple_function_indicator[OF f])
|
|
13 |
proof- case goal1
|
|
14 |
have *:"\<And>x. \<forall>y\<in>range f. y * indicator (f -` {y}) x \<noteq> \<omega>"
|
|
15 |
"\<forall>x\<in>range f. x * lmeasure (f -` {x} \<inter> UNIV) \<noteq> \<omega>"
|
|
16 |
using f' om unfolding indicator_def by auto
|
|
17 |
show ?case unfolding space_lebesgue_space real_of_pinfreal_setsum'[OF *(1),THEN sym]
|
|
18 |
unfolding real_of_pinfreal_setsum'[OF *(2),THEN sym]
|
|
19 |
unfolding real_of_pinfreal_setsum space_lebesgue_space
|
|
20 |
apply(rule has_integral_setsum)
|
|
21 |
proof safe show "finite (range f)" using f by (auto dest: lebesgue.simple_functionD)
|
|
22 |
fix y::'a show "((\<lambda>x. real (f y * indicator (f -` {f y}) x)) has_integral
|
|
23 |
real (f y * lmeasure (f -` {f y} \<inter> UNIV))) UNIV"
|
|
24 |
proof(cases "f y = 0") case False
|
|
25 |
have mea:"gmeasurable (f -` {f y})" apply(rule glmeasurable_finite)
|
|
26 |
using assms unfolding lebesgue.simple_function_def using False by auto
|
|
27 |
have *:"\<And>x. real (indicator (f -` {f y}) x::pinfreal) = (if x \<in> f -` {f y} then 1 else 0)" by auto
|
|
28 |
show ?thesis unfolding real_of_pinfreal_mult[THEN sym]
|
|
29 |
apply(rule has_integral_cmul[where 'b=real, unfolded real_scaleR_def])
|
|
30 |
unfolding Int_UNIV_right lmeasure_gmeasure[OF mea,THEN sym]
|
|
31 |
unfolding measure_integral_univ[OF mea] * apply(rule integrable_integral)
|
|
32 |
unfolding gmeasurable_integrable[THEN sym] using mea .
|
|
33 |
qed auto
|
|
34 |
qed qed
|
|
35 |
|
|
36 |
lemma (in measure_space) positive_integral_omega:
|
|
37 |
assumes "f \<in> borel_measurable M"
|
|
38 |
and "positive_integral f \<noteq> \<omega>"
|
|
39 |
shows "\<mu> (f -` {\<omega>} \<inter> space M) = 0"
|
|
40 |
proof -
|
|
41 |
have "\<omega> * \<mu> (f -` {\<omega>} \<inter> space M) = positive_integral (\<lambda>x. \<omega> * indicator (f -` {\<omega>} \<inter> space M) x)"
|
|
42 |
using positive_integral_cmult_indicator[OF borel_measurable_vimage, OF assms(1), of \<omega> \<omega>] by simp
|
|
43 |
also have "\<dots> \<le> positive_integral f"
|
|
44 |
by (auto intro!: positive_integral_mono simp: indicator_def)
|
|
45 |
finally show ?thesis
|
|
46 |
using assms(2) by (cases ?thesis) auto
|
|
47 |
qed
|
|
48 |
|
|
49 |
lemma (in measure_space) simple_integral_omega:
|
|
50 |
assumes "simple_function f"
|
|
51 |
and "simple_integral f \<noteq> \<omega>"
|
|
52 |
shows "\<mu> (f -` {\<omega>} \<inter> space M) = 0"
|
|
53 |
proof (rule positive_integral_omega)
|
|
54 |
show "f \<in> borel_measurable M" using assms by (auto intro: borel_measurable_simple_function)
|
|
55 |
show "positive_integral f \<noteq> \<omega>"
|
|
56 |
using assms by (simp add: positive_integral_eq_simple_integral)
|
|
57 |
qed
|
|
58 |
|
|
59 |
lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s"
|
|
60 |
unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
|
|
61 |
using assms by auto
|
|
62 |
|
|
63 |
lemma simple_function_has_integral':
|
|
64 |
fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
|
|
65 |
assumes f:"lebesgue.simple_function f"
|
|
66 |
and i: "lebesgue.simple_integral f \<noteq> \<omega>"
|
|
67 |
shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.simple_integral f))) UNIV"
|
|
68 |
proof- let ?f = "\<lambda>x. if f x = \<omega> then 0 else f x"
|
|
69 |
{ fix x have "real (f x) = real (?f x)" by (cases "f x") auto } note * = this
|
|
70 |
have **:"{x. f x \<noteq> ?f x} = f -` {\<omega>}" by auto
|
|
71 |
have **:"lmeasure {x\<in>space lebesgue_space. f x \<noteq> ?f x} = 0"
|
|
72 |
using lebesgue.simple_integral_omega[OF assms] by(auto simp add:**)
|
|
73 |
show ?thesis apply(subst lebesgue.simple_integral_cong'[OF f _ **])
|
|
74 |
apply(rule lebesgue.simple_function_compose1[OF f])
|
|
75 |
unfolding * defer apply(rule simple_function_has_integral)
|
|
76 |
proof-
|
|
77 |
show "lebesgue.simple_function ?f"
|
|
78 |
using lebesgue.simple_function_compose1[OF f] .
|
|
79 |
show "\<forall>x. ?f x \<noteq> \<omega>" by auto
|
|
80 |
show "\<forall>x\<in>range ?f. lmeasure (?f -` {x} \<inter> UNIV) = \<omega> \<longrightarrow> x = 0"
|
|
81 |
proof (safe, simp, safe, rule ccontr)
|
|
82 |
fix y assume "f y \<noteq> \<omega>" "f y \<noteq> 0"
|
|
83 |
hence "(\<lambda>x. if f x = \<omega> then 0 else f x) -` {if f y = \<omega> then 0 else f y} = f -` {f y}"
|
|
84 |
by (auto split: split_if_asm)
|
|
85 |
moreover assume "lmeasure ((\<lambda>x. if f x = \<omega> then 0 else f x) -` {if f y = \<omega> then 0 else f y}) = \<omega>"
|
|
86 |
ultimately have "lmeasure (f -` {f y}) = \<omega>" by simp
|
|
87 |
moreover
|
|
88 |
have "f y * lmeasure (f -` {f y}) \<noteq> \<omega>" using i f
|
|
89 |
unfolding lebesgue.simple_integral_def setsum_\<omega> lebesgue.simple_function_def
|
|
90 |
by auto
|
|
91 |
ultimately have "f y = 0" by (auto split: split_if_asm)
|
|
92 |
then show False using `f y \<noteq> 0` by simp
|
|
93 |
qed
|
|
94 |
qed
|
|
95 |
qed
|
|
96 |
|
|
97 |
lemma (in measure_space) positive_integral_monotone_convergence:
|
|
98 |
fixes f::"nat \<Rightarrow> 'a \<Rightarrow> pinfreal"
|
|
99 |
assumes i: "\<And>i. f i \<in> borel_measurable M" and mono: "\<And>x. mono (\<lambda>n. f n x)"
|
|
100 |
and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
|
|
101 |
shows "u \<in> borel_measurable M"
|
|
102 |
and "(\<lambda>i. positive_integral (f i)) ----> positive_integral u" (is ?ilim)
|
|
103 |
proof -
|
|
104 |
from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u]
|
|
105 |
show ?ilim using mono lim i by auto
|
|
106 |
have "(SUP i. f i) = u" using mono lim SUP_Lim_pinfreal
|
|
107 |
unfolding expand_fun_eq SUPR_fun_expand mono_def by auto
|
|
108 |
moreover have "(SUP i. f i) \<in> borel_measurable M"
|
|
109 |
using i by (rule borel_measurable_SUP)
|
|
110 |
ultimately show "u \<in> borel_measurable M" by simp
|
|
111 |
qed
|
|
112 |
|
|
113 |
lemma positive_integral_has_integral:
|
|
114 |
fixes f::"'a::ordered_euclidean_space => pinfreal"
|
|
115 |
assumes f:"f \<in> borel_measurable lebesgue_space"
|
|
116 |
and int_om:"lebesgue.positive_integral f \<noteq> \<omega>"
|
|
117 |
and f_om:"\<forall>x. f x \<noteq> \<omega>" (* TODO: remove this *)
|
|
118 |
shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.positive_integral f))) UNIV"
|
|
119 |
proof- let ?i = "lebesgue.positive_integral f"
|
|
120 |
from lebesgue.borel_measurable_implies_simple_function_sequence[OF f]
|
|
121 |
guess u .. note conjunctD2[OF this,rule_format] note u = conjunctD2[OF this(1)] this(2)
|
|
122 |
let ?u = "\<lambda>i x. real (u i x)" and ?f = "\<lambda>x. real (f x)"
|
|
123 |
have u_simple:"\<And>k. lebesgue.simple_integral (u k) = lebesgue.positive_integral (u k)"
|
|
124 |
apply(subst lebesgue.positive_integral_eq_simple_integral[THEN sym,OF u(1)]) ..
|
|
125 |
(*unfolding image_iff defer apply(rule) using u(2) by smt*)
|
|
126 |
have int_u_le:"\<And>k. lebesgue.simple_integral (u k) \<le> lebesgue.positive_integral f"
|
|
127 |
unfolding u_simple apply(rule lebesgue.positive_integral_mono)
|
|
128 |
using isoton_Sup[OF u(3)] unfolding le_fun_def by auto
|
|
129 |
have u_int_om:"\<And>i. lebesgue.simple_integral (u i) \<noteq> \<omega>"
|
|
130 |
proof- case goal1 thus ?case using int_u_le[of i] int_om by auto qed
|
|
131 |
|
|
132 |
note u_int = simple_function_has_integral'[OF u(1) this]
|
|
133 |
have "(\<lambda>x. real (f x)) integrable_on UNIV \<and>
|
|
134 |
(\<lambda>k. gintegral UNIV (\<lambda>x. real (u k x))) ----> gintegral UNIV (\<lambda>x. real (f x))"
|
|
135 |
apply(rule monotone_convergence_increasing) apply(rule,rule,rule u_int)
|
|
136 |
proof safe case goal1 show ?case apply(rule real_of_pinfreal_mono) using u(2,3) by auto
|
|
137 |
next case goal2 show ?case using u(3) apply(subst lim_Real[THEN sym])
|
|
138 |
prefer 3 apply(subst Real_real') defer apply(subst Real_real')
|
|
139 |
using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] using f_om u by auto
|
|
140 |
next case goal3
|
|
141 |
show ?case apply(rule bounded_realI[where B="real (lebesgue.positive_integral f)"])
|
|
142 |
apply safe apply(subst abs_of_nonneg) apply(rule integral_nonneg,rule) apply(rule u_int)
|
|
143 |
unfolding integral_unique[OF u_int] defer apply(rule real_of_pinfreal_mono[OF _ int_u_le])
|
|
144 |
using u int_om by auto
|
|
145 |
qed note int = conjunctD2[OF this]
|
|
146 |
|
|
147 |
have "(\<lambda>i. lebesgue.simple_integral (u i)) ----> ?i" unfolding u_simple
|
|
148 |
apply(rule lebesgue.positive_integral_monotone_convergence(2))
|
|
149 |
apply(rule lebesgue.borel_measurable_simple_function[OF u(1)])
|
|
150 |
using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] by auto
|
|
151 |
hence "(\<lambda>i. real (lebesgue.simple_integral (u i))) ----> real ?i" apply-
|
|
152 |
apply(subst lim_Real[THEN sym]) prefer 3
|
|
153 |
apply(subst Real_real') defer apply(subst Real_real')
|
|
154 |
using u f_om int_om u_int_om by auto
|
|
155 |
note * = LIMSEQ_unique[OF this int(2)[unfolded integral_unique[OF u_int]]]
|
|
156 |
show ?thesis unfolding * by(rule integrable_integral[OF int(1)])
|
|
157 |
qed
|
|
158 |
|
|
159 |
lemma lebesgue_integral_has_integral:
|
|
160 |
fixes f::"'a::ordered_euclidean_space => real"
|
|
161 |
assumes f:"lebesgue.integrable f"
|
|
162 |
shows "(f has_integral (lebesgue.integral f)) UNIV"
|
|
163 |
proof- let ?n = "\<lambda>x. - min (f x) 0" and ?p = "\<lambda>x. max (f x) 0"
|
|
164 |
have *:"f = (\<lambda>x. ?p x - ?n x)" apply rule by auto
|
|
165 |
note f = lebesgue.integrableD[OF f]
|
|
166 |
show ?thesis unfolding lebesgue.integral_def apply(subst *)
|
|
167 |
proof(rule has_integral_sub) case goal1
|
|
168 |
have *:"\<forall>x. Real (f x) \<noteq> \<omega>" by auto
|
|
169 |
note lebesgue.borel_measurable_Real[OF f(1)]
|
|
170 |
from positive_integral_has_integral[OF this f(2) *]
|
|
171 |
show ?case unfolding real_Real_max .
|
|
172 |
next case goal2
|
|
173 |
have *:"\<forall>x. Real (- f x) \<noteq> \<omega>" by auto
|
|
174 |
note lebesgue.borel_measurable_uminus[OF f(1)]
|
|
175 |
note lebesgue.borel_measurable_Real[OF this]
|
|
176 |
from positive_integral_has_integral[OF this f(3) *]
|
|
177 |
show ?case unfolding real_Real_max minus_min_eq_max by auto
|
|
178 |
qed
|
|
179 |
qed
|
|
180 |
|
|
181 |
lemma lmeasurable_imp_borel[dest]: fixes s::"'a::ordered_euclidean_space set"
|
|
182 |
assumes "s \<in> sets borel_space" shows "lmeasurable s"
|
|
183 |
proof- let ?S = "range (\<lambda>(a, b). {a .. (b :: 'a\<Colon>ordered_euclidean_space)})"
|
|
184 |
have *:"?S \<subseteq> sets lebesgue_space" by auto
|
|
185 |
have "s \<in> sigma_sets UNIV ?S" using assms
|
|
186 |
unfolding borel_space_eq_atLeastAtMost by (simp add: sigma_def)
|
|
187 |
thus ?thesis using lebesgue.sigma_subset[of ?S,unfolded sets_sigma,OF *]
|
|
188 |
by auto
|
|
189 |
qed
|
|
190 |
|
|
191 |
lemma lmeasurable_open[dest]:
|
|
192 |
assumes "open s" shows "lmeasurable s"
|
|
193 |
proof- have "s \<in> sets borel_space" using assms by auto
|
|
194 |
thus ?thesis by auto qed
|
|
195 |
|
|
196 |
lemma continuous_on_imp_borel_measurable:
|
|
197 |
fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
|
|
198 |
assumes "continuous_on UNIV f"
|
|
199 |
shows "f \<in> borel_measurable lebesgue_space"
|
|
200 |
apply(rule lebesgue.borel_measurableI)
|
|
201 |
unfolding lebesgue_measurable apply(rule lmeasurable_open)
|
|
202 |
using continuous_open_preimage[OF assms] unfolding vimage_def by auto
|
|
203 |
|
|
204 |
|
|
205 |
lemma (in measure_space) integral_monotone_convergence_pos':
|
|
206 |
assumes i: "\<And>i. integrable (f i)" and mono: "\<And>x. mono (\<lambda>n. f n x)"
|
|
207 |
and pos: "\<And>x i. 0 \<le> f i x"
|
|
208 |
and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
|
|
209 |
and ilim: "(\<lambda>i. integral (f i)) ----> x"
|
|
210 |
shows "integrable u \<and> integral u = x"
|
|
211 |
using integral_monotone_convergence_pos[OF assms] by auto
|
|
212 |
|
|
213 |
end
|