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 fun_eq_iff 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 have int_u_le:"\<And>k. lebesgue.simple_integral (u k) \<le> lebesgue.positive_integral f" |
|
126 unfolding u_simple apply(rule lebesgue.positive_integral_mono) |
|
127 using isoton_Sup[OF u(3)] unfolding le_fun_def by auto |
|
128 have u_int_om:"\<And>i. lebesgue.simple_integral (u i) \<noteq> \<omega>" |
|
129 proof- case goal1 thus ?case using int_u_le[of i] int_om by auto qed |
|
130 |
|
131 note u_int = simple_function_has_integral'[OF u(1) this] |
|
132 have "(\<lambda>x. real (f x)) integrable_on UNIV \<and> |
|
133 (\<lambda>k. gintegral UNIV (\<lambda>x. real (u k x))) ----> gintegral UNIV (\<lambda>x. real (f x))" |
|
134 apply(rule monotone_convergence_increasing) apply(rule,rule,rule u_int) |
|
135 proof safe case goal1 show ?case apply(rule real_of_pinfreal_mono) using u(2,3) by auto |
|
136 next case goal2 show ?case using u(3) apply(subst lim_Real[THEN sym]) |
|
137 prefer 3 apply(subst Real_real') defer apply(subst Real_real') |
|
138 using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] using f_om u by auto |
|
139 next case goal3 |
|
140 show ?case apply(rule bounded_realI[where B="real (lebesgue.positive_integral f)"]) |
|
141 apply safe apply(subst abs_of_nonneg) apply(rule integral_nonneg,rule) apply(rule u_int) |
|
142 unfolding integral_unique[OF u_int] defer apply(rule real_of_pinfreal_mono[OF _ int_u_le]) |
|
143 using u int_om by auto |
|
144 qed note int = conjunctD2[OF this] |
|
145 |
|
146 have "(\<lambda>i. lebesgue.simple_integral (u i)) ----> ?i" unfolding u_simple |
|
147 apply(rule lebesgue.positive_integral_monotone_convergence(2)) |
|
148 apply(rule lebesgue.borel_measurable_simple_function[OF u(1)]) |
|
149 using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] by auto |
|
150 hence "(\<lambda>i. real (lebesgue.simple_integral (u i))) ----> real ?i" apply- |
|
151 apply(subst lim_Real[THEN sym]) prefer 3 |
|
152 apply(subst Real_real') defer apply(subst Real_real') |
|
153 using u f_om int_om u_int_om by auto |
|
154 note * = LIMSEQ_unique[OF this int(2)[unfolded integral_unique[OF u_int]]] |
|
155 show ?thesis unfolding * by(rule integrable_integral[OF int(1)]) |
|
156 qed |
|
157 |
|
158 lemma lebesgue_integral_has_integral: |
|
159 fixes f::"'a::ordered_euclidean_space => real" |
|
160 assumes f:"lebesgue.integrable f" |
|
161 shows "(f has_integral (lebesgue.integral f)) UNIV" |
|
162 proof- let ?n = "\<lambda>x. - min (f x) 0" and ?p = "\<lambda>x. max (f x) 0" |
|
163 have *:"f = (\<lambda>x. ?p x - ?n x)" apply rule by auto |
|
164 note f = lebesgue.integrableD[OF f] |
|
165 show ?thesis unfolding lebesgue.integral_def apply(subst *) |
|
166 proof(rule has_integral_sub) case goal1 |
|
167 have *:"\<forall>x. Real (f x) \<noteq> \<omega>" by auto |
|
168 note lebesgue.borel_measurable_Real[OF f(1)] |
|
169 from positive_integral_has_integral[OF this f(2) *] |
|
170 show ?case unfolding real_Real_max . |
|
171 next case goal2 |
|
172 have *:"\<forall>x. Real (- f x) \<noteq> \<omega>" by auto |
|
173 note lebesgue.borel_measurable_uminus[OF f(1)] |
|
174 note lebesgue.borel_measurable_Real[OF this] |
|
175 from positive_integral_has_integral[OF this f(3) *] |
|
176 show ?case unfolding real_Real_max minus_min_eq_max by auto |
|
177 qed |
|
178 qed |
|
179 |
|
180 lemma lmeasurable_imp_borel[dest]: fixes s::"'a::ordered_euclidean_space set" |
|
181 assumes "s \<in> sets borel_space" shows "lmeasurable s" |
|
182 proof- let ?S = "range (\<lambda>(a, b). {a .. (b :: 'a\<Colon>ordered_euclidean_space)})" |
|
183 have *:"?S \<subseteq> sets lebesgue_space" by auto |
|
184 have "s \<in> sigma_sets UNIV ?S" using assms |
|
185 unfolding borel_space_eq_atLeastAtMost by (simp add: sigma_def) |
|
186 thus ?thesis using lebesgue.sigma_subset[of ?S,unfolded sets_sigma,OF *] |
|
187 by auto |
|
188 qed |
|
189 |
|
190 lemma lmeasurable_open[dest]: |
|
191 assumes "open s" shows "lmeasurable s" |
|
192 proof- have "s \<in> sets borel_space" using assms by auto |
|
193 thus ?thesis by auto qed |
|
194 |
|
195 lemma continuous_on_imp_borel_measurable: |
|
196 fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space" |
|
197 assumes "continuous_on UNIV f" |
|
198 shows "f \<in> borel_measurable lebesgue_space" |
|
199 apply(rule lebesgue.borel_measurableI) |
|
200 unfolding lebesgue_measurable apply(rule lmeasurable_open) |
|
201 using continuous_open_preimage[OF assms] unfolding vimage_def by auto |
|
202 |
|
203 |
|
204 lemma (in measure_space) integral_monotone_convergence_pos': |
|
205 assumes i: "\<And>i. integrable (f i)" and mono: "\<And>x. mono (\<lambda>n. f n x)" |
|
206 and pos: "\<And>x i. 0 \<le> f i x" |
|
207 and lim: "\<And>x. (\<lambda>i. f i x) ----> u x" |
|
208 and ilim: "(\<lambda>i. integral (f i)) ----> x" |
|
209 shows "integrable u \<and> integral u = x" |
|
210 using integral_monotone_convergence_pos[OF assms] by auto |
|
211 |
|
212 end |
|