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