2 Author: Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU) |
2 Author: Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU) |
3 |
3 |
4 Lebesgue integral over an interval (with endpoints possibly +-\<infinity>) |
4 Lebesgue integral over an interval (with endpoints possibly +-\<infinity>) |
5 *) |
5 *) |
6 |
6 |
7 theory Interval_Integral |
7 theory Interval_Integral (*FIX ME rename? Lebesgue *) |
8 imports Equivalence_Lebesgue_Henstock_Integration |
8 imports Equivalence_Lebesgue_Henstock_Integration |
9 begin |
9 begin |
10 |
10 |
11 lemma%important continuous_on_vector_derivative: |
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" |
12 "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f" |
13 by%unimportant (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous) |
13 by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous) |
14 |
14 |
15 definition%important "einterval a b = {x. a < ereal x \<and> ereal x < b}" |
15 definition "einterval a b = {x. a < ereal x \<and> ereal x < b}" |
16 |
16 |
17 lemma einterval_eq[simp]: |
17 lemma einterval_eq[simp]: |
18 shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}" |
18 shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}" |
19 and einterval_eq_Ici: "einterval (ereal a) \<infinity> = {a <..}" |
19 and einterval_eq_Ici: "einterval (ereal a) \<infinity> = {a <..}" |
20 and einterval_eq_Iic: "einterval (- \<infinity>) (ereal b) = {..< b}" |
20 and einterval_eq_Iic: "einterval (- \<infinity>) (ereal b) = {..< b}" |
35 (auto simp: einterval_def intro!: open_Collect_conj open_Collect_less continuous_intros) |
35 (auto simp: einterval_def intro!: open_Collect_conj open_Collect_less continuous_intros) |
36 |
36 |
37 lemma borel_einterval[measurable]: "einterval a b \<in> sets borel" |
37 lemma borel_einterval[measurable]: "einterval a b \<in> sets borel" |
38 unfolding einterval_def by measurable |
38 unfolding einterval_def by measurable |
39 |
39 |
40 subsection\<open>Approximating a (possibly infinite) interval\<close> |
40 subsection%important \<open>Approximating a (possibly infinite) interval\<close> |
41 |
41 |
42 lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))" |
42 lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))" |
43 unfolding filterlim_def by (auto intro: le_supI1) |
43 unfolding filterlim_def by (auto intro: le_supI1) |
44 |
44 |
45 lemma%important ereal_incseq_approx: |
45 lemma ereal_incseq_approx: |
46 fixes a b :: ereal |
46 fixes a b :: ereal |
47 assumes "a < b" |
47 assumes "a < b" |
48 obtains X :: "nat \<Rightarrow> real" where "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b" |
48 obtains X :: "nat \<Rightarrow> real" where "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b" |
49 proof%unimportant (cases b) |
49 proof (cases b) |
50 case PInf |
50 case PInf |
51 with \<open>a < b\<close> have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)" |
51 with \<open>a < b\<close> have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)" |
52 by (cases a) auto |
52 by (cases a) auto |
53 moreover have "(\<lambda>x. ereal (real (Suc x))) \<longlonglongrightarrow> \<infinity>" |
53 moreover have "(\<lambda>x. ereal (real (Suc x))) \<longlonglongrightarrow> \<infinity>" |
54 by (simp add: Lim_PInfty LIMSEQ_Suc_iff) (metis le_SucI of_nat_Suc of_nat_mono order_trans real_arch_simple) |
54 by (simp add: Lim_PInfty LIMSEQ_Suc_iff) (metis le_SucI of_nat_Suc of_nat_mono order_trans real_arch_simple) |
76 ultimately show thesis |
76 ultimately show thesis |
77 by (intro that[of "\<lambda>i. b' - d / Suc (Suc i)"]) |
77 by (intro that[of "\<lambda>i. b' - d / Suc (Suc i)"]) |
78 (auto simp: real incseq_def intro!: divide_left_mono) |
78 (auto simp: real incseq_def intro!: divide_left_mono) |
79 qed (insert \<open>a < b\<close>, auto) |
79 qed (insert \<open>a < b\<close>, auto) |
80 |
80 |
81 lemma%important ereal_decseq_approx: |
81 lemma ereal_decseq_approx: |
82 fixes a b :: ereal |
82 fixes a b :: ereal |
83 assumes "a < b" |
83 assumes "a < b" |
84 obtains X :: "nat \<Rightarrow> real" where |
84 obtains X :: "nat \<Rightarrow> real" where |
85 "decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> a" |
85 "decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> a" |
86 proof%unimportant - |
86 proof - |
87 have "-b < -a" using \<open>a < b\<close> by simp |
87 have "-b < -a" using \<open>a < b\<close> by simp |
88 from ereal_incseq_approx[OF this] guess X . |
88 from ereal_incseq_approx[OF this] guess X . |
89 then show thesis |
89 then show thesis |
90 apply (intro that[of "\<lambda>i. - X i"]) |
90 apply (intro that[of "\<lambda>i. - X i"]) |
91 apply (auto simp: decseq_def incseq_def simp flip: uminus_ereal.simps) |
91 apply (auto simp: decseq_def incseq_def simp flip: uminus_ereal.simps) |
92 apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+ |
92 apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+ |
93 done |
93 done |
94 qed |
94 qed |
95 |
95 |
96 lemma%important einterval_Icc_approximation: |
96 proposition einterval_Icc_approximation: |
97 fixes a b :: ereal |
97 fixes a b :: ereal |
98 assumes "a < b" |
98 assumes "a < b" |
99 obtains u l :: "nat \<Rightarrow> real" where |
99 obtains u l :: "nat \<Rightarrow> real" where |
100 "einterval a b = (\<Union>i. {l i .. u i})" |
100 "einterval a b = (\<Union>i. {l i .. u i})" |
101 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
101 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
102 "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
102 "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
103 proof%unimportant - |
103 proof - |
104 from dense[OF \<open>a < b\<close>] obtain c where "a < c" "c < b" by safe |
104 from dense[OF \<open>a < b\<close>] obtain c where "a < c" "c < b" by safe |
105 from ereal_incseq_approx[OF \<open>c < b\<close>] guess u . note u = this |
105 from ereal_incseq_approx[OF \<open>c < b\<close>] guess u . note u = this |
106 from ereal_decseq_approx[OF \<open>a < c\<close>] guess l . note l = this |
106 from ereal_decseq_approx[OF \<open>a < c\<close>] guess l . note l = this |
107 { fix i from less_trans[OF \<open>l i < c\<close> \<open>c < u i\<close>] have "l i < u i" by simp } |
107 { fix i from less_trans[OF \<open>l i < c\<close> \<open>c < u i\<close>] have "l i < u i" by simp } |
108 have "einterval a b = (\<Union>i. {l i .. u i})" |
108 have "einterval a b = (\<Union>i. {l i .. u i})" |
200 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}" |
200 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}" |
201 shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow> |
201 shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow> |
202 interval_lebesgue_integrable M a b (\<lambda>x. c * f x)" |
202 interval_lebesgue_integrable M a b (\<lambda>x. c * f x)" |
203 by (simp add: interval_lebesgue_integrable_def) |
203 by (simp add: interval_lebesgue_integrable_def) |
204 |
204 |
205 lemma%important interval_lebesgue_integrable_mult_left [intro, simp]: |
205 lemma interval_lebesgue_integrable_mult_left [intro, simp]: |
206 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}" |
206 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}" |
207 shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow> |
207 shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow> |
208 interval_lebesgue_integrable M a b (\<lambda>x. f x * c)" |
208 interval_lebesgue_integrable M a b (\<lambda>x. f x * c)" |
209 by%unimportant (simp add: interval_lebesgue_integrable_def) |
209 by (simp add: interval_lebesgue_integrable_def) |
210 |
210 |
211 lemma%important interval_lebesgue_integrable_divide [intro, simp]: |
211 lemma interval_lebesgue_integrable_divide [intro, simp]: |
212 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}" |
212 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}" |
213 shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow> |
213 shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow> |
214 interval_lebesgue_integrable M a b (\<lambda>x. f x / c)" |
214 interval_lebesgue_integrable M a b (\<lambda>x. f x / c)" |
215 by%unimportant (simp add: interval_lebesgue_integrable_def) |
215 by (simp add: interval_lebesgue_integrable_def) |
216 |
216 |
217 lemma interval_lebesgue_integral_mult_right [simp]: |
217 lemma interval_lebesgue_integral_mult_right [simp]: |
218 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}" |
218 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}" |
219 shows "interval_lebesgue_integral M a b (\<lambda>x. c * f x) = |
219 shows "interval_lebesgue_integral M a b (\<lambda>x. c * f x) = |
220 c * interval_lebesgue_integral M a b f" |
220 c * interval_lebesgue_integral M a b f" |
221 by (simp add: interval_lebesgue_integral_def) |
221 by (simp add: interval_lebesgue_integral_def) |
222 |
222 |
223 lemma%important interval_lebesgue_integral_mult_left [simp]: |
223 lemma interval_lebesgue_integral_mult_left [simp]: |
224 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}" |
224 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}" |
225 shows "interval_lebesgue_integral M a b (\<lambda>x. f x * c) = |
225 shows "interval_lebesgue_integral M a b (\<lambda>x. f x * c) = |
226 interval_lebesgue_integral M a b f * c" |
226 interval_lebesgue_integral M a b f * c" |
227 by%unimportant (simp add: interval_lebesgue_integral_def) |
227 by (simp add: interval_lebesgue_integral_def) |
228 |
228 |
229 lemma interval_lebesgue_integral_divide [simp]: |
229 lemma interval_lebesgue_integral_divide [simp]: |
230 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}" |
230 fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}" |
231 shows "interval_lebesgue_integral M a b (\<lambda>x. f x / c) = |
231 shows "interval_lebesgue_integral M a b (\<lambda>x. f x / c) = |
232 interval_lebesgue_integral M a b f / c" |
232 interval_lebesgue_integral M a b f / c" |
240 "interval_lebesgue_integral M a b (\<lambda>x. complex_of_real (f x)) = |
240 "interval_lebesgue_integral M a b (\<lambda>x. complex_of_real (f x)) = |
241 of_real (interval_lebesgue_integral M a b f)" |
241 of_real (interval_lebesgue_integral M a b f)" |
242 unfolding interval_lebesgue_integral_def |
242 unfolding interval_lebesgue_integral_def |
243 by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real) |
243 by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real) |
244 |
244 |
245 lemma%important interval_lebesgue_integral_le_eq: |
245 lemma interval_lebesgue_integral_le_eq: |
246 fixes a b f |
246 fixes a b f |
247 assumes "a \<le> b" |
247 assumes "a \<le> b" |
248 shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)" |
248 shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)" |
249 using%unimportant assms by (auto simp: interval_lebesgue_integral_def) |
249 using assms by (auto simp: interval_lebesgue_integral_def) |
250 |
250 |
251 lemma interval_lebesgue_integral_gt_eq: |
251 lemma interval_lebesgue_integral_gt_eq: |
252 fixes a b f |
252 fixes a b f |
253 assumes "a > b" |
253 assumes "a > b" |
254 shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)" |
254 shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)" |
269 lemma interval_integrable_endpoints_reverse: |
269 lemma interval_integrable_endpoints_reverse: |
270 "interval_lebesgue_integrable lborel a b f \<longleftrightarrow> |
270 "interval_lebesgue_integrable lborel a b f \<longleftrightarrow> |
271 interval_lebesgue_integrable lborel b a f" |
271 interval_lebesgue_integrable lborel b a f" |
272 by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same) |
272 by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same) |
273 |
273 |
274 lemma%important interval_integral_reflect: |
274 lemma interval_integral_reflect: |
275 "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))" |
275 "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))" |
276 proof%unimportant (induct a b rule: linorder_wlog) |
276 proof (induct a b rule: linorder_wlog) |
277 case (sym a b) then show ?case |
277 case (sym a b) then show ?case |
278 by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse |
278 by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse |
279 split: if_split_asm) |
279 split: if_split_asm) |
280 next |
280 next |
281 case (le a b) |
281 case (le a b) |
297 by (auto simp: interval_lebesgue_integral_le_eq interval_lebesgue_integrable_def) |
297 by (auto simp: interval_lebesgue_integral_le_eq interval_lebesgue_integrable_def) |
298 |
298 |
299 lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..\<infinity> | M. f x) = (LINT x : {a<..} | M. f x)" |
299 lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..\<infinity> | M. f x) = (LINT x : {a<..} | M. f x)" |
300 unfolding interval_lebesgue_integral_def by auto |
300 unfolding interval_lebesgue_integral_def by auto |
301 |
301 |
302 lemma%important interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) = |
302 proposition interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) = |
303 (set_integrable M {a<..} f)" |
303 (set_integrable M {a<..} f)" |
304 unfolding%unimportant interval_lebesgue_integrable_def by auto |
304 unfolding%unimportant interval_lebesgue_integrable_def by auto |
305 |
305 |
306 subsection%important\<open>Basic properties of integration over an interval wrt lebesgue measure\<close> |
306 subsection%important\<open>Basic properties of integration over an interval wrt lebesgue measure\<close> |
307 |
307 |
315 fixes a b c :: real |
315 fixes a b c :: real |
316 shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)" |
316 shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)" |
317 unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq |
317 unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq |
318 by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def) |
318 by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def) |
319 |
319 |
320 lemma%important interval_integral_cong_AE: |
320 lemma interval_integral_cong_AE: |
321 assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel" |
321 assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel" |
322 assumes "AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x" |
322 assumes "AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x" |
323 shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g" |
323 shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g" |
324 using assms |
324 using assms |
325 proof%unimportant (induct a b rule: linorder_wlog) |
325 proof (induct a b rule: linorder_wlog) |
326 case (sym a b) then show ?case |
326 case (sym a b) then show ?case |
327 by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b]) |
327 by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b]) |
328 next |
328 next |
329 case (le a b) then show ?case |
329 case (le a b) then show ?case |
330 by (auto simp: interval_lebesgue_integral_def max_def min_def |
330 by (auto simp: interval_lebesgue_integral_def max_def min_def |
331 intro!: set_lebesgue_integral_cong_AE) |
331 intro!: set_lebesgue_integral_cong_AE) |
332 qed |
332 qed |
333 |
333 |
334 lemma%important interval_integral_cong: |
334 lemma interval_integral_cong: |
335 assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x" |
335 assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x" |
336 shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g" |
336 shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g" |
337 using assms |
337 using assms |
338 proof%unimportant (induct a b rule: linorder_wlog) |
338 proof (induct a b rule: linorder_wlog) |
339 case (sym a b) then show ?case |
339 case (sym a b) then show ?case |
340 by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b]) |
340 by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b]) |
341 next |
341 next |
342 case (le a b) then show ?case |
342 case (le a b) then show ?case |
343 by (auto simp: interval_lebesgue_integral_def max_def min_def |
343 by (auto simp: interval_lebesgue_integral_def max_def min_def |
405 unfolding interval_lebesgue_integral_def set_lebesgue_integral_def |
405 unfolding interval_lebesgue_integral_def set_lebesgue_integral_def |
406 apply (intro if_cong refl arg_cong[where f="\<lambda>x. - x"] integral_discrete_difference[of X] assms) |
406 apply (intro if_cong refl arg_cong[where f="\<lambda>x. - x"] integral_discrete_difference[of X] assms) |
407 apply (auto simp: eq anti_eq einterval_iff split: split_indicator) |
407 apply (auto simp: eq anti_eq einterval_iff split: split_indicator) |
408 done |
408 done |
409 |
409 |
410 lemma%important interval_integral_sum: |
410 lemma interval_integral_sum: |
411 fixes a b c :: ereal |
411 fixes a b c :: ereal |
412 assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f" |
412 assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f" |
413 shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)" |
413 shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)" |
414 proof%unimportant - |
414 proof - |
415 let ?I = "\<lambda>a b. LBINT x=a..b. f x" |
415 let ?I = "\<lambda>a b. LBINT x=a..b. f x" |
416 { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c" |
416 { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c" |
417 then have ord: "a \<le> b" "b \<le> c" "a \<le> c" and f': "set_integrable lborel (einterval a c) f" |
417 then have ord: "a \<le> b" "b \<le> c" "a \<le> c" and f': "set_integrable lborel (einterval a c) f" |
418 by (auto simp: interval_lebesgue_integrable_def) |
418 by (auto simp: interval_lebesgue_integrable_def) |
419 then have f: "set_borel_measurable borel (einterval a c) f" |
419 then have f: "set_borel_measurable borel (einterval a c) f" |
444 using integrable |
444 using integrable |
445 by (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases]) |
445 by (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases]) |
446 (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3) |
446 (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3) |
447 qed |
447 qed |
448 |
448 |
449 lemma%important interval_integrable_isCont: |
449 lemma interval_integrable_isCont: |
450 fixes a b and f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}" |
450 fixes a b and f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}" |
451 shows "(\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> isCont f x) \<Longrightarrow> |
451 shows "(\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> isCont f x) \<Longrightarrow> |
452 interval_lebesgue_integrable lborel a b f" |
452 interval_lebesgue_integrable lborel a b f" |
453 proof%unimportant (induct a b rule: linorder_wlog) |
453 proof (induct a b rule: linorder_wlog) |
454 case (le a b) then show ?case |
454 case (le a b) then show ?case |
455 unfolding interval_lebesgue_integrable_def set_integrable_def |
455 unfolding interval_lebesgue_integrable_def set_integrable_def |
456 by (auto simp: interval_lebesgue_integrable_def |
456 by (auto simp: interval_lebesgue_integrable_def |
457 intro!: set_integrable_subset[unfolded set_integrable_def, OF borel_integrable_compact[of "{a .. b}"]] |
457 intro!: set_integrable_subset[unfolded set_integrable_def, OF borel_integrable_compact[of "{a .. b}"]] |
458 continuous_at_imp_continuous_on) |
458 continuous_at_imp_continuous_on) |
491 assumes f_measurable: "set_borel_measurable lborel (einterval a b) f" |
491 assumes f_measurable: "set_borel_measurable lborel (einterval a b) f" |
492 assumes lbint_lim: "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> C" |
492 assumes lbint_lim: "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> C" |
493 shows |
493 shows |
494 "set_integrable lborel (einterval a b) f" |
494 "set_integrable lborel (einterval a b) f" |
495 "(LBINT x=a..b. f x) = C" |
495 "(LBINT x=a..b. f x) = C" |
496 proof%unimportant - |
496 proof - |
497 have 1 [unfolded set_integrable_def]: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable) |
497 have 1 [unfolded set_integrable_def]: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable) |
498 have 2: "AE x in lborel. mono (\<lambda>n. indicator {l n..u n} x *\<^sub>R f x)" |
498 have 2: "AE x in lborel. mono (\<lambda>n. indicator {l n..u n} x *\<^sub>R f x)" |
499 proof - |
499 proof - |
500 from f_nonneg have "AE x in lborel. \<forall>i. l i \<le> x \<longrightarrow> x \<le> u i \<longrightarrow> 0 \<le> f x" |
500 from f_nonneg have "AE x in lborel. \<forall>i. l i \<le> x \<longrightarrow> x \<le> u i \<longrightarrow> 0 \<le> f x" |
501 by eventually_elim |
501 by eventually_elim |
532 show "set_integrable lborel (einterval a b) f" |
532 show "set_integrable lborel (einterval a b) f" |
533 unfolding set_integrable_def |
533 unfolding set_integrable_def |
534 by (rule integrable_monotone_convergence[OF 1 2 3 4 5]) |
534 by (rule integrable_monotone_convergence[OF 1 2 3 4 5]) |
535 qed |
535 qed |
536 |
536 |
537 lemma%important interval_integral_Icc_approx_integrable: |
537 proposition interval_integral_Icc_approx_integrable: |
538 fixes u l :: "nat \<Rightarrow> real" and a b :: ereal |
538 fixes u l :: "nat \<Rightarrow> real" and a b :: ereal |
539 fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}" |
539 fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}" |
540 assumes "a < b" |
540 assumes "a < b" |
541 assumes approx: "einterval a b = (\<Union>i. {l i .. u i})" |
541 assumes approx: "einterval a b = (\<Union>i. {l i .. u i})" |
542 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
542 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
543 "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
543 "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
544 assumes f_integrable: "set_integrable lborel (einterval a b) f" |
544 assumes f_integrable: "set_integrable lborel (einterval a b) f" |
545 shows "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)" |
545 shows "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)" |
546 proof%unimportant - |
546 proof - |
547 have "(\<lambda>i. LBINT x:{l i.. u i}. f x) \<longlonglongrightarrow> (LBINT x:einterval a b. f x)" |
547 have "(\<lambda>i. LBINT x:{l i.. u i}. f x) \<longlonglongrightarrow> (LBINT x:einterval a b. f x)" |
548 unfolding set_lebesgue_integral_def |
548 unfolding set_lebesgue_integral_def |
549 proof (rule integral_dominated_convergence) |
549 proof (rule integral_dominated_convergence) |
550 show "integrable lborel (\<lambda>x. norm (indicator (einterval a b) x *\<^sub>R f x))" |
550 show "integrable lborel (\<lambda>x. norm (indicator (einterval a b) x *\<^sub>R f x))" |
551 using f_integrable integrable_norm set_integrable_def by blast |
551 using f_integrable integrable_norm set_integrable_def by blast |
578 |
578 |
579 (* |
579 (* |
580 TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.) |
580 TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.) |
581 *) |
581 *) |
582 |
582 |
583 lemma%important interval_integral_FTC_finite: |
583 lemma interval_integral_FTC_finite: |
584 fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real |
584 fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real |
585 assumes f: "continuous_on {min a b..max a b} f" |
585 assumes f: "continuous_on {min a b..max a b} f" |
586 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 |
586 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 |
587 {min a b..max a b})" |
587 {min a b..max a b})" |
588 shows "(LBINT x=a..b. f x) = F b - F a" |
588 shows "(LBINT x=a..b. f x) = F b - F a" |
589 proof%unimportant (cases "a \<le> b") |
589 proof (cases "a \<le> b") |
590 case True |
590 case True |
591 have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)" |
591 have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)" |
592 by (simp add: True interval_integral_Icc set_lebesgue_integral_def) |
592 by (simp add: True interval_integral_Icc set_lebesgue_integral_def) |
593 also have "\<dots> = F b - F a" |
593 also have "\<dots> = F b - F a" |
594 proof (rule integral_FTC_atLeastAtMost [OF True]) |
594 proof (rule integral_FTC_atLeastAtMost [OF True]) |
615 finally show ?thesis |
615 finally show ?thesis |
616 by (metis interval_integral_endpoints_reverse) |
616 by (metis interval_integral_endpoints_reverse) |
617 qed |
617 qed |
618 |
618 |
619 |
619 |
620 lemma%important interval_integral_FTC_nonneg: |
620 lemma interval_integral_FTC_nonneg: |
621 fixes f F :: "real \<Rightarrow> real" and a b :: ereal |
621 fixes f F :: "real \<Rightarrow> real" and a b :: ereal |
622 assumes "a < b" |
622 assumes "a < b" |
623 assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x" |
623 assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x" |
624 assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x" |
624 assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x" |
625 assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x" |
625 assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x" |
626 assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)" |
626 assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)" |
627 assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)" |
627 assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)" |
628 shows |
628 shows |
629 "set_integrable lborel (einterval a b) f" |
629 "set_integrable lborel (einterval a b) f" |
630 "(LBINT x=a..b. f x) = B - A" |
630 "(LBINT x=a..b. f x) = B - A" |
631 proof%unimportant - |
631 proof - |
632 obtain u l where approx: |
632 obtain u l where approx: |
633 "einterval a b = (\<Union>i. {l i .. u i})" |
633 "einterval a b = (\<Union>i. {l i .. u i})" |
634 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
634 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
635 "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
635 "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
636 by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>]) |
636 by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>]) |
667 by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3]) |
667 by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3]) |
668 show "set_integrable lborel (einterval a b) f" |
668 show "set_integrable lborel (einterval a b) f" |
669 by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3]) |
669 by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3]) |
670 qed |
670 qed |
671 |
671 |
672 lemma%important interval_integral_FTC_integrable: |
672 theorem interval_integral_FTC_integrable: |
673 fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: ereal |
673 fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: ereal |
674 assumes "a < b" |
674 assumes "a < b" |
675 assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)" |
675 assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)" |
676 assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x" |
676 assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x" |
677 assumes f_integrable: "set_integrable lborel (einterval a b) f" |
677 assumes f_integrable: "set_integrable lborel (einterval a b) f" |
678 assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)" |
678 assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)" |
679 assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)" |
679 assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)" |
680 shows "(LBINT x=a..b. f x) = B - A" |
680 shows "(LBINT x=a..b. f x) = B - A" |
681 proof%unimportant - |
681 proof - |
682 obtain u l where approx: |
682 obtain u l where approx: |
683 "einterval a b = (\<Union>i. {l i .. u i})" |
683 "einterval a b = (\<Union>i. {l i .. u i})" |
684 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
684 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
685 "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
685 "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
686 by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>]) |
686 by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>]) |
712 (* |
712 (* |
713 The second Fundamental Theorem of Calculus and existence of antiderivatives on an |
713 The second Fundamental Theorem of Calculus and existence of antiderivatives on an |
714 einterval. |
714 einterval. |
715 *) |
715 *) |
716 |
716 |
717 lemma%important interval_integral_FTC2: |
717 theorem interval_integral_FTC2: |
718 fixes a b c :: real and f :: "real \<Rightarrow> 'a::euclidean_space" |
718 fixes a b c :: real and f :: "real \<Rightarrow> 'a::euclidean_space" |
719 assumes "a \<le> c" "c \<le> b" |
719 assumes "a \<le> c" "c \<le> b" |
720 and contf: "continuous_on {a..b} f" |
720 and contf: "continuous_on {a..b} f" |
721 fixes x :: real |
721 fixes x :: real |
722 assumes "a \<le> x" and "x \<le> b" |
722 assumes "a \<le> x" and "x \<le> b" |
723 shows "((\<lambda>u. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})" |
723 shows "((\<lambda>u. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})" |
724 proof%unimportant - |
724 proof - |
725 let ?F = "(\<lambda>u. LBINT y=a..u. f y)" |
725 let ?F = "(\<lambda>u. LBINT y=a..u. f y)" |
726 have intf: "set_integrable lborel {a..b} f" |
726 have intf: "set_integrable lborel {a..b} f" |
727 by (rule borel_integrable_atLeastAtMost', rule contf) |
727 by (rule borel_integrable_atLeastAtMost', rule contf) |
728 have "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})" |
728 have "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})" |
729 using \<open>a \<le> x\<close> \<open>x \<le> b\<close> |
729 using \<open>a \<le> x\<close> \<open>x \<le> b\<close> |
744 apply (auto simp: interval_lebesgue_integrable_def simp del: real_scaleR_def) |
744 apply (auto simp: interval_lebesgue_integrable_def simp del: real_scaleR_def) |
745 by (rule set_integrable_subset [OF intf], auto simp: min_def max_def) |
745 by (rule set_integrable_subset [OF intf], auto simp: min_def max_def) |
746 qed (insert assms, auto) |
746 qed (insert assms, auto) |
747 qed |
747 qed |
748 |
748 |
749 lemma%important einterval_antiderivative: |
749 proposition einterval_antiderivative: |
750 fixes a b :: ereal and f :: "real \<Rightarrow> 'a::euclidean_space" |
750 fixes a b :: ereal and f :: "real \<Rightarrow> 'a::euclidean_space" |
751 assumes "a < b" and contf: "\<And>x :: real. a < x \<Longrightarrow> x < b \<Longrightarrow> isCont f x" |
751 assumes "a < b" and contf: "\<And>x :: real. a < x \<Longrightarrow> x < b \<Longrightarrow> isCont f x" |
752 shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)" |
752 shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)" |
753 proof%unimportant - |
753 proof - |
754 from einterval_nonempty [OF \<open>a < b\<close>] obtain c :: real where [simp]: "a < c" "c < b" |
754 from einterval_nonempty [OF \<open>a < b\<close>] obtain c :: real where [simp]: "a < c" "c < b" |
755 by (auto simp: einterval_def) |
755 by (auto simp: einterval_def) |
756 let ?F = "(\<lambda>u. LBINT y=c..u. f y)" |
756 let ?F = "(\<lambda>u. LBINT y=c..u. f y)" |
757 show ?thesis |
757 show ?thesis |
758 proof (rule exI, clarsimp) |
758 proof (rule exI, clarsimp) |
784 subsection%important\<open>The substitution theorem\<close> |
784 subsection%important\<open>The substitution theorem\<close> |
785 |
785 |
786 text\<open>Once again, three versions: first, for finite intervals, and then two versions for |
786 text\<open>Once again, three versions: first, for finite intervals, and then two versions for |
787 arbitrary intervals.\<close> |
787 arbitrary intervals.\<close> |
788 |
788 |
789 lemma%important interval_integral_substitution_finite: |
789 theorem interval_integral_substitution_finite: |
790 fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space" |
790 fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space" |
791 assumes "a \<le> b" |
791 assumes "a \<le> b" |
792 and derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_real_derivative (g' x)) (at x within {a..b})" |
792 and derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_real_derivative (g' x)) (at x within {a..b})" |
793 and contf : "continuous_on (g ` {a..b}) f" |
793 and contf : "continuous_on (g ` {a..b}) f" |
794 and contg': "continuous_on {a..b} g'" |
794 and contg': "continuous_on {a..b} g'" |
795 shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y" |
795 shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y" |
796 proof%unimportant- |
796 proof- |
797 have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})" |
797 have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})" |
798 using derivg unfolding has_field_derivative_iff_has_vector_derivative . |
798 using derivg unfolding has_field_derivative_iff_has_vector_derivative . |
799 then have contg [simp]: "continuous_on {a..b} g" |
799 then have contg [simp]: "continuous_on {a..b} g" |
800 by (rule continuous_on_vector_derivative) auto |
800 by (rule continuous_on_vector_derivative) auto |
801 have 1: "\<exists>x\<in>{a..b}. u = g x" if "min (g a) (g b) \<le> u" "u \<le> max (g a) (g b)" for u |
801 have 1: "\<exists>x\<in>{a..b}. u = g x" if "min (g a) (g b) \<le> u" "u \<le> max (g a) (g b)" for u |
831 ultimately show ?thesis by simp |
831 ultimately show ?thesis by simp |
832 qed |
832 qed |
833 |
833 |
834 (* TODO: is it possible to lift the assumption here that g' is nonnegative? *) |
834 (* TODO: is it possible to lift the assumption here that g' is nonnegative? *) |
835 |
835 |
836 lemma%important interval_integral_substitution_integrable: |
836 theorem interval_integral_substitution_integrable: |
837 fixes f :: "real \<Rightarrow> 'a::euclidean_space" and a b u v :: ereal |
837 fixes f :: "real \<Rightarrow> 'a::euclidean_space" and a b u v :: ereal |
838 assumes "a < b" |
838 assumes "a < b" |
839 and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x" |
839 and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x" |
840 and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)" |
840 and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)" |
841 and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x" |
841 and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x" |
843 and A: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)" |
843 and A: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)" |
844 and B: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)" |
844 and B: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)" |
845 and integrable: "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))" |
845 and integrable: "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))" |
846 and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)" |
846 and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)" |
847 shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))" |
847 shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))" |
848 proof%unimportant - |
848 proof - |
849 obtain u l where approx [simp]: |
849 obtain u l where approx [simp]: |
850 "einterval a b = (\<Union>i. {l i .. u i})" |
850 "einterval a b = (\<Union>i. {l i .. u i})" |
851 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
851 "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
852 "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
852 "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
853 by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>]) |
853 by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>]) |
930 |
930 |
931 (* TODO: the last two proofs are only slightly different. Factor out common part? |
931 (* TODO: the last two proofs are only slightly different. Factor out common part? |
932 An alternative: make the second one the main one, and then have another lemma |
932 An alternative: make the second one the main one, and then have another lemma |
933 that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *) |
933 that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *) |
934 |
934 |
935 lemma%important interval_integral_substitution_nonneg: |
935 theorem interval_integral_substitution_nonneg: |
936 fixes f g g':: "real \<Rightarrow> real" and a b u v :: ereal |
936 fixes f g g':: "real \<Rightarrow> real" and a b u v :: ereal |
937 assumes "a < b" |
937 assumes "a < b" |
938 and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x" |
938 and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x" |
939 and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)" |
939 and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)" |
940 and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x" |
940 and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x" |
944 and B: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)" |
944 and B: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)" |
945 and integrable_fg: "set_integrable lborel (einterval a b) (\<lambda>x. f (g x) * g' x)" |
945 and integrable_fg: "set_integrable lborel (einterval a b) (\<lambda>x. f (g x) * g' x)" |
946 shows |
946 shows |
947 "set_integrable lborel (einterval A B) f" |
947 "set_integrable lborel (einterval A B) f" |
948 "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))" |
948 "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))" |
949 proof%unimportant - |
949 proof - |
950 from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this |
950 from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this |
951 note less_imp_le [simp] |
951 note less_imp_le [simp] |
952 have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x" |
952 have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x" |
953 by (rule order_less_le_trans, rule approx, force) |
953 by (rule order_less_le_trans, rule approx, force) |
954 have lessb[simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b" |
954 have lessb[simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b" |
1077 ("(4CLBINT _=_.._. _)" [0,60,60,61] 60) |
1077 ("(4CLBINT _=_.._. _)" [0,60,60,61] 60) |
1078 |
1078 |
1079 translations |
1079 translations |
1080 "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)" |
1080 "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)" |
1081 |
1081 |
1082 lemma%important interval_integral_norm: |
1082 proposition interval_integral_norm: |
1083 fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" |
1083 fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" |
1084 shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow> |
1084 shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow> |
1085 norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)" |
1085 norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)" |
1086 using%unimportant integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"] |
1086 using%unimportant integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"] |
1087 by%unimportant (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def) |
1087 by%unimportant (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def) |
1088 |
1088 |
1089 lemma%important interval_integral_norm2: |
1089 proposition interval_integral_norm2: |
1090 "interval_lebesgue_integrable lborel a b f \<Longrightarrow> |
1090 "interval_lebesgue_integrable lborel a b f \<Longrightarrow> |
1091 norm (LBINT t=a..b. f t) \<le> \<bar>LBINT t=a..b. norm (f t)\<bar>" |
1091 norm (LBINT t=a..b. f t) \<le> \<bar>LBINT t=a..b. norm (f t)\<bar>" |
1092 proof%unimportant (induct a b rule: linorder_wlog) |
1092 proof (induct a b rule: linorder_wlog) |
1093 case (sym a b) then show ?case |
1093 case (sym a b) then show ?case |
1094 by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b]) |
1094 by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b]) |
1095 next |
1095 next |
1096 case (le a b) |
1096 case (le a b) |
1097 then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)" |
1097 then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)" |