author | wenzelm |
Thu, 25 Jul 2024 10:30:22 +0200 | |
changeset 80616 | 94703573e0af |
parent 79599 | 2c18ac57e92e |
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 |
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
|
12 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
13 |
lemma einterval_eq[simp]: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
14 |
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
|
15 |
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
|
16 |
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
|
17 |
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
|
18 |
by (auto simp: einterval_def) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
19 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
20 |
lemma einterval_same: "einterval a a = {}" |
68096 | 21 |
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
|
22 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
23 |
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
|
24 |
by (simp add: einterval_def) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
25 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
26 |
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
|
27 |
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
|
28 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
29 |
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
|
30 |
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
|
31 |
(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
|
32 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
33 |
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
|
34 |
unfolding einterval_def by measurable |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
35 |
|
69683 | 36 |
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
|
37 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
38 |
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
|
39 |
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
|
40 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
41 |
lemma ereal_incseq_approx: |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
42 |
fixes a b :: ereal |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
43 |
assumes "a < b" |
68095
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68046
diff
changeset
|
44 |
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
|
45 |
proof (cases b) |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
46 |
case PInf |
61808 | 47 |
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
|
48 |
by (cases a) auto |
61969 | 49 |
moreover have "(\<lambda>x. ereal (real (Suc x))) \<longlonglongrightarrow> \<infinity>" |
71827 | 50 |
by (simp add: Lim_PInfty filterlim_sequentially_Suc) (metis le_SucI of_nat_Suc of_nat_mono order_trans real_arch_simple) |
61969 | 51 |
moreover have "\<And>r. (\<lambda>x. ereal (r + real (Suc x))) \<longlonglongrightarrow> \<infinity>" |
71827 | 52 |
by (simp add: filterlim_sequentially_Suc 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
|
53 |
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
|
54 |
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
|
55 |
(auto simp: incseq_def PInf) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
56 |
next |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
57 |
case (real b') |
63040 | 58 |
define d where "d = b' - (if a = -\<infinity> then b' - 1 else real_of_ereal a)" |
61808 | 59 |
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
|
60 |
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
|
61 |
moreover |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
62 |
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
|
63 |
by (intro mult_strict_left_mono) auto |
61808 | 64 |
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
|
65 |
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
|
66 |
moreover |
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68046
diff
changeset
|
67 |
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
|
68 |
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
|
69 |
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
|
70 |
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
|
71 |
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
|
72 |
ultimately show thesis |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
73 |
by (intro that[of "\<lambda>i. b' - d / Suc (Suc i)"]) |
68096 | 74 |
(auto simp: real incseq_def intro!: divide_left_mono) |
74362 | 75 |
qed (use \<open>a < b\<close> in auto) |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
76 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
77 |
lemma ereal_decseq_approx: |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
78 |
fixes a b :: ereal |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
79 |
assumes "a < b" |
63329 | 80 |
obtains X :: "nat \<Rightarrow> real" where |
61969 | 81 |
"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
|
82 |
proof - |
61808 | 83 |
have "-b < -a" using \<open>a < b\<close> by simp |
74362 | 84 |
from ereal_incseq_approx[OF this] obtain X where |
85 |
"incseq X" |
|
86 |
"\<And>i. - b < ereal (X i)" |
|
87 |
"\<And>i. ereal (X i) < - a" |
|
88 |
"(\<lambda>x. ereal (X x)) \<longlonglongrightarrow> - a" |
|
89 |
by auto |
|
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
90 |
then show thesis |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
91 |
apply (intro that[of "\<lambda>i. - X i"]) |
68403 | 92 |
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
|
93 |
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
|
94 |
done |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
95 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
96 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
97 |
proposition einterval_Icc_approximation: |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
98 |
fixes a b :: ereal |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
99 |
assumes "a < b" |
63329 | 100 |
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
|
101 |
"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
|
102 |
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
61969 | 103 |
"l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
104 |
proof - |
61808 | 105 |
from dense[OF \<open>a < b\<close>] obtain c where "a < c" "c < b" by safe |
74362 | 106 |
from ereal_incseq_approx[OF \<open>c < b\<close>] obtain u where u: |
107 |
"incseq u" |
|
108 |
"\<And>i. c < ereal (u i)" |
|
109 |
"\<And>i. ereal (u i) < b" |
|
110 |
"(\<lambda>x. ereal (u x)) \<longlonglongrightarrow> b" |
|
111 |
by auto |
|
112 |
from ereal_decseq_approx[OF \<open>a < c\<close>] obtain l where l: |
|
113 |
"decseq l" |
|
114 |
"\<And>i. a < ereal (l i)" |
|
115 |
"\<And>i. ereal (l i) < c" |
|
116 |
"(\<lambda>x. ereal (l x)) \<longlonglongrightarrow> a" |
|
117 |
by auto |
|
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
118 |
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
|
119 |
proof (auto simp: einterval_iff) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
120 |
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
|
121 |
have "eventually (\<lambda>i. ereal (l i) < ereal x) sequentially" |
61808 | 122 |
using l(4) \<open>a < ereal x\<close> by (rule order_tendstoD) |
63329 | 123 |
moreover |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
124 |
have "eventually (\<lambda>i. ereal x < ereal (u i)) sequentially" |
61808 | 125 |
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
|
126 |
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
|
127 |
by eventually_elim auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
128 |
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
|
129 |
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
|
130 |
next |
63329 | 131 |
fix x i assume "l i \<le> x" "x \<le> u i" |
61808 | 132 |
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
|
133 |
show "a < ereal x" "ereal x < b" |
68403 | 134 |
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
|
135 |
qed |
78480 | 136 |
moreover { fix i from less_trans[OF \<open>l i < c\<close> \<open>c < u i\<close>] have "l i < u i" by simp } |
137 |
ultimately show thesis |
|
138 |
by (simp add: l that u) |
|
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
139 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
140 |
|
63329 | 141 |
(* 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
|
142 |
they are real. *) |
70136 | 143 |
definition\<^marker>\<open>tag important\<close> 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
|
144 |
"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
|
145 |
(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
|
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_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
|
149 |
("(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
|
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 |
"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
|
153 |
|
70136 | 154 |
definition\<^marker>\<open>tag important\<close> 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
|
155 |
"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
|
156 |
(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
|
157 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
158 |
syntax |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
159 |
"_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
|
160 |
("(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
|
161 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
162 |
translations |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
163 |
"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
|
164 |
|
69683 | 165 |
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
|
166 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
167 |
lemma interval_lebesgue_integral_cong: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
168 |
"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
|
169 |
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
|
170 |
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
|
171 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
172 |
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
|
173 |
"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
|
174 |
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
|
175 |
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
|
176 |
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
|
177 |
|
62083 | 178 |
lemma interval_integrable_mirror: |
179 |
shows "interval_lebesgue_integrable lborel a b (\<lambda>x. f (-x)) \<longleftrightarrow> |
|
180 |
interval_lebesgue_integrable lborel (-b) (-a) f" |
|
181 |
proof - |
|
182 |
have *: "indicator (einterval a b) (- x) = (indicator (einterval (-b) (-a)) x :: real)" |
|
183 |
for a b :: ereal and x :: real |
|
184 |
by (cases a b rule: ereal2_cases) (auto simp: einterval_def split: split_indicator) |
|
185 |
show ?thesis |
|
186 |
unfolding interval_lebesgue_integrable_def |
|
187 |
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
|
188 |
by (simp add: * set_integrable_def) |
62083 | 189 |
qed |
190 |
||
63329 | 191 |
lemma interval_lebesgue_integral_add [intro, simp]: |
192 |
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
|
193 |
assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g" |
78480 | 194 |
shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)" |
195 |
and "interval_lebesgue_integral M a b (\<lambda>x. f x + g x) = |
|
196 |
interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g" |
|
68096 | 197 |
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
|
198 |
field_simps) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
199 |
|
63329 | 200 |
lemma interval_lebesgue_integral_diff [intro, simp]: |
201 |
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
|
202 |
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
|
203 |
"interval_lebesgue_integrable M a b g" |
63329 | 204 |
shows "interval_lebesgue_integrable M a b (\<lambda>x. f x - g x)" and |
205 |
"interval_lebesgue_integral M a b (\<lambda>x. f x - g x) = |
|
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
206 |
interval_lebesgue_integral M a b f - interval_lebesgue_integral M a b g" |
68096 | 207 |
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
|
208 |
field_simps) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
209 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
210 |
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
|
211 |
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
|
212 |
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
|
213 |
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
|
214 |
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
|
215 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
216 |
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
|
217 |
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
|
218 |
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
|
219 |
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
|
220 |
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
|
221 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
222 |
lemma interval_lebesgue_integrable_divide [intro, simp]: |
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59587
diff
changeset
|
223 |
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
|
224 |
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
|
225 |
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
|
226 |
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
|
227 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
228 |
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
|
229 |
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
|
230 |
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
|
231 |
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
|
232 |
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
|
233 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
234 |
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
|
235 |
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
|
236 |
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
|
237 |
interval_lebesgue_integral M a b f * c" |
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
238 |
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
|
239 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
240 |
lemma interval_lebesgue_integral_divide [simp]: |
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59587
diff
changeset
|
241 |
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
|
242 |
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
|
243 |
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
|
244 |
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
|
245 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
246 |
lemma interval_lebesgue_integral_uminus: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
247 |
"interval_lebesgue_integral M a b (\<lambda>x. - f x) = - interval_lebesgue_integral M a b f" |
68096 | 248 |
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
|
249 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
250 |
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
|
251 |
"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
|
252 |
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
|
253 |
unfolding interval_lebesgue_integral_def |
68096 | 254 |
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
|
255 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
256 |
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
|
257 |
fixes a b f |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
258 |
assumes "a \<le> b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
259 |
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
|
260 |
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
|
261 |
|
63329 | 262 |
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
|
263 |
fixes a b f |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
264 |
assumes "a > b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
265 |
shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)" |
68096 | 266 |
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
|
267 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
268 |
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
|
269 |
fixes a b f |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
270 |
assumes "a > b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
271 |
shows "interval_lebesgue_integral M a b f = - interval_lebesgue_integral M b a f" |
68096 | 272 |
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
|
273 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
274 |
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
|
275 |
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
|
276 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
277 |
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
|
278 |
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
|
279 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
280 |
lemma interval_integrable_endpoints_reverse: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
281 |
"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
|
282 |
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
|
283 |
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
|
284 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
285 |
lemma interval_integral_reflect: |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
286 |
"(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
|
287 |
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
|
288 |
case (sym a b) then show ?case |
68096 | 289 |
by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse |
62390 | 290 |
split: if_split_asm) |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
291 |
next |
67974
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
292 |
case (le a b) |
79599
2c18ac57e92e
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
paulson <lp15@cam.ac.uk>
parents:
78480
diff
changeset
|
293 |
have "(LBINT x:{x. - x \<in> einterval a b}. f (- x)) = (LBINT x:einterval (- b) (- a). f (- x))" |
78480 | 294 |
unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def einterval_def |
295 |
by (metis (lifting) ereal_less_uminus_reorder ereal_uminus_less_reorder indicator_simps mem_Collect_eq uminus_ereal.simps(1)) |
|
67974
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
296 |
then show ?case |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
297 |
unfolding interval_lebesgue_integral_def |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
298 |
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
|
299 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
300 |
|
61897
bc0fc5499085
Bochner integral: prove dominated convergence at_top
hoelzl
parents:
61882
diff
changeset
|
301 |
lemma interval_lebesgue_integral_0_infty: |
bc0fc5499085
Bochner integral: prove dominated convergence at_top
hoelzl
parents:
61882
diff
changeset
|
302 |
"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
|
303 |
"interval_lebesgue_integral M 0 \<infinity> f = (LINT x:{0<..}|M. f x)" |
63329 | 304 |
unfolding zero_ereal_def |
61897
bc0fc5499085
Bochner integral: prove dominated convergence at_top
hoelzl
parents:
61882
diff
changeset
|
305 |
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
|
306 |
|
bc0fc5499085
Bochner integral: prove dominated convergence at_top
hoelzl
parents:
61882
diff
changeset
|
307 |
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
|
308 |
unfolding interval_lebesgue_integral_def by auto |
bc0fc5499085
Bochner integral: prove dominated convergence at_top
hoelzl
parents:
61882
diff
changeset
|
309 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
310 |
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
|
311 |
(set_integrable M {a<..} f)" |
70136 | 312 |
unfolding interval_lebesgue_integrable_def by auto |
61897
bc0fc5499085
Bochner integral: prove dominated convergence at_top
hoelzl
parents:
61882
diff
changeset
|
313 |
|
69683 | 314 |
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
|
315 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
316 |
lemma interval_integral_zero [simp]: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
317 |
fixes a b :: ereal |
79599
2c18ac57e92e
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
paulson <lp15@cam.ac.uk>
parents:
78480
diff
changeset
|
318 |
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
|
319 |
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
|
320 |
by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
321 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
322 |
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
|
323 |
fixes a b c :: real |
79599
2c18ac57e92e
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
paulson <lp15@cam.ac.uk>
parents:
78480
diff
changeset
|
324 |
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
|
325 |
unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq |
68096 | 326 |
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
|
327 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
328 |
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
|
329 |
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
|
330 |
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
|
331 |
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
|
332 |
using assms |
78480 | 333 |
by (auto simp: interval_lebesgue_integral_def max_def min_def intro!: set_lebesgue_integral_cong_AE) |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
334 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
335 |
lemma interval_integral_cong: |
63329 | 336 |
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
|
337 |
shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g" |
78480 | 338 |
using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_cong) |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
339 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
340 |
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
|
341 |
"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
|
342 |
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
|
343 |
interval_lebesgue_integrable lborel a b f = interval_lebesgue_integrable lborel a b g" |
68096 | 344 |
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
|
345 |
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
|
346 |
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
|
347 |
done |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
348 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
349 |
lemma interval_integrable_abs_iff: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
350 |
fixes f :: "real \<Rightarrow> real" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
351 |
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
|
352 |
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
|
353 |
unfolding interval_lebesgue_integrable_def |
78480 | 354 |
by (simp add: set_integrable_abs_iff') |
59092
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_integral_Icc: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
357 |
fixes a b :: real |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
358 |
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
|
359 |
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
|
360 |
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
|
361 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
362 |
lemma interval_integral_Icc': |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
363 |
"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
|
364 |
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
|
365 |
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
|
366 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
367 |
lemma interval_integral_Ioc: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
368 |
"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
|
369 |
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
|
370 |
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
|
371 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
372 |
(* 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
|
373 |
lemma interval_integral_Ioc': |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
374 |
"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
|
375 |
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
|
376 |
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
|
377 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
378 |
lemma interval_integral_Ico: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
379 |
"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
|
380 |
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
|
381 |
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
|
382 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
383 |
lemma interval_integral_Ioi: |
61882 | 384 |
"\<bar>a\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..\<infinity>. f x) = (LBINT x : {real_of_ereal a <..}. f x)" |
68096 | 385 |
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
|
386 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
387 |
lemma interval_integral_Ioo: |
61882 | 388 |
"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 | 389 |
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
|
390 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
391 |
lemma interval_integral_discrete_difference: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
392 |
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
|
393 |
assumes "countable X" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
394 |
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
|
395 |
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
|
396 |
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
|
397 |
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
|
398 |
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
|
399 |
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
|
400 |
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
|
401 |
done |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
402 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
403 |
lemma interval_integral_sum: |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
404 |
fixes a b c :: ereal |
63329 | 405 |
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
|
406 |
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
|
407 |
proof - |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
408 |
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
|
409 |
{ 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
|
410 |
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
|
411 |
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
|
412 |
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
|
413 |
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
|
414 |
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
|
415 |
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
|
416 |
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
|
417 |
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
|
418 |
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
|
419 |
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
|
420 |
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
|
421 |
unfolding set_borel_measurable_def |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
422 |
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
|
423 |
qed |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
424 |
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
|
425 |
using ord |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
426 |
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
|
427 |
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
|
428 |
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
|
429 |
} note 1 = this |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
430 |
{ 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
|
431 |
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
|
432 |
by (metis add.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
433 |
} note 2 = this |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
434 |
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
|
435 |
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
|
436 |
show ?thesis |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
437 |
using integrable |
73526
a3cc9fa1295d
new automatic order prover: stateless, complete, verified
nipkow
parents:
71827
diff
changeset
|
438 |
apply (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases]) |
a3cc9fa1295d
new automatic order prover: stateless, complete, verified
nipkow
parents:
71827
diff
changeset
|
439 |
apply simp_all (* remove some looping cases *) |
a3cc9fa1295d
new automatic order prover: stateless, complete, verified
nipkow
parents:
71827
diff
changeset
|
440 |
by (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3) |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
441 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
442 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
443 |
lemma interval_integrable_isCont: |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
444 |
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
|
445 |
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
|
446 |
interval_lebesgue_integrable lborel a b f" |
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
447 |
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
|
448 |
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
|
449 |
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
|
450 |
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
|
451 |
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
|
452 |
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
|
453 |
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
|
454 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
455 |
lemma interval_integrable_continuous_on: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
456 |
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
|
457 |
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
|
458 |
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
|
459 |
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
|
460 |
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
|
461 |
|
63329 | 462 |
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
|
463 |
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
|
464 |
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
|
465 |
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
|
466 |
|
63329 | 467 |
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
|
468 |
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
|
469 |
shows "a \<le> b \<Longrightarrow> set_integrable lborel (einterval a b) f \<Longrightarrow> LBINT x=a..b. f x = integral (einterval a b) f" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
470 |
by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral) |
63329 | 471 |
|
67974
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
472 |
|
69683 | 473 |
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
|
474 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
475 |
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
|
476 |
fixes a b :: ereal |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
477 |
assumes "a < b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
478 |
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
|
479 |
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
|
480 |
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
61969 | 481 |
"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
|
482 |
fixes f :: "real \<Rightarrow> real" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
483 |
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
|
484 |
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
|
485 |
assumes f_measurable: "set_borel_measurable lborel (einterval a b) f" |
61969 | 486 |
assumes lbint_lim: "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> C" |
63329 | 487 |
shows |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
488 |
"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
|
489 |
"(LBINT x=a..b. f x) = C" |
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
490 |
proof - |
67974
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
491 |
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
|
492 |
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
|
493 |
proof - |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
494 |
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
|
495 |
by eventually_elim |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
496 |
(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
|
497 |
then show ?thesis |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
498 |
apply eventually_elim |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
499 |
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
|
500 |
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
|
501 |
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
|
502 |
done |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
503 |
qed |
61969 | 504 |
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
|
505 |
proof - |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
506 |
{ 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
|
507 |
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
|
508 |
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
|
509 |
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
|
510 |
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
|
511 |
done |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
512 |
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
|
513 |
by eventually_elim auto } |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
514 |
then show ?thesis |
70365
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70136
diff
changeset
|
515 |
unfolding approx(1) by (auto intro!: AE_I2 tendsto_eventually split: split_indicator) |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
516 |
qed |
61969 | 517 |
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
|
518 |
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
|
519 |
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
|
520 |
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
|
521 |
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
|
522 |
using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def less_imp_le) |
68096 | 523 |
also have "\<dots> = C" |
67974
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
524 |
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
|
525 |
finally show "(LBINT x=a..b. f x) = C" . |
63329 | 526 |
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
|
527 |
unfolding set_integrable_def |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
528 |
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
|
529 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
530 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
531 |
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
|
532 |
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
|
533 |
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
|
534 |
assumes "a < b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
535 |
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
|
536 |
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b" |
61969 | 537 |
"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
|
538 |
assumes f_integrable: "set_integrable lborel (einterval a b) f" |
61969 | 539 |
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
|
540 |
proof - |
61969 | 541 |
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
|
542 |
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
|
543 |
proof (rule integral_dominated_convergence) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
544 |
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
|
545 |
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
|
546 |
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
|
547 |
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
|
548 |
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
|
549 |
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
|
550 |
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
|
551 |
by (intro AE_I2) (auto simp: approx split: split_indicator) |
61969 | 552 |
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" |
70365
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70136
diff
changeset
|
553 |
proof (intro AE_I2 tendsto_intros tendsto_eventually) |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
554 |
fix x |
63329 | 555 |
{ fix i assume "l i \<le> x" "x \<le> u i" |
61808 | 556 |
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
|
557 |
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
|
558 |
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
|
559 |
then show "eventually (\<lambda>xa. indicator {l xa..u xa} x = (indicator (einterval a b) x::real)) sequentially" |
61969 | 560 |
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
|
561 |
by (auto split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
562 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
563 |
qed |
61808 | 564 |
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
|
565 |
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
|
566 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
567 |
|
69683 | 568 |
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
|
569 |
|
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
570 |
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
|
571 |
arbitrary intervals.\<close> |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
572 |
|
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
573 |
(* |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
574 |
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
|
575 |
*) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
576 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
577 |
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
|
578 |
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
|
579 |
assumes f: "continuous_on {min a b..max a b} f" |
63329 | 580 |
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 |
581 |
{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
|
582 |
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
|
583 |
proof (cases "a \<le> b") |
67974
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
584 |
case True |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
585 |
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
|
586 |
by (simp add: True interval_integral_Icc set_lebesgue_integral_def) |
68096 | 587 |
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
|
588 |
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
|
589 |
show "continuous_on {a..b} f" |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
590 |
using True f by linarith |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
591 |
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
|
592 |
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
|
593 |
qed |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
594 |
finally show ?thesis . |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
595 |
next |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
596 |
case False |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
597 |
then have "b \<le> a" |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
598 |
by simp |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
599 |
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
|
600 |
by (simp add: \<open>b \<le> a\<close> interval_integral_Icc set_lebesgue_integral_def) |
68096 | 601 |
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
|
602 |
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
|
603 |
show "continuous_on {b..a} f" |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
604 |
using False f by linarith |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
605 |
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
|
606 |
\<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
|
607 |
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
|
608 |
qed auto |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
609 |
finally show ?thesis |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
610 |
by (metis interval_integral_endpoints_reverse) |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
611 |
qed |
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
612 |
|
3f352a91b45a
replacement of set integral abbreviations by actual definitions!
paulson <lp15@cam.ac.uk>
parents:
66164
diff
changeset
|
613 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
614 |
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
|
615 |
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
|
616 |
assumes "a < b" |
63329 | 617 |
assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x" |
618 |
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
|
619 |
assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x" |
61973 | 620 |
assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)" |
621 |
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
|
622 |
shows |
63329 | 623 |
"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
|
624 |
"(LBINT x=a..b. f x) = B - A" |
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
625 |
proof - |
68095
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68046
diff
changeset
|
626 |
obtain u l where approx: |
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68046
diff
changeset
|
627 |
"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
|
628 |
"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
|
629 |
"l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68046
diff
changeset
|
630 |
by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>]) |
78480 | 631 |
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
|
632 |
by (rule order_less_le_trans, rule approx, force) |
78480 | 633 |
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
|
634 |
by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) |
78480 | 635 |
have cf: "\<And>i. continuous_on {min (l i) (u i)..max (l i) (u i)} f" |
636 |
using approx f by (intro continuous_at_imp_continuous_on strip) auto |
|
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
637 |
have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)" |
78480 | 638 |
apply (intro interval_integral_FTC_finite cf DERIV_subset [OF F]) |
639 |
by (smt (verit) F aless approx(4) has_real_derivative_iff_has_vector_derivative has_vector_derivative_at_within lessb) |
|
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
640 |
have 1: "\<And>i. set_integrable lborel {l i..u i} f" |
78480 | 641 |
by (meson aless lessb assms(3) atLeastAtMost_iff borel_integrable_atLeastAtMost' 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
|
642 |
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
|
643 |
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
|
644 |
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
|
645 |
simp: continuous_on_eq_continuous_at einterval_iff f) |
78480 | 646 |
have "(\<lambda>x. F (l x)) \<longlonglongrightarrow> A" |
647 |
using A approx unfolding tendsto_at_iff_sequentially comp_def |
|
648 |
by (force elim!: allE[of _ "\<lambda>i. ereal (l i)"]) |
|
649 |
moreover have "(\<lambda>x. F (u x)) \<longlonglongrightarrow> B" |
|
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
650 |
using B approx unfolding tendsto_at_iff_sequentially comp_def |
78480 | 651 |
by (force elim!: allE[of _ "\<lambda>i. ereal (u i)"]) |
652 |
ultimately have 3: "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A" |
|
653 |
by (simp add: FTCi tendsto_diff) |
|
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
654 |
show "(LBINT x=a..b. f x) = B - A" |
61808 | 655 |
by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3]) |
63329 | 656 |
show "set_integrable lborel (einterval a b) f" |
61808 | 657 |
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
|
658 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
659 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
660 |
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
|
661 |
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
|
662 |
assumes "a < b" |
63329 | 663 |
assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)" |
664 |
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
|
665 |
assumes f_integrable: "set_integrable lborel (einterval a b) f" |
61973 | 666 |
assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)" |
667 |
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
|
668 |
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
|
669 |
proof - |
68095
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68046
diff
changeset
|
670 |
obtain u l where approx: |
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68046
diff
changeset
|
671 |
"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
|
672 |
"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
|
673 |
"l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" |
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68046
diff
changeset
|
674 |
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
|
675 |
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
|
676 |
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
|
677 |
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
|
678 |
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
|
679 |
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
|
680 |
using assms approx |
68096 | 681 |
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
|
682 |
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
|
683 |
intro: has_vector_derivative_at_within) |
61969 | 684 |
have "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A" |
68096 | 685 |
unfolding FTCi |
686 |
proof (intro tendsto_intros) |
|
687 |
show "(\<lambda>x. F (l x)) \<longlonglongrightarrow> A" |
|
688 |
using A approx unfolding tendsto_at_iff_sequentially comp_def |
|
689 |
by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto) |
|
690 |
show "(\<lambda>x. F (u x)) \<longlonglongrightarrow> B" |
|
691 |
using B approx unfolding tendsto_at_iff_sequentially comp_def |
|
692 |
by (elim allE[of _ "\<lambda>i. ereal (u i)"], auto) |
|
693 |
qed |
|
61969 | 694 |
moreover have "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)" |
61808 | 695 |
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
|
696 |
ultimately show ?thesis |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
697 |
by (elim LIMSEQ_unique) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
698 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
699 |
|
63329 | 700 |
(* |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
701 |
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
|
702 |
einterval. |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
703 |
*) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
704 |
|
69681
689997a8a582
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
immler
parents:
69680
diff
changeset
|
705 |
theorem interval_integral_FTC2: |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
706 |
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
|
707 |
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
|
708 |
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
|
709 |
fixes x :: real |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
710 |
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
|
711 |
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
|
712 |
proof - |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
713 |
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
|
714 |
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
|
715 |
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
|
716 |
have "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})" |
68096 | 717 |
using \<open>a \<le> x\<close> \<open>x \<le> b\<close> |
718 |
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
|
719 |
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
|
720 |
by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
721 |
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
|
722 |
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
|
723 |
(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
|
724 |
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
|
725 |
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
|
726 |
then show ?thesis |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
727 |
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
|
728 |
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
|
729 |
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
|
730 |
using assms |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
731 |
apply (intro interval_integral_sum) |
68096 | 732 |
apply (auto simp: interval_lebesgue_integrable_def simp del: real_scaleR_def) |