author | hoelzl |
Tue, 27 Jan 2015 16:12:40 +0100 | |
changeset 59452 | 2538b2c51769 |
parent 59092 | d469103c0737 |
child 61609 | 77b453bd616f |
permissions | -rw-r--r-- |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
1 |
(* Title: HOL/Probability/Lebesgue_Integral_Substitution.thy |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
2 |
Author: Manuel Eberl |
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 |
Provides lemmas for integration by substitution for the basic integral types. |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
5 |
Note that the substitution function must have a nonnegative derivative. |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
6 |
This could probably be weakened somehow. |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
7 |
*) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
8 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
9 |
section {* Integration by Substition *} |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
10 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
11 |
theory Lebesgue_Integral_Substitution |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
12 |
imports Interval_Integral |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
13 |
begin |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
14 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
15 |
lemma measurable_sets_borel: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
16 |
"\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
17 |
by (drule (1) measurable_sets) simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
18 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
19 |
lemma closure_Iii: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
20 |
assumes "a < b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
21 |
shows "closure {a<..<b::real} = {a..b}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
22 |
proof- |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
23 |
have "{a<..<b} = ball ((a+b)/2) ((b-a)/2)" by (auto simp: dist_real_def field_simps not_less) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
24 |
also from assms have "closure ... = cball ((a+b)/2) ((b-a)/2)" by (intro closure_ball) simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
25 |
also have "... = {a..b}" by (auto simp: dist_real_def field_simps not_less) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
26 |
finally show ?thesis . |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
27 |
qed |
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 continuous_ge_on_Iii: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
30 |
assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
31 |
shows "g (x::real) \<ge> (a::real)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
32 |
proof- |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
33 |
from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_Iii[symmetric]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
34 |
also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
35 |
hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
36 |
also from assms(1) have "closed (g -` {a..} \<inter> {c..d})" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
37 |
by (auto simp: continuous_on_closed_vimage) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
38 |
hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
39 |
finally show ?thesis using `x \<in> {c..d}` by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
40 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
41 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
42 |
lemma interior_real_semiline': |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
43 |
fixes a :: real |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
44 |
shows "interior {..a} = {..<a}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
45 |
proof - |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
46 |
{ |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
47 |
fix y |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
48 |
assume "a > y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
49 |
then have "y \<in> interior {..a}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
50 |
apply (simp add: mem_interior) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
51 |
apply (rule_tac x="(a-y)" in exI) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
52 |
apply (auto simp add: dist_norm) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
53 |
done |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
54 |
} |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
55 |
moreover |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
56 |
{ |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
57 |
fix y |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
58 |
assume "y \<in> interior {..a}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
59 |
then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
60 |
using mem_interior_cball[of y "{..a}"] by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
61 |
moreover from e have "y + e \<in> cball y e" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
62 |
by (auto simp add: cball_def dist_norm) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
63 |
ultimately have "a \<ge> y + e" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
64 |
then have "a > y" using e by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
65 |
} |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
66 |
ultimately show ?thesis by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
67 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
68 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
69 |
lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
70 |
proof- |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
71 |
have "{a..b} = {a..} \<inter> {..b}" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
72 |
also have "interior ... = {a<..} \<inter> {..<b}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
73 |
by (simp add: interior_real_semiline interior_real_semiline') |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
74 |
also have "... = {a<..<b}" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
75 |
finally show ?thesis . |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
76 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
77 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
78 |
lemma nn_integral_indicator_singleton[simp]: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
79 |
assumes [measurable]: "{y} \<in> sets M" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
80 |
shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = max 0 (f y) * emeasure M {y}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
81 |
proof- |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
82 |
have "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = (\<integral>\<^sup>+x. max 0 (f y) * indicator {y} x \<partial>M)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
83 |
by (subst nn_integral_max_0[symmetric]) (auto intro!: nn_integral_cong split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
84 |
then show ?thesis |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
85 |
by (simp add: nn_integral_cmult) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
86 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
87 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
88 |
lemma nn_integral_set_ereal: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
89 |
"(\<integral>\<^sup>+x. ereal (f x) * indicator A x \<partial>M) = (\<integral>\<^sup>+x. ereal (f x * indicator A x) \<partial>M)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
90 |
by (rule nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
91 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
92 |
lemma nn_integral_indicator_singleton'[simp]: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
93 |
assumes [measurable]: "{y} \<in> sets M" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
94 |
shows "(\<integral>\<^sup>+x. ereal (f x * indicator {y} x) \<partial>M) = max 0 (f y) * emeasure M {y}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
95 |
by (subst nn_integral_set_ereal[symmetric]) simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
96 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
97 |
lemma set_borel_measurable_sets: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
98 |
fixes f :: "_ \<Rightarrow> _::real_normed_vector" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
99 |
assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
100 |
shows "f -` B \<inter> X \<in> sets M" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
101 |
proof - |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
102 |
have "f \<in> borel_measurable (restrict_space M X)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
103 |
using assms by (subst borel_measurable_restrict_space_iff) auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
104 |
then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
105 |
by (rule measurable_sets) fact |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
106 |
with `X \<in> sets M` show ?thesis |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
107 |
by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
108 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
109 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
110 |
lemma borel_set_induct[consumes 1, case_names empty interval compl union]: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
111 |
assumes "A \<in> sets borel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
112 |
assumes empty: "P {}" and int: "\<And>a b. a \<le> b \<Longrightarrow> P {a..b}" and compl: "\<And>A. A \<in> sets borel \<Longrightarrow> P A \<Longrightarrow> P (-A)" and |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
113 |
un: "\<And>f. disjoint_family f \<Longrightarrow> (\<And>i. f i \<in> sets borel) \<Longrightarrow> (\<And>i. P (f i)) \<Longrightarrow> P (\<Union>i::nat. f i)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
114 |
shows "P (A::real set)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
115 |
proof- |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
116 |
let ?G = "range (\<lambda>(a,b). {a..b::real})" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
117 |
have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> sigma_sets UNIV ?G" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
118 |
using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
119 |
thus ?thesis |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
120 |
proof (induction rule: sigma_sets_induct_disjoint) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
121 |
case (union f) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
122 |
from union.hyps(2) have "\<And>i. f i \<in> sets borel" by (auto simp: borel_eq_atLeastAtMost) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
123 |
with union show ?case by (auto intro: un) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
124 |
next |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
125 |
case (basic A) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
126 |
then obtain a b where "A = {a .. b}" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
127 |
then show ?case |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
128 |
by (cases "a \<le> b") (auto intro: int empty) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
129 |
qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
130 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
131 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
132 |
definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
133 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
134 |
lemma mono_onI: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
135 |
"(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on f A" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
136 |
unfolding mono_on_def by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
137 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
138 |
lemma mono_onD: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
139 |
"\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
140 |
unfolding mono_on_def by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
141 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
142 |
lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
143 |
unfolding mono_def mono_on_def by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
144 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
145 |
lemma mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
146 |
unfolding mono_on_def by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
147 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
148 |
definition "strict_mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
149 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
150 |
lemma strict_mono_onI: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
151 |
"(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on f A" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
152 |
unfolding strict_mono_on_def by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
153 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
154 |
lemma strict_mono_onD: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
155 |
"\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
156 |
unfolding strict_mono_on_def by simp |
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 |
lemma mono_on_greaterD: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
159 |
assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
160 |
shows "x > y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
161 |
proof (rule ccontr) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
162 |
assume "\<not>x > y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
163 |
hence "x \<le> y" by (simp add: not_less) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
164 |
from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
165 |
with assms(4) show False by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
166 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
167 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
168 |
lemma strict_mono_inv: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
169 |
fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
170 |
assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
171 |
shows "strict_mono g" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
172 |
proof |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
173 |
fix x y :: 'b assume "x < y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
174 |
from `surj f` obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
175 |
with `x < y` and `strict_mono f` have "x' < y'" by (simp add: strict_mono_less) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
176 |
with inv show "g x < g y" by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
177 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
178 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
179 |
lemma strict_mono_on_imp_inj_on: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
180 |
assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
181 |
shows "inj_on f A" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
182 |
proof (rule inj_onI) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
183 |
fix x y assume "x \<in> A" "y \<in> A" "f x = f y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
184 |
thus "x = y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
185 |
by (cases x y rule: linorder_cases) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
186 |
(auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
187 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
188 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
189 |
lemma strict_mono_on_leD: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
190 |
assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
191 |
shows "f x \<le> f y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
192 |
proof (insert le_less_linear[of y x], elim disjE) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
193 |
assume "x < y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
194 |
with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
195 |
thus ?thesis by (rule less_imp_le) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
196 |
qed (insert assms, simp) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
197 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
198 |
lemma strict_mono_on_eqD: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
199 |
fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
200 |
assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
201 |
shows "y = x" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
202 |
using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
203 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
204 |
lemma mono_on_imp_deriv_nonneg: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
205 |
assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
206 |
assumes "x \<in> interior A" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
207 |
shows "D \<ge> 0" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
208 |
proof (rule tendsto_le_const) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
209 |
let ?A' = "(\<lambda>y. y - x) ` interior A" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
210 |
from deriv show "((\<lambda>h. (f (x + h) - f x) / h) ---> D) (at 0)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
211 |
by (simp add: field_has_derivative_at has_field_derivative_def) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
212 |
from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
213 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
214 |
show "eventually (\<lambda>h. (f (x + h) - f x) / h \<ge> 0) (at 0)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
215 |
proof (subst eventually_at_topological, intro exI conjI ballI impI) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
216 |
have "open (interior A)" by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
217 |
hence "open (op + (-x) ` interior A)" by (rule open_translation) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
218 |
also have "(op + (-x) ` interior A) = ?A'" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
219 |
finally show "open ?A'" . |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
220 |
next |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
221 |
from `x \<in> interior A` show "0 \<in> ?A'" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
222 |
next |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
223 |
fix h assume "h \<in> ?A'" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
224 |
hence "x + h \<in> interior A" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
225 |
with mono' and `x \<in> interior A` show "(f (x + h) - f x) / h \<ge> 0" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
226 |
by (cases h rule: linorder_cases[of _ 0]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
227 |
(simp_all add: divide_nonpos_neg divide_nonneg_pos mono_onD field_simps) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
228 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
229 |
qed simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
230 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
231 |
lemma strict_mono_on_imp_mono_on: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
232 |
"strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
233 |
by (rule mono_onI, rule strict_mono_on_leD) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
234 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
235 |
lemma has_real_derivative_imp_continuous_on: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
236 |
assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
237 |
shows "continuous_on A f" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
238 |
apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
239 |
apply (intro ballI Deriv.differentiableI) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
240 |
apply (rule has_field_derivative_subset[OF assms]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
241 |
apply simp_all |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
242 |
done |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
243 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
244 |
lemma closure_contains_Sup: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
245 |
fixes S :: "real set" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
246 |
assumes "S \<noteq> {}" "bdd_above S" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
247 |
shows "Sup S \<in> closure S" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
248 |
proof- |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
249 |
have "Inf (uminus ` S) \<in> closure (uminus ` S)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
250 |
using assms by (intro closure_contains_Inf) auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
251 |
also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
252 |
also have "closure (uminus ` S) = uminus ` closure S" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
253 |
by (rule sym, intro closure_injective_linear_image) (auto intro: linearI) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
254 |
finally show ?thesis by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
255 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
256 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
257 |
lemma closed_contains_Sup: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
258 |
fixes S :: "real set" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
259 |
shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
260 |
by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
261 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
262 |
lemma deriv_nonneg_imp_mono: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
263 |
assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
264 |
assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
265 |
assumes ab: "a \<le> b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
266 |
shows "g a \<le> g b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
267 |
proof (cases "a < b") |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
268 |
assume "a < b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
269 |
from deriv have "\<forall>x. x \<ge> a \<and> x \<le> b \<longrightarrow> (g has_real_derivative g' x) (at x)" by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
270 |
from MVT2[OF `a < b` this] and deriv |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
271 |
obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
272 |
from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
273 |
with g_ab show ?thesis by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
274 |
qed (insert ab, simp) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
275 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
276 |
lemma continuous_interval_vimage_Int: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
277 |
assumes "continuous_on {a::real..b} g" and mono: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
278 |
assumes "a \<le> b" "(c::real) \<le> d" "{c..d} \<subseteq> {g a..g b}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
279 |
obtains c' d' where "{a..b} \<inter> g -` {c..d} = {c'..d'}" "c' \<le> d'" "g c' = c" "g d' = d" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
280 |
proof- |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
281 |
let ?A = "{a..b} \<inter> g -` {c..d}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
282 |
from IVT'[of g a c b, OF _ _ `a \<le> b` assms(1)] assms(4,5) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
283 |
obtain c'' where c'': "c'' \<in> ?A" "g c'' = c" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
284 |
from IVT'[of g a d b, OF _ _ `a \<le> b` assms(1)] assms(4,5) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
285 |
obtain d'' where d'': "d'' \<in> ?A" "g d'' = d" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
286 |
hence [simp]: "?A \<noteq> {}" by blast |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
287 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
288 |
def c' \<equiv> "Inf ?A" and d' \<equiv> "Sup ?A" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
289 |
have "?A \<subseteq> {c'..d'}" unfolding c'_def d'_def |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
290 |
by (intro subsetI) (auto intro: cInf_lower cSup_upper) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
291 |
moreover from assms have "closed ?A" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
292 |
using continuous_on_closed_vimage[of "{a..b}" g] by (subst Int_commute) simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
293 |
hence c'd'_in_set: "c' \<in> ?A" "d' \<in> ?A" unfolding c'_def d'_def |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
294 |
by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+ |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
295 |
hence "{c'..d'} \<subseteq> ?A" using assms |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
296 |
by (intro subsetI) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
297 |
(auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
298 |
intro!: mono) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
299 |
moreover have "c' \<le> d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
300 |
moreover have "g c' \<le> c" "g d' \<ge> d" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
301 |
apply (insert c'' d'' c'd'_in_set) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
302 |
apply (subst c''(2)[symmetric]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
303 |
apply (auto simp: c'_def intro!: mono cInf_lower c'') [] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
304 |
apply (subst d''(2)[symmetric]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
305 |
apply (auto simp: d'_def intro!: mono cSup_upper d'') [] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
306 |
done |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
307 |
with c'd'_in_set have "g c' = c" "g d' = d" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
308 |
ultimately show ?thesis using that by blast |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
309 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
310 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
311 |
lemma nn_integral_substitution_aux: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
312 |
fixes f :: "real \<Rightarrow> ereal" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
313 |
assumes Mf: "f \<in> borel_measurable borel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
314 |
assumes nonnegf: "\<And>x. f x \<ge> 0" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
315 |
assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
316 |
assumes contg': "continuous_on {a..b} g'" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
317 |
assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
318 |
assumes "a < b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
319 |
shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
320 |
(\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
321 |
proof- |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
322 |
from `a < b` have [simp]: "a \<le> b" by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
323 |
from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
324 |
from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
325 |
Mg': "set_borel_measurable borel {a..b} g'" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
326 |
by (simp_all only: set_measurable_continuous_on_ivl) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
327 |
from derivg have derivg': "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
328 |
by (simp only: has_field_derivative_iff_has_vector_derivative) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
329 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
330 |
have real_ind[simp]: "\<And>A x. real (indicator A x :: ereal) = indicator A x" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
331 |
by (auto split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
332 |
have ereal_ind[simp]: "\<And>A x. ereal (indicator A x) = indicator A x" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
333 |
by (auto split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
334 |
have [simp]: "\<And>x A. indicator A (g x) = indicator (g -` A) x" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
335 |
by (auto split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
336 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
337 |
from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
338 |
by (rule deriv_nonneg_imp_mono) simp_all |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
339 |
with monog have [simp]: "g a \<le> g b" by (auto intro: mono_onD) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
340 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
341 |
show ?thesis |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
342 |
proof (induction rule: borel_measurable_induct[OF Mf nonnegf, case_names cong set mult add sup]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
343 |
case (cong f1 f2) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
344 |
from cong.hyps(3) have "f1 = f2" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
345 |
with cong show ?case by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
346 |
next |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
347 |
case (set A) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
348 |
from set.hyps show ?case |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
349 |
proof (induction rule: borel_set_induct) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
350 |
case empty |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
351 |
thus ?case by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
352 |
next |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
353 |
case (interval c d) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
354 |
{ |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
355 |
fix u v :: real assume asm: "{u..v} \<subseteq> {g a..g b}" "u \<le> v" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
356 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
357 |
obtain u' v' where u'v': "{a..b} \<inter> g-`{u..v} = {u'..v'}" "u' \<le> v'" "g u' = u" "g v' = v" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
358 |
using asm by (rule_tac continuous_interval_vimage_Int[OF contg monog, of u v]) simp_all |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
359 |
hence "{u'..v'} \<subseteq> {a..b}" "{u'..v'} \<subseteq> g -` {u..v}" by blast+ |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
360 |
with u'v'(2) have "u' \<in> g -` {u..v}" "v' \<in> g -` {u..v}" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
361 |
from u'v'(1) have [simp]: "{a..b} \<inter> g -` {u..v} \<in> sets borel" by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
362 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
363 |
have A: "continuous_on {min u' v'..max u' v'} g'" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
364 |
by (simp only: u'v' max_absorb2 min_absorb1) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
365 |
(intro continuous_on_subset[OF contg'], insert u'v', auto) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
366 |
have "\<And>x. x \<in> {u'..v'} \<Longrightarrow> (g has_real_derivative g' x) (at x within {u'..v'})" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
367 |
using asm by (intro has_field_derivative_subset[OF derivg] set_mp[OF `{u'..v'} \<subseteq> {a..b}`]) auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
368 |
hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow> |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
369 |
(g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
370 |
by (simp only: u'v' max_absorb2 min_absorb1) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
371 |
(auto simp: has_field_derivative_iff_has_vector_derivative) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
372 |
have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
373 |
by (rule set_integrable_subset[OF borel_integrable_atLeastAtMost'[OF contg']]) simp_all |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
374 |
hence "(\<integral>\<^sup>+x. ereal (g' x) * indicator ({a..b} \<inter> g-` {u..v}) x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
375 |
LBINT x:{a..b} \<inter> g-`{u..v}. g' x" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
376 |
by (subst ereal_ind[symmetric], subst times_ereal.simps, subst nn_integral_eq_integral) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
377 |
(auto intro: measurable_sets Mg simp: derivg_nonneg mult.commute split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
378 |
also from interval_integral_FTC_finite[OF A B] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
379 |
have "LBINT x:{a..b} \<inter> g-`{u..v}. g' x = v - u" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
380 |
by (simp add: u'v' interval_integral_Icc `u \<le> v`) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
381 |
finally have "(\<integral>\<^sup>+ x. ereal (g' x) * indicator ({a..b} \<inter> g -` {u..v}) x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
382 |
ereal (v - u)" . |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
383 |
} note A = this |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
384 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
385 |
have "(\<integral>\<^sup>+x. indicator {c..d} (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
386 |
(\<integral>\<^sup>+ x. ereal (g' x) * indicator ({a..b} \<inter> g -` {c..d}) x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
387 |
by (intro nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
388 |
also have "{a..b} \<inter> g-`{c..d} = {a..b} \<inter> g-`{max (g a) c..min (g b) d}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
389 |
using `a \<le> b` `c \<le> d` |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
390 |
by (auto intro!: monog intro: order.trans) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
391 |
also have "(\<integral>\<^sup>+ x. ereal (g' x) * indicator ... x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
392 |
(if max (g a) c \<le> min (g b) d then min (g b) d - max (g a) c else 0)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
393 |
using `c \<le> d` by (simp add: A) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
394 |
also have "... = (\<integral>\<^sup>+ x. indicator ({g a..g b} \<inter> {c..d}) x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
395 |
by (subst nn_integral_indicator) (auto intro!: measurable_sets Mg simp:) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
396 |
also have "... = (\<integral>\<^sup>+ x. indicator {c..d} x * indicator {g a..g b} x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
397 |
by (intro nn_integral_cong) (auto split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
398 |
finally show ?case .. |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
399 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
400 |
next |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
401 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
402 |
case (compl A) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
403 |
note `A \<in> sets borel`[measurable] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
404 |
from emeasure_mono[of "A \<inter> {g a..g b}" "{g a..g b}" lborel] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
405 |
have [simp]: "emeasure lborel (A \<inter> {g a..g b}) \<noteq> \<infinity>" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
406 |
have [simp]: "g -` A \<inter> {a..b} \<in> sets borel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
407 |
by (rule set_borel_measurable_sets[OF Mg]) auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
408 |
have [simp]: "g -` (-A) \<inter> {a..b} \<in> sets borel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
409 |
by (rule set_borel_measurable_sets[OF Mg]) auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
410 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
411 |
have "(\<integral>\<^sup>+x. indicator (-A) x * indicator {g a..g b} x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
412 |
(\<integral>\<^sup>+x. indicator (-A \<inter> {g a..g b}) x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
413 |
by (rule nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
414 |
also from compl have "... = emeasure lborel ({g a..g b} - A)" using derivg_nonneg |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
415 |
by (simp add: vimage_Compl diff_eq Int_commute[of "-A"]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
416 |
also have "{g a..g b} - A = {g a..g b} - A \<inter> {g a..g b}" by blast |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
417 |
also have "emeasure lborel ... = g b - g a - emeasure lborel (A \<inter> {g a..g b})" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
418 |
using `A \<in> sets borel` by (subst emeasure_Diff) (auto simp: real_of_ereal_minus) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
419 |
also have "emeasure lborel (A \<inter> {g a..g b}) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
420 |
\<integral>\<^sup>+x. indicator A x * indicator {g a..g b} x \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
421 |
using `A \<in> sets borel` |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
422 |
by (subst nn_integral_indicator[symmetric], simp, intro nn_integral_cong) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
423 |
(simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
424 |
also have "... = \<integral>\<^sup>+ x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel" (is "_ = ?I") |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
425 |
by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
426 |
also have "g b - g a = LBINT x:{a..b}. g' x" using derivg' |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
427 |
by (intro integral_FTC_atLeastAtMost[symmetric]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
428 |
(auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
429 |
has_vector_derivative_at_within) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
430 |
also have "ereal ... = \<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
431 |
using borel_integrable_atLeastAtMost'[OF contg'] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
432 |
by (subst nn_integral_eq_integral) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
433 |
(simp_all add: mult.commute derivg_nonneg split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
434 |
also have Mg'': "(\<lambda>x. indicator (g -` A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x)) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
435 |
\<in> borel_measurable borel" using Mg' |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
436 |
by (intro borel_measurable_ereal_times borel_measurable_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
437 |
(simp_all add: mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
438 |
have le: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel) \<le> |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
439 |
(\<integral>\<^sup>+x. ereal (g' x) * indicator {a..b} x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
440 |
by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
441 |
note integrable = borel_integrable_atLeastAtMost'[OF contg'] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
442 |
with le have notinf: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel) \<noteq> \<infinity>" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
443 |
by (auto simp: real_integrable_def nn_integral_set_ereal mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
444 |
have "(\<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel) - ?I = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
445 |
\<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) - |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
446 |
indicator (g -` A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
447 |
apply (intro nn_integral_diff[symmetric]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
448 |
apply (insert Mg', simp add: mult.commute) [] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
449 |
apply (insert Mg'', simp) [] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
450 |
apply (simp split: split_indicator add: derivg_nonneg) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
451 |
apply (rule notinf) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
452 |
apply (simp split: split_indicator add: derivg_nonneg) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
453 |
done |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
454 |
also have "... = \<integral>\<^sup>+ x. indicator (-A) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
455 |
by (intro nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
456 |
finally show ?case . |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
457 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
458 |
next |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
459 |
case (union f) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
460 |
then have [simp]: "\<And>i. {a..b} \<inter> g -` f i \<in> sets borel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
461 |
by (subst Int_commute, intro set_borel_measurable_sets[OF Mg]) auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
462 |
have "g -` (\<Union>i. f i) \<inter> {a..b} = (\<Union>i. {a..b} \<inter> g -` f i)" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
463 |
hence "g -` (\<Union>i. f i) \<inter> {a..b} \<in> sets borel" by (auto simp del: UN_simps) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
464 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
465 |
have "(\<integral>\<^sup>+x. indicator (\<Union>i. f i) x * indicator {g a..g b} x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
466 |
\<integral>\<^sup>+x. indicator (\<Union>i. {g a..g b} \<inter> f i) x \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
467 |
by (intro nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
468 |
also from union have "... = emeasure lborel (\<Union>i. {g a..g b} \<inter> f i)" by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
469 |
also from union have "... = (\<Sum>i. emeasure lborel ({g a..g b} \<inter> f i))" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
470 |
by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
471 |
also from union have "... = (\<Sum>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel)" by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
472 |
also have "(\<lambda>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
473 |
(\<lambda>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
474 |
by (intro ext nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
475 |
also from union.IH have "(\<Sum>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
476 |
(\<Sum>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)" by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
477 |
also have "(\<lambda>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
478 |
(\<lambda>i. \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
479 |
by (intro ext nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
480 |
also have "(\<Sum>i. ... i) = \<integral>\<^sup>+ x. (\<Sum>i. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
481 |
using Mg' |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
482 |
apply (intro nn_integral_suminf[symmetric]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
483 |
apply (rule borel_measurable_ereal_times, simp add: borel_measurable_ereal mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
484 |
apply (rule borel_measurable_indicator, subst sets_lborel) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
485 |
apply (simp_all split: split_indicator add: derivg_nonneg) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
486 |
done |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
487 |
also have "(\<lambda>x i. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
488 |
(\<lambda>x i. ereal (g' x * indicator {a..b} x) * indicator (g -` f i) x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
489 |
by (intro ext) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
490 |
also have "(\<integral>\<^sup>+ x. (\<Sum>i. ereal (g' x * indicator {a..b} x) * indicator (g -` f i) x) \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
491 |
\<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) * (\<Sum>i. indicator (g -` f i) x) \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
492 |
by (intro nn_integral_cong suminf_cmult_ereal) (auto split: split_indicator simp: derivg_nonneg) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
493 |
also from union have "(\<lambda>x. \<Sum>i. indicator (g -` f i) x :: ereal) = (\<lambda>x. indicator (\<Union>i. g -` f i) x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
494 |
by (intro ext suminf_indicator) (auto simp: disjoint_family_on_def) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
495 |
also have "(\<integral>\<^sup>+x. ereal (g' x * indicator {a..b} x) * ... x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
496 |
(\<integral>\<^sup>+x. indicator (\<Union>i. f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
497 |
by (intro nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
498 |
finally show ?case . |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
499 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
500 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
501 |
next |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
502 |
case (mult f c) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
503 |
note Mf[measurable] = `f \<in> borel_measurable borel` |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
504 |
let ?I = "indicator {a..b}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
505 |
have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg' |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
506 |
by (intro borel_measurable_ereal_times measurable_compose[OF _ Mf]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
507 |
(simp_all add: borel_measurable_ereal mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
508 |
also have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. f (g x) * ereal (g' x) * ?I x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
509 |
by (intro ext) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
510 |
finally have Mf': "(\<lambda>x. f (g x) * ereal (g' x) * ?I x) \<in> borel_measurable borel" . |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
511 |
with mult show ?case |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
512 |
by (subst (1 2 3) mult_ac, subst (1 2) nn_integral_cmult) (simp_all add: mult_ac) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
513 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
514 |
next |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
515 |
case (add f2 f1) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
516 |
let ?I = "indicator {a..b}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
517 |
{ |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
518 |
fix f :: "real \<Rightarrow> ereal" assume Mf: "f \<in> borel_measurable borel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
519 |
have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg' |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
520 |
by (intro borel_measurable_ereal_times measurable_compose[OF _ Mf]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
521 |
(simp_all add: borel_measurable_ereal mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
522 |
also have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. f (g x) * ereal (g' x) * ?I x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
523 |
by (intro ext) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
524 |
finally have "(\<lambda>x. f (g x) * ereal (g' x) * ?I x) \<in> borel_measurable borel" . |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
525 |
} note Mf' = this[OF `f1 \<in> borel_measurable borel`] this[OF `f2 \<in> borel_measurable borel`] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
526 |
from add have not_neginf: "\<And>x. f1 x \<noteq> -\<infinity>" "\<And>x. f2 x \<noteq> -\<infinity>" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
527 |
by (metis Infty_neq_0(1) ereal_0_le_uminus_iff ereal_infty_less_eq(1))+ |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
528 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
529 |
have "(\<integral>\<^sup>+ x. (f1 x + f2 x) * indicator {g a..g b} x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
530 |
(\<integral>\<^sup>+ x. f1 x * indicator {g a..g b} x + f2 x * indicator {g a..g b} x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
531 |
by (intro nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
532 |
also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) + |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
533 |
(\<integral>\<^sup>+ x. f2 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
534 |
by (simp_all add: nn_integral_add) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
535 |
also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ereal (g' x) * indicator {a..b} x + |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
536 |
f2 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
537 |
by (intro nn_integral_add[symmetric]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
538 |
(auto simp add: Mf' derivg_nonneg split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
539 |
also from not_neginf have "... = \<integral>\<^sup>+ x. (f1 (g x) + f2 (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
540 |
by (intro nn_integral_cong) (simp split: split_indicator add: ereal_distrib) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
541 |
finally show ?case . |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
542 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
543 |
next |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
544 |
case (sup F) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
545 |
{ |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
546 |
fix i |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
547 |
let ?I = "indicator {a..b}" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
548 |
have "(\<lambda>x. F i (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg' |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
549 |
by (rule_tac borel_measurable_ereal_times, rule_tac measurable_compose[OF _ sup.hyps(1)]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
550 |
(simp_all add: mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
551 |
also have "(\<lambda>x. F i (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. F i (g x) * ereal (g' x) * ?I x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
552 |
by (intro ext) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
553 |
finally have "... \<in> borel_measurable borel" . |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
554 |
} note Mf' = this |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
555 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
556 |
have "(\<integral>\<^sup>+x. (SUP i. F i x) * indicator {g a..g b} x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
557 |
\<integral>\<^sup>+x. (SUP i. F i x* indicator {g a..g b} x) \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
558 |
by (intro nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
559 |
also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i x* indicator {g a..g b} x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
560 |
by (intro nn_integral_monotone_convergence_SUP) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
561 |
(auto simp: incseq_def le_fun_def split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
562 |
also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
563 |
by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
564 |
also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x) * ereal (g' x) * indicator {a..b} x) \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
565 |
by (intro nn_integral_monotone_convergence_SUP[symmetric]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
566 |
(auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
567 |
intro!: ereal_mult_right_mono) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
568 |
also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel" |
59452
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
59092
diff
changeset
|
569 |
by (subst mult.assoc, subst mult.commute, subst SUP_ereal_mult_left) |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
570 |
(auto split: split_indicator simp: derivg_nonneg mult_ac) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
571 |
finally show ?case by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
572 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
573 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
574 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
575 |
lemma nn_integral_substitution: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
576 |
fixes f :: "real \<Rightarrow> real" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
577 |
assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
578 |
assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
579 |
assumes contg': "continuous_on {a..b} g'" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
580 |
assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
581 |
assumes "a \<le> b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
582 |
shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
583 |
(\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
584 |
proof (cases "a = b") |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
585 |
assume "a \<noteq> b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
586 |
with `a \<le> b` have "a < b" by auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
587 |
let ?f' = "\<lambda>x. max 0 (f x * indicator {g a..g b} x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
588 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
589 |
from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
590 |
by (rule deriv_nonneg_imp_mono) simp_all |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
591 |
have bounds: "\<And>x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g x \<ge> g a" "\<And>x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g x \<le> g b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
592 |
by (auto intro: monog) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
593 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
594 |
from derivg_nonneg have nonneg: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
595 |
"\<And>f x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g' x \<noteq> 0 \<Longrightarrow> f x * ereal (g' x) \<ge> 0 \<Longrightarrow> f x \<ge> 0" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
596 |
by (force simp: ereal_zero_le_0_iff field_simps) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
597 |
have nonneg': "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<not> 0 \<le> f (g x) \<Longrightarrow> 0 \<le> f (g x) * g' x \<Longrightarrow> g' x = 0" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
598 |
by (metis atLeastAtMost_iff derivg_nonneg eq_iff mult_eq_0_iff mult_le_0_iff) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
599 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
600 |
have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
601 |
(\<integral>\<^sup>+x. ereal (?f' x) * indicator {g a..g b} x \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
602 |
by (subst nn_integral_max_0[symmetric], intro nn_integral_cong) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
603 |
(auto split: split_indicator simp: zero_ereal_def) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
604 |
also have "... = \<integral>\<^sup>+ x. ?f' (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel" using Mf |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
605 |
by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg `a < b`]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
606 |
(auto simp add: zero_ereal_def mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
607 |
also have "... = \<integral>\<^sup>+ x. max 0 (f (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
608 |
by (intro nn_integral_cong) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
609 |
(auto split: split_indicator simp: max_def dest: bounds) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
610 |
also have "... = \<integral>\<^sup>+ x. max 0 (f (g x) * ereal (g' x) * indicator {a..b} x) \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
611 |
by (intro nn_integral_cong) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
612 |
(auto simp: max_def derivg_nonneg split: split_indicator intro!: nonneg') |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
613 |
also have "... = \<integral>\<^sup>+ x. f (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
614 |
by (rule nn_integral_max_0) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
615 |
also have "... = \<integral>\<^sup>+x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
616 |
by (intro nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
617 |
finally show ?thesis . |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
618 |
qed auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
619 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
620 |
lemma integral_substitution: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
621 |
assumes integrable: "set_integrable lborel {g a..g b} f" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
622 |
assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
623 |
assumes contg': "continuous_on {a..b} g'" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
624 |
assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
625 |
assumes "a \<le> b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
626 |
shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
627 |
and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
628 |
proof- |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
629 |
from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
630 |
from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
631 |
Mg': "set_borel_measurable borel {a..b} g'" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
632 |
by (simp_all only: set_measurable_continuous_on_ivl) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
633 |
from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
634 |
by (rule deriv_nonneg_imp_mono) simp_all |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
635 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
636 |
have "(\<lambda>x. ereal (f x) * indicator {g a..g b} x) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
637 |
(\<lambda>x. ereal (f x * indicator {g a..g b} x))" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
638 |
by (intro ext) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
639 |
with integrable have M1: "(\<lambda>x. f x * indicator {g a..g b} x) \<in> borel_measurable borel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
640 |
unfolding real_integrable_def by (force simp: mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
641 |
have "(\<lambda>x. ereal (-f x) * indicator {g a..g b} x) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
642 |
(\<lambda>x. -ereal (f x * indicator {g a..g b} x))" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
643 |
by (intro ext) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
644 |
with integrable have M2: "(\<lambda>x. -f x * indicator {g a..g b} x) \<in> borel_measurable borel" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
645 |
unfolding real_integrable_def by (force simp: mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
646 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
647 |
have "LBINT x. (f x :: real) * indicator {g a..g b} x = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
648 |
real (\<integral>\<^sup>+ x. ereal (f x) * indicator {g a..g b} x \<partial>lborel) - |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
649 |
real (\<integral>\<^sup>+ x. ereal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
650 |
by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ereal mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
651 |
also have "(\<integral>\<^sup>+x. ereal (f x) * indicator {g a..g b} x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
652 |
(\<integral>\<^sup>+x. ereal (f x * indicator {g a..g b} x) \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
653 |
by (intro nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
654 |
also with M1 have A: "(\<integral>\<^sup>+ x. ereal (f x * indicator {g a..g b} x) \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
655 |
(\<integral>\<^sup>+ x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
656 |
by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg `a \<le> b`]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
657 |
(auto simp: nn_integral_set_ereal mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
658 |
also have "(\<integral>\<^sup>+ x. ereal (- (f x)) * indicator {g a..g b} x \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
659 |
(\<integral>\<^sup>+ x. ereal (- (f x) * indicator {g a..g b} x) \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
660 |
by (intro nn_integral_cong) (simp split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
661 |
also with M2 have B: "(\<integral>\<^sup>+ x. ereal (- (f x) * indicator {g a..g b} x) \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
662 |
(\<integral>\<^sup>+ x. ereal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
663 |
by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg `a \<le> b`]) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
664 |
(auto simp: nn_integral_set_ereal mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
665 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
666 |
also { |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
667 |
from integrable have Mf: "set_borel_measurable borel {g a..g b} f" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
668 |
unfolding real_integrable_def by simp |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
669 |
from borel_measurable_times[OF measurable_compose[OF Mg Mf] Mg'] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
670 |
have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) * |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
671 |
(g' x * indicator {a..b} x)) \<in> borel_measurable borel" (is "?f \<in> _") |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
672 |
by (simp add: mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
673 |
also have "?f = (\<lambda>x. f (g x) * g' x * indicator {a..b} x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
674 |
using monog by (intro ext) (auto split: split_indicator) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
675 |
finally show "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
676 |
using A B integrable unfolding real_integrable_def |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
677 |
by (simp_all add: nn_integral_set_ereal mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
678 |
} note integrable' = this |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
679 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
680 |
have "real (\<integral>\<^sup>+ x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel) - |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
681 |
real (\<integral>\<^sup>+ x. ereal (-f (g x) * g' x * indicator {a..b} x) \<partial>lborel) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
682 |
(LBINT x. f (g x) * g' x * indicator {a..b} x)" using integrable' |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
683 |
by (subst real_lebesgue_integral_def) (simp_all add: field_simps) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
684 |
finally show "(LBINT x. f x * indicator {g a..g b} x) = |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
685 |
(LBINT x. f (g x) * g' x * indicator {a..b} x)" . |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
686 |
qed |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
687 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
688 |
lemma interval_integral_substitution: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
689 |
assumes integrable: "set_integrable lborel {g a..g b} f" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
690 |
assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
691 |
assumes contg': "continuous_on {a..b} g'" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
692 |
assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
693 |
assumes "a \<le> b" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
694 |
shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
695 |
and "(LBINT x=g a..g b. f x) = (LBINT x=a..b. f (g x) * g' x)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
696 |
apply (rule integral_substitution[OF assms], simp, simp) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
697 |
apply (subst (1 2) interval_integral_Icc, fact) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
698 |
apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
699 |
using integral_substitution(2)[OF assms] |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
700 |
apply (simp add: mult.commute) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
701 |
done |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
702 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
703 |
lemma set_borel_integrable_singleton[simp]: |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
704 |
"set_integrable lborel {x} (f :: real \<Rightarrow> real)" |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
705 |
by (subst integrable_discrete_difference[where X="{x}" and g="\<lambda>_. 0"]) auto |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
706 |
|
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff
changeset
|
707 |
end |