|
1 (* Title: HOL/Probability/Interval_Integral.thy |
|
2 Author: Jeremy Avigad, Johannes Hölzl, Luke Serafin |
|
3 |
|
4 Lebesgue integral over an interval (with endpoints possibly +-\<infinity>) |
|
5 *) |
|
6 |
|
7 theory Interval_Integral |
|
8 imports Set_Integral |
|
9 begin |
|
10 |
|
11 lemma continuous_on_vector_derivative: |
|
12 "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f" |
|
13 by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous) |
|
14 |
|
15 lemma has_vector_derivative_weaken: |
|
16 fixes x D and f g s t |
|
17 assumes f: "(f has_vector_derivative D) (at x within t)" |
|
18 and "x \<in> s" "s \<subseteq> t" |
|
19 and "\<And>x. x \<in> s \<Longrightarrow> f x = g x" |
|
20 shows "(g has_vector_derivative D) (at x within s)" |
|
21 proof - |
|
22 have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)" |
|
23 unfolding has_vector_derivative_def has_derivative_iff_norm |
|
24 using assms by (intro conj_cong Lim_cong_within refl) auto |
|
25 then show ?thesis |
|
26 using has_vector_derivative_within_subset[OF f `s \<subseteq> t`] by simp |
|
27 qed |
|
28 |
|
29 definition "einterval a b = {x. a < ereal x \<and> ereal x < b}" |
|
30 |
|
31 lemma einterval_eq[simp]: |
|
32 shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}" |
|
33 and einterval_eq_Ici: "einterval (ereal a) \<infinity> = {a <..}" |
|
34 and einterval_eq_Iic: "einterval (- \<infinity>) (ereal b) = {..< b}" |
|
35 and einterval_eq_UNIV: "einterval (- \<infinity>) \<infinity> = UNIV" |
|
36 by (auto simp: einterval_def) |
|
37 |
|
38 lemma einterval_same: "einterval a a = {}" |
|
39 by (auto simp add: einterval_def) |
|
40 |
|
41 lemma einterval_iff: "x \<in> einterval a b \<longleftrightarrow> a < ereal x \<and> ereal x < b" |
|
42 by (simp add: einterval_def) |
|
43 |
|
44 lemma einterval_nonempty: "a < b \<Longrightarrow> \<exists>c. c \<in> einterval a b" |
|
45 by (cases a b rule: ereal2_cases, auto simp: einterval_def intro!: dense gt_ex lt_ex) |
|
46 |
|
47 lemma open_einterval[simp]: "open (einterval a b)" |
|
48 by (cases a b rule: ereal2_cases) |
|
49 (auto simp: einterval_def intro!: open_Collect_conj open_Collect_less continuous_intros) |
|
50 |
|
51 lemma borel_einterval[measurable]: "einterval a b \<in> sets borel" |
|
52 unfolding einterval_def by measurable |
|
53 |
|
54 (* |
|
55 Approximating a (possibly infinite) interval |
|
56 *) |
|
57 |
|
58 lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))" |
|
59 unfolding filterlim_def by (auto intro: le_supI1) |
|
60 |
|
61 lemma ereal_incseq_approx: |
|
62 fixes a b :: ereal |
|
63 assumes "a < b" |
|
64 obtains X :: "nat \<Rightarrow> real" where |
|
65 "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X ----> b" |
|
66 proof (cases b) |
|
67 case PInf |
|
68 with `a < b` have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)" |
|
69 by (cases a) auto |
|
70 moreover have " (\<lambda>x. ereal (real (Suc x))) ----> \<infinity>" |
|
71 using natceiling_le_eq by (subst LIMSEQ_Suc_iff) (auto simp: Lim_PInfty) |
|
72 moreover have "\<And>r. (\<lambda>x. ereal (r + real (Suc x))) ----> \<infinity>" |
|
73 apply (subst LIMSEQ_Suc_iff) |
|
74 apply (subst Lim_PInfty) |
|
75 apply (metis add.commute diff_le_eq natceiling_le_eq ereal_less_eq(3)) |
|
76 done |
|
77 ultimately show thesis |
|
78 by (intro that[of "\<lambda>i. real a + Suc i"]) |
|
79 (auto simp: incseq_def PInf) |
|
80 next |
|
81 case (real b') |
|
82 def d \<equiv> "b' - (if a = -\<infinity> then b' - 1 else real a)" |
|
83 with `a < b` have a': "0 < d" |
|
84 by (cases a) (auto simp: real) |
|
85 moreover |
|
86 have "\<And>i r. r < b' \<Longrightarrow> (b' - r) * 1 < (b' - r) * real (Suc (Suc i))" |
|
87 by (intro mult_strict_left_mono) auto |
|
88 with `a < b` a' have "\<And>i. a < ereal (b' - d / real (Suc (Suc i)))" |
|
89 by (cases a) (auto simp: real d_def field_simps) |
|
90 moreover have "(\<lambda>i. b' - d / Suc (Suc i)) ----> b'" |
|
91 apply (subst filterlim_sequentially_Suc) |
|
92 apply (subst filterlim_sequentially_Suc) |
|
93 apply (rule tendsto_eq_intros) |
|
94 apply (auto intro!: tendsto_divide_0[OF tendsto_const] filterlim_sup1 |
|
95 simp: at_infinity_eq_at_top_bot filterlim_real_sequentially) |
|
96 done |
|
97 ultimately show thesis |
|
98 by (intro that[of "\<lambda>i. b' - d / Suc (Suc i)"]) |
|
99 (auto simp add: real incseq_def intro!: divide_left_mono) |
|
100 qed (insert `a < b`, auto) |
|
101 |
|
102 lemma ereal_decseq_approx: |
|
103 fixes a b :: ereal |
|
104 assumes "a < b" |
|
105 obtains X :: "nat \<Rightarrow> real" where |
|
106 "decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X ----> a" |
|
107 proof - |
|
108 have "-b < -a" using `a < b` by simp |
|
109 from ereal_incseq_approx[OF this] guess X . |
|
110 then show thesis |
|
111 apply (intro that[of "\<lambda>i. - X i"]) |
|
112 apply (auto simp add: uminus_ereal.simps[symmetric] decseq_def incseq_def |
|
113 simp del: uminus_ereal.simps) |
|
114 apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+ |
|
115 done |
|
116 qed |
|
117 |
|
118 lemma einterval_Icc_approximation: |
|
119 fixes a b :: ereal |
|
120 assumes "a < b" |
|
121 obtains u l :: "nat \<Rightarrow> real" where |
|
122 "einterval a b = (\<Union>i. {l i .. u i})" |
|
123 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
|
124 "l ----> a" "u ----> b" |
|
125 proof - |
|
126 from dense[OF `a < b`] obtain c where "a < c" "c < b" by safe |
|
127 from ereal_incseq_approx[OF `c < b`] guess u . note u = this |
|
128 from ereal_decseq_approx[OF `a < c`] guess l . note l = this |
|
129 { fix i from less_trans[OF `l i < c` `c < u i`] have "l i < u i" by simp } |
|
130 have "einterval a b = (\<Union>i. {l i .. u i})" |
|
131 proof (auto simp: einterval_iff) |
|
132 fix x assume "a < ereal x" "ereal x < b" |
|
133 have "eventually (\<lambda>i. ereal (l i) < ereal x) sequentially" |
|
134 using l(4) `a < ereal x` by (rule order_tendstoD) |
|
135 moreover |
|
136 have "eventually (\<lambda>i. ereal x < ereal (u i)) sequentially" |
|
137 using u(4) `ereal x< b` by (rule order_tendstoD) |
|
138 ultimately have "eventually (\<lambda>i. l i < x \<and> x < u i) sequentially" |
|
139 by eventually_elim auto |
|
140 then show "\<exists>i. l i \<le> x \<and> x \<le> u i" |
|
141 by (auto intro: less_imp_le simp: eventually_sequentially) |
|
142 next |
|
143 fix x i assume "l i \<le> x" "x \<le> u i" |
|
144 with `a < ereal (l i)` `ereal (u i) < b` |
|
145 show "a < ereal x" "ereal x < b" |
|
146 by (auto simp del: ereal_less_eq(3) simp add: ereal_less_eq(3)[symmetric]) |
|
147 qed |
|
148 show thesis |
|
149 by (intro that) fact+ |
|
150 qed |
|
151 |
|
152 (* TODO: in this definition, it would be more natural if einterval a b included a and b when |
|
153 they are real. *) |
|
154 definition interval_lebesgue_integral :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> 'a::{banach, second_countable_topology}" where |
|
155 "interval_lebesgue_integral M a b f = |
|
156 (if a \<le> b then (LINT x:einterval a b|M. f x) else - (LINT x:einterval b a|M. f x))" |
|
157 |
|
158 syntax |
|
159 "_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real" |
|
160 ("(5LINT _=_.._|_. _)" [0,60,60,61,100] 60) |
|
161 |
|
162 translations |
|
163 "LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (\<lambda>x. f)" |
|
164 |
|
165 definition interval_lebesgue_integrable :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a::{banach, second_countable_topology}) \<Rightarrow> bool" where |
|
166 "interval_lebesgue_integrable M a b f = |
|
167 (if a \<le> b then set_integrable M (einterval a b) f else set_integrable M (einterval b a) f)" |
|
168 |
|
169 syntax |
|
170 "_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" |
|
171 ("(4LBINT _=_.._. _)" [0,60,60,61] 60) |
|
172 |
|
173 translations |
|
174 "LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)" |
|
175 |
|
176 (* |
|
177 Basic properties of integration over an interval. |
|
178 *) |
|
179 |
|
180 lemma interval_lebesgue_integral_cong: |
|
181 "a \<le> b \<Longrightarrow> (\<And>x. x \<in> einterval a b \<Longrightarrow> f x = g x) \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow> |
|
182 interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g" |
|
183 by (auto intro: set_lebesgue_integral_cong simp: interval_lebesgue_integral_def) |
|
184 |
|
185 lemma interval_lebesgue_integral_cong_AE: |
|
186 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> |
|
187 a \<le> b \<Longrightarrow> AE x \<in> einterval a b in M. f x = g x \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow> |
|
188 interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g" |
|
189 by (auto intro: set_lebesgue_integral_cong_AE simp: interval_lebesgue_integral_def) |
|
190 |
|
191 lemma interval_lebesgue_integral_add [intro, simp]: |
|
192 fixes M a b f |
|
193 assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g" |
|
194 shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)" and |
|
195 "interval_lebesgue_integral M a b (\<lambda>x. f x + g x) = |
|
196 interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g" |
|
197 using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def |
|
198 field_simps) |
|
199 |
|
200 lemma interval_lebesgue_integral_diff [intro, simp]: |
|
201 fixes M a b f |
|
202 assumes "interval_lebesgue_integrable M a b f" |
|
203 "interval_lebesgue_integrable M a b g" |
|
204 shows "interval_lebesgue_integrable M a b (\<lambda>x. f x - g x)" and |
|
205 "interval_lebesgue_integral M a b (\<lambda>x. f x - g x) = |
|
206 interval_lebesgue_integral M a b f - interval_lebesgue_integral M a b g" |
|
207 using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def |
|
208 field_simps) |
|
209 |
|
210 lemma interval_lebesgue_integrable_mult_right [intro, simp]: |
|
211 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}" |
|
212 shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow> |
|
213 interval_lebesgue_integrable M a b (\<lambda>x. c * f x)" |
|
214 by (simp add: interval_lebesgue_integrable_def) |
|
215 |
|
216 lemma interval_lebesgue_integrable_mult_left [intro, simp]: |
|
217 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}" |
|
218 shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow> |
|
219 interval_lebesgue_integrable M a b (\<lambda>x. f x * c)" |
|
220 by (simp add: interval_lebesgue_integrable_def) |
|
221 |
|
222 lemma interval_lebesgue_integrable_divide [intro, simp]: |
|
223 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}" |
|
224 shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow> |
|
225 interval_lebesgue_integrable M a b (\<lambda>x. f x / c)" |
|
226 by (simp add: interval_lebesgue_integrable_def) |
|
227 |
|
228 lemma interval_lebesgue_integral_mult_right [simp]: |
|
229 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}" |
|
230 shows "interval_lebesgue_integral M a b (\<lambda>x. c * f x) = |
|
231 c * interval_lebesgue_integral M a b f" |
|
232 by (simp add: interval_lebesgue_integral_def) |
|
233 |
|
234 lemma interval_lebesgue_integral_mult_left [simp]: |
|
235 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}" |
|
236 shows "interval_lebesgue_integral M a b (\<lambda>x. f x * c) = |
|
237 interval_lebesgue_integral M a b f * c" |
|
238 by (simp add: interval_lebesgue_integral_def) |
|
239 |
|
240 lemma interval_lebesgue_integral_divide [simp]: |
|
241 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}" |
|
242 shows "interval_lebesgue_integral M a b (\<lambda>x. f x / c) = |
|
243 interval_lebesgue_integral M a b f / c" |
|
244 by (simp add: interval_lebesgue_integral_def) |
|
245 |
|
246 lemma interval_lebesgue_integral_uminus: |
|
247 "interval_lebesgue_integral M a b (\<lambda>x. - f x) = - interval_lebesgue_integral M a b f" |
|
248 by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def) |
|
249 |
|
250 lemma interval_lebesgue_integral_of_real: |
|
251 "interval_lebesgue_integral M a b (\<lambda>x. complex_of_real (f x)) = |
|
252 of_real (interval_lebesgue_integral M a b f)" |
|
253 unfolding interval_lebesgue_integral_def |
|
254 by (auto simp add: interval_lebesgue_integral_def set_integral_complex_of_real) |
|
255 |
|
256 lemma interval_lebesgue_integral_le_eq: |
|
257 fixes a b f |
|
258 assumes "a \<le> b" |
|
259 shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)" |
|
260 using assms by (auto simp add: interval_lebesgue_integral_def) |
|
261 |
|
262 lemma interval_lebesgue_integral_gt_eq: |
|
263 fixes a b f |
|
264 assumes "a > b" |
|
265 shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)" |
|
266 using assms by (auto simp add: interval_lebesgue_integral_def less_imp_le einterval_def) |
|
267 |
|
268 lemma interval_lebesgue_integral_gt_eq': |
|
269 fixes a b f |
|
270 assumes "a > b" |
|
271 shows "interval_lebesgue_integral M a b f = - interval_lebesgue_integral M b a f" |
|
272 using assms by (auto simp add: interval_lebesgue_integral_def less_imp_le einterval_def) |
|
273 |
|
274 lemma interval_integral_endpoints_same [simp]: "(LBINT x=a..a. f x) = 0" |
|
275 by (simp add: interval_lebesgue_integral_def einterval_same) |
|
276 |
|
277 lemma interval_integral_endpoints_reverse: "(LBINT x=a..b. f x) = -(LBINT x=b..a. f x)" |
|
278 by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integral_def einterval_same) |
|
279 |
|
280 lemma interval_integrable_endpoints_reverse: |
|
281 "interval_lebesgue_integrable lborel a b f \<longleftrightarrow> |
|
282 interval_lebesgue_integrable lborel b a f" |
|
283 by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same) |
|
284 |
|
285 lemma interval_integral_reflect: |
|
286 "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))" |
|
287 proof (induct a b rule: linorder_wlog) |
|
288 case (sym a b) then show ?case |
|
289 by (auto simp add: interval_lebesgue_integral_def interval_integrable_endpoints_reverse |
|
290 split: split_if_asm) |
|
291 next |
|
292 case (le a b) then show ?case |
|
293 unfolding interval_lebesgue_integral_def |
|
294 by (subst set_integral_reflect) |
|
295 (auto simp: interval_lebesgue_integrable_def einterval_iff |
|
296 ereal_uminus_le_reorder ereal_uminus_less_reorder not_less |
|
297 uminus_ereal.simps[symmetric] |
|
298 simp del: uminus_ereal.simps |
|
299 intro!: integral_cong |
|
300 split: split_indicator) |
|
301 qed |
|
302 |
|
303 (* |
|
304 Basic properties of integration over an interval wrt lebesgue measure. |
|
305 *) |
|
306 |
|
307 lemma interval_integral_zero [simp]: |
|
308 fixes a b :: ereal |
|
309 shows"LBINT x=a..b. 0 = 0" |
|
310 using assms unfolding interval_lebesgue_integral_def einterval_eq |
|
311 by simp |
|
312 |
|
313 lemma interval_integral_const [intro, simp]: |
|
314 fixes a b c :: real |
|
315 shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)" |
|
316 using assms unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq |
|
317 by (auto simp add: less_imp_le field_simps measure_def) |
|
318 |
|
319 lemma interval_integral_cong_AE: |
|
320 assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel" |
|
321 assumes "AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x" |
|
322 shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g" |
|
323 using assms |
|
324 proof (induct a b rule: linorder_wlog) |
|
325 case (sym a b) then show ?case |
|
326 by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b]) |
|
327 next |
|
328 case (le a b) then show ?case |
|
329 by (auto simp: interval_lebesgue_integral_def max_def min_def |
|
330 intro!: set_lebesgue_integral_cong_AE) |
|
331 qed |
|
332 |
|
333 lemma interval_integral_cong: |
|
334 assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x" |
|
335 shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g" |
|
336 using assms |
|
337 proof (induct a b rule: linorder_wlog) |
|
338 case (sym a b) then show ?case |
|
339 by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b]) |
|
340 next |
|
341 case (le a b) then show ?case |
|
342 by (auto simp: interval_lebesgue_integral_def max_def min_def |
|
343 intro!: set_lebesgue_integral_cong) |
|
344 qed |
|
345 |
|
346 lemma interval_lebesgue_integrable_cong_AE: |
|
347 "f \<in> borel_measurable lborel \<Longrightarrow> g \<in> borel_measurable lborel \<Longrightarrow> |
|
348 AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x \<Longrightarrow> |
|
349 interval_lebesgue_integrable lborel a b f = interval_lebesgue_integrable lborel a b g" |
|
350 apply (simp add: interval_lebesgue_integrable_def ) |
|
351 apply (intro conjI impI set_integrable_cong_AE) |
|
352 apply (auto simp: min_def max_def) |
|
353 done |
|
354 |
|
355 lemma interval_integrable_abs_iff: |
|
356 fixes f :: "real \<Rightarrow> real" |
|
357 shows "f \<in> borel_measurable lborel \<Longrightarrow> |
|
358 interval_lebesgue_integrable lborel a b (\<lambda>x. \<bar>f x\<bar>) = interval_lebesgue_integrable lborel a b f" |
|
359 unfolding interval_lebesgue_integrable_def |
|
360 by (subst (1 2) set_integrable_abs_iff') simp_all |
|
361 |
|
362 lemma interval_integral_Icc: |
|
363 fixes a b :: real |
|
364 shows "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {a..b}. f x)" |
|
365 by (auto intro!: set_integral_discrete_difference[where X="{a, b}"] |
|
366 simp add: interval_lebesgue_integral_def) |
|
367 |
|
368 lemma interval_integral_Icc': |
|
369 "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {x. a \<le> ereal x \<and> ereal x \<le> b}. f x)" |
|
370 by (auto intro!: set_integral_discrete_difference[where X="{real a, real b}"] |
|
371 simp add: interval_lebesgue_integral_def einterval_iff) |
|
372 |
|
373 lemma interval_integral_Ioc: |
|
374 "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {a<..b}. f x)" |
|
375 by (auto intro!: set_integral_discrete_difference[where X="{a, b}"] |
|
376 simp add: interval_lebesgue_integral_def einterval_iff) |
|
377 |
|
378 (* TODO: other versions as well? *) (* Yes: I need the Icc' version. *) |
|
379 lemma interval_integral_Ioc': |
|
380 "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {x. a < ereal x \<and> ereal x \<le> b}. f x)" |
|
381 by (auto intro!: set_integral_discrete_difference[where X="{real a, real b}"] |
|
382 simp add: interval_lebesgue_integral_def einterval_iff) |
|
383 |
|
384 lemma interval_integral_Ico: |
|
385 "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {a..<b}. f x)" |
|
386 by (auto intro!: set_integral_discrete_difference[where X="{a, b}"] |
|
387 simp add: interval_lebesgue_integral_def einterval_iff) |
|
388 |
|
389 lemma interval_integral_Ioi: |
|
390 "\<bar>a\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..\<infinity>. f x) = (LBINT x : {real a <..}. f x)" |
|
391 by (auto simp add: interval_lebesgue_integral_def einterval_iff) |
|
392 |
|
393 lemma interval_integral_Ioo: |
|
394 "a \<le> b \<Longrightarrow> \<bar>a\<bar> < \<infinity> ==> \<bar>b\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {real a <..< real b}. f x)" |
|
395 by (auto simp add: interval_lebesgue_integral_def einterval_iff) |
|
396 |
|
397 lemma interval_integral_discrete_difference: |
|
398 fixes f :: "real \<Rightarrow> 'b::{banach, second_countable_topology}" and a b :: ereal |
|
399 assumes "countable X" |
|
400 and eq: "\<And>x. a \<le> b \<Longrightarrow> a < x \<Longrightarrow> x < b \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x" |
|
401 and anti_eq: "\<And>x. b \<le> a \<Longrightarrow> b < x \<Longrightarrow> x < a \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x" |
|
402 assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M" |
|
403 shows "interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g" |
|
404 unfolding interval_lebesgue_integral_def |
|
405 apply (intro if_cong refl arg_cong[where f="\<lambda>x. - x"] integral_discrete_difference[of X] assms) |
|
406 apply (auto simp: eq anti_eq einterval_iff split: split_indicator) |
|
407 done |
|
408 |
|
409 lemma interval_integral_sum: |
|
410 fixes a b c :: ereal |
|
411 assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f" |
|
412 shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)" |
|
413 proof - |
|
414 let ?I = "\<lambda>a b. LBINT x=a..b. f x" |
|
415 { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c" |
|
416 then have ord: "a \<le> b" "b \<le> c" "a \<le> c" and f': "set_integrable lborel (einterval a c) f" |
|
417 by (auto simp: interval_lebesgue_integrable_def) |
|
418 then have f: "set_borel_measurable borel (einterval a c) f" |
|
419 by (drule_tac borel_measurable_integrable) simp |
|
420 have "(LBINT x:einterval a c. f x) = (LBINT x:einterval a b \<union> einterval b c. f x)" |
|
421 proof (rule set_integral_cong_set) |
|
422 show "AE x in lborel. (x \<in> einterval a b \<union> einterval b c) = (x \<in> einterval a c)" |
|
423 using AE_lborel_singleton[of "real b"] ord |
|
424 by (cases a b c rule: ereal3_cases) (auto simp: einterval_iff) |
|
425 qed (insert ord, auto intro!: set_borel_measurable_subset[OF f] simp: einterval_iff) |
|
426 also have "\<dots> = (LBINT x:einterval a b. f x) + (LBINT x:einterval b c. f x)" |
|
427 using ord |
|
428 by (intro set_integral_Un_AE) (auto intro!: set_integrable_subset[OF f'] simp: einterval_iff not_less) |
|
429 finally have "?I a b + ?I b c = ?I a c" |
|
430 using ord by (simp add: interval_lebesgue_integral_def) |
|
431 } note 1 = this |
|
432 { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c" |
|
433 from 1[OF this] have "?I b c + ?I a b = ?I a c" |
|
434 by (metis add.commute) |
|
435 } note 2 = this |
|
436 have 3: "\<And>a b. b \<le> a \<Longrightarrow> (LBINT x=a..b. f x) = - (LBINT x=b..a. f x)" |
|
437 by (rule interval_integral_endpoints_reverse) |
|
438 show ?thesis |
|
439 using integrable |
|
440 by (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases]) |
|
441 (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3) |
|
442 qed |
|
443 |
|
444 lemma interval_integrable_isCont: |
|
445 fixes a b and f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}" |
|
446 shows "(\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> isCont f x) \<Longrightarrow> |
|
447 interval_lebesgue_integrable lborel a b f" |
|
448 proof (induct a b rule: linorder_wlog) |
|
449 case (le a b) then show ?case |
|
450 by (auto simp: interval_lebesgue_integrable_def |
|
451 intro!: set_integrable_subset[OF borel_integrable_compact[of "{a .. b}"]] |
|
452 continuous_at_imp_continuous_on) |
|
453 qed (auto intro: interval_integrable_endpoints_reverse[THEN iffD1]) |
|
454 |
|
455 lemma interval_integrable_continuous_on: |
|
456 fixes a b :: real and f |
|
457 assumes "a \<le> b" and "continuous_on {a..b} f" |
|
458 shows "interval_lebesgue_integrable lborel a b f" |
|
459 using assms unfolding interval_lebesgue_integrable_def apply simp |
|
460 by (rule set_integrable_subset, rule borel_integrable_atLeastAtMost' [of a b], auto) |
|
461 |
|
462 lemma interval_integral_eq_integral: |
|
463 fixes f :: "real \<Rightarrow> 'a::euclidean_space" |
|
464 shows "a \<le> b \<Longrightarrow> set_integrable lborel {a..b} f \<Longrightarrow> LBINT x=a..b. f x = integral {a..b} f" |
|
465 by (subst interval_integral_Icc, simp) (rule set_borel_integral_eq_integral) |
|
466 |
|
467 lemma interval_integral_eq_integral': |
|
468 fixes f :: "real \<Rightarrow> 'a::euclidean_space" |
|
469 shows "a \<le> b \<Longrightarrow> set_integrable lborel (einterval a b) f \<Longrightarrow> LBINT x=a..b. f x = integral (einterval a b) f" |
|
470 by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral) |
|
471 |
|
472 (* |
|
473 General limit approximation arguments |
|
474 *) |
|
475 |
|
476 lemma interval_integral_Icc_approx_nonneg: |
|
477 fixes a b :: ereal |
|
478 assumes "a < b" |
|
479 fixes u l :: "nat \<Rightarrow> real" |
|
480 assumes approx: "einterval a b = (\<Union>i. {l i .. u i})" |
|
481 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
|
482 "l ----> a" "u ----> b" |
|
483 fixes f :: "real \<Rightarrow> real" |
|
484 assumes f_integrable: "\<And>i. set_integrable lborel {l i..u i} f" |
|
485 assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x" |
|
486 assumes f_measurable: "set_borel_measurable lborel (einterval a b) f" |
|
487 assumes lbint_lim: "(\<lambda>i. LBINT x=l i.. u i. f x) ----> C" |
|
488 shows |
|
489 "set_integrable lborel (einterval a b) f" |
|
490 "(LBINT x=a..b. f x) = C" |
|
491 proof - |
|
492 have 1: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable) |
|
493 have 2: "AE x in lborel. mono (\<lambda>n. indicator {l n..u n} x *\<^sub>R f x)" |
|
494 proof - |
|
495 from f_nonneg have "AE x in lborel. \<forall>i. l i \<le> x \<longrightarrow> x \<le> u i \<longrightarrow> 0 \<le> f x" |
|
496 by eventually_elim |
|
497 (metis approx(5) approx(6) dual_order.strict_trans1 ereal_less_eq(3) le_less_trans) |
|
498 then show ?thesis |
|
499 apply eventually_elim |
|
500 apply (auto simp: mono_def split: split_indicator) |
|
501 apply (metis approx(3) decseqD order_trans) |
|
502 apply (metis approx(2) incseqD order_trans) |
|
503 done |
|
504 qed |
|
505 have 3: "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) ----> indicator (einterval a b) x *\<^sub>R f x" |
|
506 proof - |
|
507 { fix x i assume "l i \<le> x" "x \<le> u i" |
|
508 then have "eventually (\<lambda>i. l i \<le> x \<and> x \<le> u i) sequentially" |
|
509 apply (auto simp: eventually_sequentially intro!: exI[of _ i]) |
|
510 apply (metis approx(3) decseqD order_trans) |
|
511 apply (metis approx(2) incseqD order_trans) |
|
512 done |
|
513 then have "eventually (\<lambda>i. f x * indicator {l i..u i} x = f x) sequentially" |
|
514 by eventually_elim auto } |
|
515 then show ?thesis |
|
516 unfolding approx(1) by (auto intro!: AE_I2 Lim_eventually split: split_indicator) |
|
517 qed |
|
518 have 4: "(\<lambda>i. \<integral> x. indicator {l i..u i} x *\<^sub>R f x \<partial>lborel) ----> C" |
|
519 using lbint_lim by (simp add: interval_integral_Icc approx less_imp_le) |
|
520 have 5: "set_borel_measurable lborel (einterval a b) f" by (rule assms) |
|
521 have "(LBINT x=a..b. f x) = lebesgue_integral lborel (\<lambda>x. indicator (einterval a b) x *\<^sub>R f x)" |
|
522 using assms by (simp add: interval_lebesgue_integral_def less_imp_le) |
|
523 also have "... = C" by (rule integral_monotone_convergence [OF 1 2 3 4 5]) |
|
524 finally show "(LBINT x=a..b. f x) = C" . |
|
525 |
|
526 show "set_integrable lborel (einterval a b) f" |
|
527 by (rule integrable_monotone_convergence[OF 1 2 3 4 5]) |
|
528 qed |
|
529 |
|
530 lemma interval_integral_Icc_approx_integrable: |
|
531 fixes u l :: "nat \<Rightarrow> real" and a b :: ereal |
|
532 fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}" |
|
533 assumes "a < b" |
|
534 assumes approx: "einterval a b = (\<Union>i. {l i .. u i})" |
|
535 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
|
536 "l ----> a" "u ----> b" |
|
537 assumes f_integrable: "set_integrable lborel (einterval a b) f" |
|
538 shows "(\<lambda>i. LBINT x=l i.. u i. f x) ----> (LBINT x=a..b. f x)" |
|
539 proof - |
|
540 have "(\<lambda>i. LBINT x:{l i.. u i}. f x) ----> (LBINT x:einterval a b. f x)" |
|
541 proof (rule integral_dominated_convergence) |
|
542 show "integrable lborel (\<lambda>x. norm (indicator (einterval a b) x *\<^sub>R f x))" |
|
543 by (rule integrable_norm) fact |
|
544 show "set_borel_measurable lborel (einterval a b) f" |
|
545 using f_integrable by (rule borel_measurable_integrable) |
|
546 then show "\<And>i. set_borel_measurable lborel {l i..u i} f" |
|
547 by (rule set_borel_measurable_subset) (auto simp: approx) |
|
548 show "\<And>i. AE x in lborel. norm (indicator {l i..u i} x *\<^sub>R f x) \<le> norm (indicator (einterval a b) x *\<^sub>R f x)" |
|
549 by (intro AE_I2) (auto simp: approx split: split_indicator) |
|
550 show "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) ----> indicator (einterval a b) x *\<^sub>R f x" |
|
551 proof (intro AE_I2 tendsto_intros Lim_eventually) |
|
552 fix x |
|
553 { fix i assume "l i \<le> x" "x \<le> u i" |
|
554 with `incseq u`[THEN incseqD, of i] `decseq l`[THEN decseqD, of i] |
|
555 have "eventually (\<lambda>i. l i \<le> x \<and> x \<le> u i) sequentially" |
|
556 by (auto simp: eventually_sequentially decseq_def incseq_def intro: order_trans) } |
|
557 then show "eventually (\<lambda>xa. indicator {l xa..u xa} x = (indicator (einterval a b) x::real)) sequentially" |
|
558 using approx order_tendstoD(2)[OF `l ----> a`, of x] order_tendstoD(1)[OF `u ----> b`, of x] |
|
559 by (auto split: split_indicator) |
|
560 qed |
|
561 qed |
|
562 with `a < b` `\<And>i. l i < u i` show ?thesis |
|
563 by (simp add: interval_lebesgue_integral_le_eq[symmetric] interval_integral_Icc less_imp_le) |
|
564 qed |
|
565 |
|
566 (* |
|
567 A slightly stronger version of integral_FTC_atLeastAtMost and related facts, |
|
568 with continuous_on instead of isCont |
|
569 |
|
570 TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.) |
|
571 *) |
|
572 |
|
573 (* |
|
574 TODO: many proofs below require inferences like |
|
575 |
|
576 a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y |
|
577 |
|
578 where x and y are real. These should be better automated. |
|
579 *) |
|
580 |
|
581 (* |
|
582 The first Fundamental Theorem of Calculus |
|
583 |
|
584 First, for finite intervals, and then two versions for arbitrary intervals. |
|
585 *) |
|
586 |
|
587 lemma interval_integral_FTC_finite: |
|
588 fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real |
|
589 assumes f: "continuous_on {min a b..max a b} f" |
|
590 assumes F: "\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> (F has_vector_derivative (f x)) (at x within |
|
591 {min a b..max a b})" |
|
592 shows "(LBINT x=a..b. f x) = F b - F a" |
|
593 apply (case_tac "a \<le> b") |
|
594 apply (subst interval_integral_Icc, simp) |
|
595 apply (rule integral_FTC_atLeastAtMost, assumption) |
|
596 apply (metis F max_def min_def) |
|
597 using f apply (simp add: min_absorb1 max_absorb2) |
|
598 apply (subst interval_integral_endpoints_reverse) |
|
599 apply (subst interval_integral_Icc, simp) |
|
600 apply (subst integral_FTC_atLeastAtMost, auto) |
|
601 apply (metis F max_def min_def) |
|
602 using f by (simp add: min_absorb2 max_absorb1) |
|
603 |
|
604 lemma interval_integral_FTC_nonneg: |
|
605 fixes f F :: "real \<Rightarrow> real" and a b :: ereal |
|
606 assumes "a < b" |
|
607 assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x" |
|
608 assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x" |
|
609 assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x" |
|
610 assumes A: "((F \<circ> real) ---> A) (at_right a)" |
|
611 assumes B: "((F \<circ> real) ---> B) (at_left b)" |
|
612 shows |
|
613 "set_integrable lborel (einterval a b) f" |
|
614 "(LBINT x=a..b. f x) = B - A" |
|
615 proof - |
|
616 from einterval_Icc_approximation[OF `a < b`] guess u l . note approx = this |
|
617 have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x" |
|
618 by (rule order_less_le_trans, rule approx, force) |
|
619 have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b" |
|
620 by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) |
|
621 have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)" |
|
622 using assms approx apply (intro interval_integral_FTC_finite) |
|
623 apply (auto simp add: less_imp_le min_def max_def |
|
624 has_field_derivative_iff_has_vector_derivative[symmetric]) |
|
625 apply (rule continuous_at_imp_continuous_on, auto intro!: f) |
|
626 by (rule DERIV_subset [OF F], auto) |
|
627 have 1: "\<And>i. set_integrable lborel {l i..u i} f" |
|
628 proof - |
|
629 fix i show "set_integrable lborel {l i .. u i} f" |
|
630 using `a < l i` `u i < b` |
|
631 by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI) |
|
632 (auto simp del: ereal_less_eq simp add: ereal_less_eq(3)[symmetric]) |
|
633 qed |
|
634 have 2: "set_borel_measurable lborel (einterval a b) f" |
|
635 by (auto simp del: real_scaleR_def intro!: set_borel_measurable_continuous |
|
636 simp: continuous_on_eq_continuous_at einterval_iff f) |
|
637 have 3: "(\<lambda>i. LBINT x=l i..u i. f x) ----> B - A" |
|
638 apply (subst FTCi) |
|
639 apply (intro tendsto_intros) |
|
640 using B approx unfolding tendsto_at_iff_sequentially comp_def |
|
641 using tendsto_at_iff_sequentially[where 'a=real] |
|
642 apply (elim allE[of _ "\<lambda>i. ereal (u i)"], auto) |
|
643 using A approx unfolding tendsto_at_iff_sequentially comp_def |
|
644 by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto) |
|
645 show "(LBINT x=a..b. f x) = B - A" |
|
646 by (rule interval_integral_Icc_approx_nonneg [OF `a < b` approx 1 f_nonneg 2 3]) |
|
647 show "set_integrable lborel (einterval a b) f" |
|
648 by (rule interval_integral_Icc_approx_nonneg [OF `a < b` approx 1 f_nonneg 2 3]) |
|
649 qed |
|
650 |
|
651 lemma interval_integral_FTC_integrable: |
|
652 fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: ereal |
|
653 assumes "a < b" |
|
654 assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)" |
|
655 assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x" |
|
656 assumes f_integrable: "set_integrable lborel (einterval a b) f" |
|
657 assumes A: "((F \<circ> real) ---> A) (at_right a)" |
|
658 assumes B: "((F \<circ> real) ---> B) (at_left b)" |
|
659 shows "(LBINT x=a..b. f x) = B - A" |
|
660 proof - |
|
661 from einterval_Icc_approximation[OF `a < b`] guess u l . note approx = this |
|
662 have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x" |
|
663 by (rule order_less_le_trans, rule approx, force) |
|
664 have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b" |
|
665 by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) |
|
666 have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)" |
|
667 using assms approx |
|
668 by (auto simp add: less_imp_le min_def max_def |
|
669 intro!: f continuous_at_imp_continuous_on interval_integral_FTC_finite |
|
670 intro: has_vector_derivative_at_within) |
|
671 have "(\<lambda>i. LBINT x=l i..u i. f x) ----> B - A" |
|
672 apply (subst FTCi) |
|
673 apply (intro tendsto_intros) |
|
674 using B approx unfolding tendsto_at_iff_sequentially comp_def |
|
675 apply (elim allE[of _ "\<lambda>i. ereal (u i)"], auto) |
|
676 using A approx unfolding tendsto_at_iff_sequentially comp_def |
|
677 by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto) |
|
678 moreover have "(\<lambda>i. LBINT x=l i..u i. f x) ----> (LBINT x=a..b. f x)" |
|
679 by (rule interval_integral_Icc_approx_integrable [OF `a < b` approx f_integrable]) |
|
680 ultimately show ?thesis |
|
681 by (elim LIMSEQ_unique) |
|
682 qed |
|
683 |
|
684 (* |
|
685 The second Fundamental Theorem of Calculus and existence of antiderivatives on an |
|
686 einterval. |
|
687 *) |
|
688 |
|
689 lemma interval_integral_FTC2: |
|
690 fixes a b c :: real and f :: "real \<Rightarrow> 'a::euclidean_space" |
|
691 assumes "a \<le> c" "c \<le> b" |
|
692 and contf: "continuous_on {a..b} f" |
|
693 fixes x :: real |
|
694 assumes "a \<le> x" and "x \<le> b" |
|
695 shows "((\<lambda>u. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})" |
|
696 proof - |
|
697 let ?F = "(\<lambda>u. LBINT y=a..u. f y)" |
|
698 have intf: "set_integrable lborel {a..b} f" |
|
699 by (rule borel_integrable_atLeastAtMost', rule contf) |
|
700 have "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})" |
|
701 apply (intro integral_has_vector_derivative) |
|
702 using `a \<le> x` `x \<le> b` by (intro continuous_on_subset [OF contf], auto) |
|
703 then have "((\<lambda>u. integral {a..u} f) has_vector_derivative (f x)) (at x within {a..b})" |
|
704 by simp |
|
705 then have "(?F has_vector_derivative (f x)) (at x within {a..b})" |
|
706 by (rule has_vector_derivative_weaken) |
|
707 (auto intro!: assms interval_integral_eq_integral[symmetric] set_integrable_subset [OF intf]) |
|
708 then have "((\<lambda>x. (LBINT y=c..a. f y) + ?F x) has_vector_derivative (f x)) (at x within {a..b})" |
|
709 by (auto intro!: derivative_eq_intros) |
|
710 then show ?thesis |
|
711 proof (rule has_vector_derivative_weaken) |
|
712 fix u assume "u \<in> {a .. b}" |
|
713 then show "(LBINT y=c..a. f y) + (LBINT y=a..u. f y) = (LBINT y=c..u. f y)" |
|
714 using assms |
|
715 apply (intro interval_integral_sum) |
|
716 apply (auto simp add: interval_lebesgue_integrable_def simp del: real_scaleR_def) |
|
717 by (rule set_integrable_subset [OF intf], auto simp add: min_def max_def) |
|
718 qed (insert assms, auto) |
|
719 qed |
|
720 |
|
721 lemma einterval_antiderivative: |
|
722 fixes a b :: ereal and f :: "real \<Rightarrow> 'a::euclidean_space" |
|
723 assumes "a < b" and contf: "\<And>x :: real. a < x \<Longrightarrow> x < b \<Longrightarrow> isCont f x" |
|
724 shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)" |
|
725 proof - |
|
726 from einterval_nonempty [OF `a < b`] obtain c :: real where [simp]: "a < c" "c < b" |
|
727 by (auto simp add: einterval_def) |
|
728 let ?F = "(\<lambda>u. LBINT y=c..u. f y)" |
|
729 show ?thesis |
|
730 proof (rule exI, clarsimp) |
|
731 fix x :: real |
|
732 assume [simp]: "a < x" "x < b" |
|
733 have 1: "a < min c x" by simp |
|
734 from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x" |
|
735 by (auto simp add: einterval_def) |
|
736 have 2: "max c x < b" by simp |
|
737 from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b" |
|
738 by (auto simp add: einterval_def) |
|
739 show "(?F has_vector_derivative f x) (at x)" |
|
740 (* TODO: factor out the next three lines to has_field_derivative_within_open *) |
|
741 unfolding has_vector_derivative_def |
|
742 apply (subst has_derivative_within_open [of _ "{d<..<e}", symmetric], auto) |
|
743 apply (subst has_vector_derivative_def [symmetric]) |
|
744 apply (rule has_vector_derivative_within_subset [of _ _ _ "{d..e}"]) |
|
745 apply (rule interval_integral_FTC2, auto simp add: less_imp_le) |
|
746 apply (rule continuous_at_imp_continuous_on) |
|
747 apply (auto intro!: contf) |
|
748 apply (rule order_less_le_trans, rule `a < d`, auto) |
|
749 apply (rule order_le_less_trans) prefer 2 |
|
750 by (rule `e < b`, auto) |
|
751 qed |
|
752 qed |
|
753 |
|
754 (* |
|
755 The substitution theorem |
|
756 |
|
757 Once again, three versions: first, for finite intervals, and then two versions for |
|
758 arbitrary intervals. |
|
759 *) |
|
760 |
|
761 lemma interval_integral_substitution_finite: |
|
762 fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space" |
|
763 assumes "a \<le> b" |
|
764 and derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_real_derivative (g' x)) (at x within {a..b})" |
|
765 and contf : "continuous_on (g ` {a..b}) f" |
|
766 and contg': "continuous_on {a..b} g'" |
|
767 shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y" |
|
768 proof- |
|
769 have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})" |
|
770 using derivg unfolding has_field_derivative_iff_has_vector_derivative . |
|
771 then have contg [simp]: "continuous_on {a..b} g" |
|
772 by (rule continuous_on_vector_derivative) auto |
|
773 have 1: "\<And>u. min (g a) (g b) \<le> u \<Longrightarrow> u \<le> max (g a) (g b) \<Longrightarrow> |
|
774 \<exists>x\<in>{a..b}. u = g x" |
|
775 apply (case_tac "g a \<le> g b") |
|
776 apply (auto simp add: min_def max_def less_imp_le) |
|
777 apply (frule (1) IVT' [of g], auto simp add: assms) |
|
778 by (frule (1) IVT2' [of g], auto simp add: assms) |
|
779 from contg `a \<le> b` have "\<exists>c d. g ` {a..b} = {c..d} \<and> c \<le> d" |
|
780 by (elim continuous_image_closed_interval) |
|
781 then obtain c d where g_im: "g ` {a..b} = {c..d}" and "c \<le> d" by auto |
|
782 have "\<exists>F. \<forall>x\<in>{a..b}. (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))" |
|
783 apply (rule exI, auto, subst g_im) |
|
784 apply (rule interval_integral_FTC2 [of c c d]) |
|
785 using `c \<le> d` apply auto |
|
786 apply (rule continuous_on_subset [OF contf]) |
|
787 using g_im by auto |
|
788 then guess F .. |
|
789 then have derivF: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> |
|
790 (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))" by auto |
|
791 have contf2: "continuous_on {min (g a) (g b)..max (g a) (g b)} f" |
|
792 apply (rule continuous_on_subset [OF contf]) |
|
793 apply (auto simp add: image_def) |
|
794 by (erule 1) |
|
795 have contfg: "continuous_on {a..b} (\<lambda>x. f (g x))" |
|
796 by (blast intro: continuous_on_compose2 contf contg) |
|
797 have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)" |
|
798 apply (subst interval_integral_Icc, simp add: assms) |
|
799 apply (rule integral_FTC_atLeastAtMost[of a b "\<lambda>x. F (g x)", OF `a \<le> b`]) |
|
800 apply (rule vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def]) |
|
801 apply (auto intro!: continuous_on_scaleR contg' contfg) |
|
802 done |
|
803 moreover have "LBINT y=(g a)..(g b). f y = F (g b) - F (g a)" |
|
804 apply (rule interval_integral_FTC_finite) |
|
805 apply (rule contf2) |
|
806 apply (frule (1) 1, auto) |
|
807 apply (rule has_vector_derivative_within_subset [OF derivF]) |
|
808 apply (auto simp add: image_def) |
|
809 by (rule 1, auto) |
|
810 ultimately show ?thesis by simp |
|
811 qed |
|
812 |
|
813 (* TODO: is it possible to lift the assumption here that g' is nonnegative? *) |
|
814 |
|
815 lemma interval_integral_substitution_integrable: |
|
816 fixes f :: "real \<Rightarrow> 'a::euclidean_space" and a b u v :: ereal |
|
817 assumes "a < b" |
|
818 and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x" |
|
819 and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)" |
|
820 and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x" |
|
821 and g'_nonneg: "\<And>x. a \<le> ereal x \<Longrightarrow> ereal x \<le> b \<Longrightarrow> 0 \<le> g' x" |
|
822 and A: "((ereal \<circ> g \<circ> real) ---> A) (at_right a)" |
|
823 and B: "((ereal \<circ> g \<circ> real) ---> B) (at_left b)" |
|
824 and integrable: "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))" |
|
825 and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)" |
|
826 shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))" |
|
827 proof - |
|
828 from einterval_Icc_approximation[OF `a < b`] guess u l . note approx [simp] = this |
|
829 note less_imp_le [simp] |
|
830 have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x" |
|
831 by (rule order_less_le_trans, rule approx, force) |
|
832 have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b" |
|
833 by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) |
|
834 have [simp]: "\<And>i. l i < b" |
|
835 apply (rule order_less_trans) prefer 2 |
|
836 by (rule approx, auto, rule approx) |
|
837 have [simp]: "\<And>i. a < u i" |
|
838 by (rule order_less_trans, rule approx, auto, rule approx) |
|
839 have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx) |
|
840 have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx) |
|
841 have g_nondec [simp]: "\<And>x y. a < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < b \<Longrightarrow> g x \<le> g y" |
|
842 apply (erule DERIV_nonneg_imp_nondecreasing, auto) |
|
843 apply (rule exI, rule conjI, rule deriv_g) |
|
844 apply (erule order_less_le_trans, auto) |
|
845 apply (rule order_le_less_trans, subst ereal_less_eq(3), assumption, auto) |
|
846 apply (rule g'_nonneg) |
|
847 apply (rule less_imp_le, erule order_less_le_trans, auto) |
|
848 by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto) |
|
849 have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})" |
|
850 proof - |
|
851 have A2: "(\<lambda>i. g (l i)) ----> A" |
|
852 using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def) |
|
853 by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto) |
|
854 hence A3: "\<And>i. g (l i) \<ge> A" |
|
855 by (intro decseq_le, auto simp add: decseq_def) |
|
856 have B2: "(\<lambda>i. g (u i)) ----> B" |
|
857 using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def) |
|
858 by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto) |
|
859 hence B3: "\<And>i. g (u i) \<le> B" |
|
860 by (intro incseq_le, auto simp add: incseq_def) |
|
861 show "A \<le> B" |
|
862 apply (rule order_trans [OF A3 [of 0]]) |
|
863 apply (rule order_trans [OF _ B3 [of 0]]) |
|
864 by auto |
|
865 { fix x :: real |
|
866 assume "A < x" and "x < B" |
|
867 then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially" |
|
868 apply (intro eventually_conj order_tendstoD) |
|
869 by (rule A2, assumption, rule B2, assumption) |
|
870 hence "\<exists>i. g (l i) < x \<and> x < g (u i)" |
|
871 by (simp add: eventually_sequentially, auto) |
|
872 } note AB = this |
|
873 show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})" |
|
874 apply (auto simp add: einterval_def) |
|
875 apply (erule (1) AB) |
|
876 apply (rule order_le_less_trans, rule A3, simp) |
|
877 apply (rule order_less_le_trans) prefer 2 |
|
878 by (rule B3, simp) |
|
879 qed |
|
880 (* finally, the main argument *) |
|
881 { |
|
882 fix i |
|
883 have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)" |
|
884 apply (rule interval_integral_substitution_finite, auto) |
|
885 apply (rule DERIV_subset) |
|
886 unfolding has_field_derivative_iff_has_vector_derivative[symmetric] |
|
887 apply (rule deriv_g) |
|
888 apply (auto intro!: continuous_at_imp_continuous_on contf contg') |
|
889 done |
|
890 } note eq1 = this |
|
891 have "(\<lambda>i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) ----> (LBINT x=a..b. g' x *\<^sub>R f (g x))" |
|
892 apply (rule interval_integral_Icc_approx_integrable [OF `a < b` approx]) |
|
893 by (rule assms) |
|
894 hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x=a..b. g' x *\<^sub>R f (g x))" |
|
895 by (simp add: eq1) |
|
896 have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})" |
|
897 apply (auto simp add: incseq_def) |
|
898 apply (rule order_le_less_trans) |
|
899 prefer 2 apply (assumption, auto) |
|
900 by (erule order_less_le_trans, rule g_nondec, auto) |
|
901 have "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x = A..B. f x)" |
|
902 apply (subst interval_lebesgue_integral_le_eq, auto simp del: real_scaleR_def) |
|
903 apply (subst interval_lebesgue_integral_le_eq, rule `A \<le> B`) |
|
904 apply (subst un, rule set_integral_cont_up, auto simp del: real_scaleR_def) |
|
905 apply (rule incseq) |
|
906 apply (subst un [symmetric]) |
|
907 by (rule integrable2) |
|
908 thus ?thesis by (intro LIMSEQ_unique [OF _ 2]) |
|
909 qed |
|
910 |
|
911 (* TODO: the last two proofs are only slightly different. Factor out common part? |
|
912 An alternative: make the second one the main one, and then have another lemma |
|
913 that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *) |
|
914 |
|
915 lemma interval_integral_substitution_nonneg: |
|
916 fixes f g g':: "real \<Rightarrow> real" and a b u v :: ereal |
|
917 assumes "a < b" |
|
918 and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x" |
|
919 and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)" |
|
920 and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x" |
|
921 and f_nonneg: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> 0 \<le> f (g x)" (* TODO: make this AE? *) |
|
922 and g'_nonneg: "\<And>x. a \<le> ereal x \<Longrightarrow> ereal x \<le> b \<Longrightarrow> 0 \<le> g' x" |
|
923 and A: "((ereal \<circ> g \<circ> real) ---> A) (at_right a)" |
|
924 and B: "((ereal \<circ> g \<circ> real) ---> B) (at_left b)" |
|
925 and integrable_fg: "set_integrable lborel (einterval a b) (\<lambda>x. f (g x) * g' x)" |
|
926 shows |
|
927 "set_integrable lborel (einterval A B) f" |
|
928 "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))" |
|
929 proof - |
|
930 from einterval_Icc_approximation[OF `a < b`] guess u l . note approx [simp] = this |
|
931 note less_imp_le [simp] |
|
932 have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x" |
|
933 by (rule order_less_le_trans, rule approx, force) |
|
934 have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b" |
|
935 by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) |
|
936 have [simp]: "\<And>i. l i < b" |
|
937 apply (rule order_less_trans) prefer 2 |
|
938 by (rule approx, auto, rule approx) |
|
939 have [simp]: "\<And>i. a < u i" |
|
940 by (rule order_less_trans, rule approx, auto, rule approx) |
|
941 have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx) |
|
942 have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx) |
|
943 have g_nondec [simp]: "\<And>x y. a < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < b \<Longrightarrow> g x \<le> g y" |
|
944 apply (erule DERIV_nonneg_imp_nondecreasing, auto) |
|
945 apply (rule exI, rule conjI, rule deriv_g) |
|
946 apply (erule order_less_le_trans, auto) |
|
947 apply (rule order_le_less_trans, subst ereal_less_eq(3), assumption, auto) |
|
948 apply (rule g'_nonneg) |
|
949 apply (rule less_imp_le, erule order_less_le_trans, auto) |
|
950 by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto) |
|
951 have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})" |
|
952 proof - |
|
953 have A2: "(\<lambda>i. g (l i)) ----> A" |
|
954 using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def) |
|
955 by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto) |
|
956 hence A3: "\<And>i. g (l i) \<ge> A" |
|
957 by (intro decseq_le, auto simp add: decseq_def) |
|
958 have B2: "(\<lambda>i. g (u i)) ----> B" |
|
959 using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def) |
|
960 by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto) |
|
961 hence B3: "\<And>i. g (u i) \<le> B" |
|
962 by (intro incseq_le, auto simp add: incseq_def) |
|
963 show "A \<le> B" |
|
964 apply (rule order_trans [OF A3 [of 0]]) |
|
965 apply (rule order_trans [OF _ B3 [of 0]]) |
|
966 by auto |
|
967 { fix x :: real |
|
968 assume "A < x" and "x < B" |
|
969 then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially" |
|
970 apply (intro eventually_conj order_tendstoD) |
|
971 by (rule A2, assumption, rule B2, assumption) |
|
972 hence "\<exists>i. g (l i) < x \<and> x < g (u i)" |
|
973 by (simp add: eventually_sequentially, auto) |
|
974 } note AB = this |
|
975 show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})" |
|
976 apply (auto simp add: einterval_def) |
|
977 apply (erule (1) AB) |
|
978 apply (rule order_le_less_trans, rule A3, simp) |
|
979 apply (rule order_less_le_trans) prefer 2 |
|
980 by (rule B3, simp) |
|
981 qed |
|
982 (* finally, the main argument *) |
|
983 { |
|
984 fix i |
|
985 have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)" |
|
986 apply (rule interval_integral_substitution_finite, auto) |
|
987 apply (rule DERIV_subset, rule deriv_g, auto) |
|
988 apply (rule continuous_at_imp_continuous_on, auto, rule contf, auto) |
|
989 by (rule continuous_at_imp_continuous_on, auto, rule contg', auto) |
|
990 then have "(LBINT x=l i.. u i. (f (g x) * g' x)) = (LBINT y=g (l i)..g (u i). f y)" |
|
991 by (simp add: ac_simps) |
|
992 } note eq1 = this |
|
993 have "(\<lambda>i. LBINT x=l i..u i. f (g x) * g' x) |
|
994 ----> (LBINT x=a..b. f (g x) * g' x)" |
|
995 apply (rule interval_integral_Icc_approx_integrable [OF `a < b` approx]) |
|
996 by (rule assms) |
|
997 hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x=a..b. f (g x) * g' x)" |
|
998 by (simp add: eq1) |
|
999 have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})" |
|
1000 apply (auto simp add: incseq_def) |
|
1001 apply (rule order_le_less_trans) |
|
1002 prefer 2 apply assumption |
|
1003 apply (rule g_nondec, auto) |
|
1004 by (erule order_less_le_trans, rule g_nondec, auto) |
|
1005 have img: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> \<exists>c \<ge> l i. c \<le> u i \<and> x = g c" |
|
1006 apply (frule (1) IVT' [of g], auto) |
|
1007 apply (rule continuous_at_imp_continuous_on, auto) |
|
1008 by (rule DERIV_isCont, rule deriv_g, auto) |
|
1009 have nonneg_f2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> 0 \<le> f x" |
|
1010 by (frule (1) img, auto, rule f_nonneg, auto) |
|
1011 have contf_2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> isCont f x" |
|
1012 by (frule (1) img, auto, rule contf, auto) |
|
1013 have integrable: "set_integrable lborel (\<Union>i. {g (l i)<..<g (u i)}) f" |
|
1014 apply (rule pos_integrable_to_top, auto simp del: real_scaleR_def) |
|
1015 apply (rule incseq) |
|
1016 apply (rule nonneg_f2, erule less_imp_le, erule less_imp_le) |
|
1017 apply (rule set_integrable_subset) |
|
1018 apply (rule borel_integrable_atLeastAtMost') |
|
1019 apply (rule continuous_at_imp_continuous_on) |
|
1020 apply (clarsimp, erule (1) contf_2, auto) |
|
1021 apply (erule less_imp_le)+ |
|
1022 using 2 unfolding interval_lebesgue_integral_def |
|
1023 by auto |
|
1024 thus "set_integrable lborel (einterval A B) f" |
|
1025 by (simp add: un) |
|
1026 |
|
1027 have "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))" |
|
1028 proof (rule interval_integral_substitution_integrable) |
|
1029 show "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))" |
|
1030 using integrable_fg by (simp add: ac_simps) |
|
1031 qed fact+ |
|
1032 then show "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))" |
|
1033 by (simp add: ac_simps) |
|
1034 qed |
|
1035 |
|
1036 |
|
1037 syntax |
|
1038 "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex" |
|
1039 ("(2CLBINT _. _)" [0,60] 60) |
|
1040 |
|
1041 translations |
|
1042 "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)" |
|
1043 |
|
1044 syntax |
|
1045 "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex" |
|
1046 ("(3CLBINT _:_. _)" [0,60,61] 60) |
|
1047 |
|
1048 translations |
|
1049 "CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)" |
|
1050 |
|
1051 abbreviation complex_interval_lebesgue_integral :: |
|
1052 "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> complex" where |
|
1053 "complex_interval_lebesgue_integral M a b f \<equiv> interval_lebesgue_integral M a b f" |
|
1054 |
|
1055 abbreviation complex_interval_lebesgue_integrable :: |
|
1056 "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool" where |
|
1057 "complex_interval_lebesgue_integrable M a b f \<equiv> interval_lebesgue_integrable M a b f" |
|
1058 |
|
1059 syntax |
|
1060 "_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex" |
|
1061 ("(4CLBINT _=_.._. _)" [0,60,60,61] 60) |
|
1062 |
|
1063 translations |
|
1064 "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)" |
|
1065 |
|
1066 lemma interval_integral_norm: |
|
1067 fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" |
|
1068 shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow> |
|
1069 norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)" |
|
1070 using integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"] |
|
1071 by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def) |
|
1072 |
|
1073 lemma interval_integral_norm2: |
|
1074 "interval_lebesgue_integrable lborel a b f \<Longrightarrow> |
|
1075 norm (LBINT t=a..b. f t) \<le> abs (LBINT t=a..b. norm (f t))" |
|
1076 proof (induct a b rule: linorder_wlog) |
|
1077 case (sym a b) then show ?case |
|
1078 by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b]) |
|
1079 next |
|
1080 case (le a b) |
|
1081 then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)" |
|
1082 using integrable_norm[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"] |
|
1083 by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def |
|
1084 intro!: integral_nonneg_AE abs_of_nonneg) |
|
1085 then show ?case |
|
1086 using le by (simp add: interval_integral_norm) |
|
1087 qed |
|
1088 |
|
1089 (* TODO: should we have a library of facts like these? *) |
|
1090 lemma integral_cos: "t \<noteq> 0 \<Longrightarrow> LBINT x=a..b. cos (t * x) = sin (t * b) / t - sin (t * a) / t" |
|
1091 apply (intro interval_integral_FTC_finite continuous_intros) |
|
1092 by (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative[symmetric]) |
|
1093 |
|
1094 |
|
1095 end |