changeset 61190 | 2bd401e364f9 |
parent 61104 | 3c2d4636cebc |
child 61200 | a5674da43c2b |
61105:44baf4d5e375 | 61190:2bd401e364f9 |
---|---|
2 |
2 |
3 theory Cauchy_Integral_Thm |
3 theory Cauchy_Integral_Thm |
4 imports Complex_Transcendental Weierstrass |
4 imports Complex_Transcendental Weierstrass |
5 begin |
5 begin |
6 |
6 |
7 (*FIXME migrate into libraries*) |
|
8 |
|
9 lemma inj_mult_left [simp]: "inj (op* x) \<longleftrightarrow> x \<noteq> (0::'a::idom)" |
|
10 by (metis injI mult_cancel_left the_inv_f_f zero_neq_one) |
|
11 |
|
12 lemma continuous_on_strong_cong: |
|
13 "s = t \<Longrightarrow> (\<And>x. x \<in> t =simp=> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g" |
|
14 by (simp add: simp_implies_def) |
|
15 |
|
16 thm image_affinity_atLeastAtMost_div_diff |
|
17 lemma image_affinity_atLeastAtMost_div: |
|
18 fixes c :: "'a::linordered_field" |
|
19 shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {} |
|
20 else if 0 \<le> m then {a/m + c .. b/m + c} |
|
21 else {b/m + c .. a/m + c})" |
|
22 using image_affinity_atLeastAtMost [of "inverse m" c a b] |
|
23 by (simp add: field_class.field_divide_inverse algebra_simps) |
|
24 |
|
25 thm continuous_on_closed_Un |
|
26 lemma continuous_on_open_Un: |
|
27 "open s \<Longrightarrow> open t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f" |
|
28 using continuous_on_open_Union [of "{s,t}"] by auto |
|
29 |
|
30 thm continuous_on_eq (*REPLACE*) |
|
31 lemma continuous_on_eq: |
|
32 "\<lbrakk>continuous_on s f; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> continuous_on s g" |
|
33 unfolding continuous_on_def tendsto_def eventually_at_topological |
|
34 by simp |
|
35 |
|
36 thm vector_derivative_add_at |
|
37 lemma vector_derivative_mult_at [simp]: |
|
38 fixes f g :: "real \<Rightarrow> 'a :: real_normed_algebra" |
|
39 shows "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk> |
|
40 \<Longrightarrow> vector_derivative (\<lambda>x. f x * g x) (at a) = f a * vector_derivative g (at a) + vector_derivative f (at a) * g a" |
|
41 by (simp add: vector_derivative_at has_vector_derivative_mult vector_derivative_works [symmetric]) |
|
42 |
|
43 lemma vector_derivative_scaleR_at [simp]: |
|
44 "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk> |
|
45 \<Longrightarrow> vector_derivative (\<lambda>x. f x *\<^sub>R g x) (at a) = f a *\<^sub>R vector_derivative g (at a) + vector_derivative f (at a) *\<^sub>R g a" |
|
46 apply (rule vector_derivative_at) |
|
47 apply (rule has_vector_derivative_scaleR) |
|
48 apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs) |
|
49 done |
|
50 |
|
51 thm Derivative.vector_diff_chain_at |
|
52 lemma vector_derivative_chain_at: |
|
53 assumes "f differentiable at x" "(g differentiable at (f x))" |
|
54 shows "vector_derivative (g \<circ> f) (at x) = |
|
55 vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))" |
|
56 by (metis Derivative.vector_diff_chain_at vector_derivative_at vector_derivative_works assms) |
|
57 |
|
58 |
|
59 subsection \<open>Piecewise differentiable functions\<close> |
|
7 |
60 |
8 definition piecewise_differentiable_on |
61 definition piecewise_differentiable_on |
9 (infixr "piecewise'_differentiable'_on" 50) |
62 (infixr "piecewise'_differentiable'_on" 50) |
10 where "f piecewise_differentiable_on i \<equiv> |
63 where "f piecewise_differentiable_on i \<equiv> |
11 continuous_on i f \<and> |
64 continuous_on i f \<and> |
12 (\<exists>s. finite s \<and> (\<forall>x \<in> i - s. f differentiable (at x)))" |
65 (\<exists>s. finite s \<and> (\<forall>x \<in> i - s. f differentiable (at x within i)))" |
13 |
66 |
14 lemma piecewise_differentiable_on_imp_continuous_on: |
67 lemma piecewise_differentiable_on_imp_continuous_on: |
15 "f piecewise_differentiable_on s \<Longrightarrow> continuous_on s f" |
68 "f piecewise_differentiable_on s \<Longrightarrow> continuous_on s f" |
16 by (simp add: piecewise_differentiable_on_def) |
69 by (simp add: piecewise_differentiable_on_def) |
17 |
70 |
18 lemma piecewise_differentiable_on_subset: |
71 lemma piecewise_differentiable_on_subset: |
19 "f piecewise_differentiable_on s \<Longrightarrow> t \<le> s \<Longrightarrow> f piecewise_differentiable_on t" |
72 "f piecewise_differentiable_on s \<Longrightarrow> t \<le> s \<Longrightarrow> f piecewise_differentiable_on t" |
20 using continuous_on_subset |
73 using continuous_on_subset |
21 by (fastforce simp: piecewise_differentiable_on_def) |
74 unfolding piecewise_differentiable_on_def |
75 apply safe |
|
76 apply (blast intro: elim: continuous_on_subset) |
|
77 by (meson Diff_iff differentiable_within_subset subsetCE) |
|
22 |
78 |
23 lemma differentiable_on_imp_piecewise_differentiable: |
79 lemma differentiable_on_imp_piecewise_differentiable: |
24 fixes a:: "'a::{linorder_topology,real_normed_vector}" |
80 fixes a:: "'a::{linorder_topology,real_normed_vector}" |
25 shows "f differentiable_on {a..b} \<Longrightarrow> f piecewise_differentiable_on {a..b}" |
81 shows "f differentiable_on {a..b} \<Longrightarrow> f piecewise_differentiable_on {a..b}" |
26 apply (simp add: piecewise_differentiable_on_def differentiable_imp_continuous_on) |
82 apply (simp add: piecewise_differentiable_on_def differentiable_imp_continuous_on) |
27 apply (rule_tac x="{a,b}" in exI, simp) |
83 apply (rule_tac x="{a,b}" in exI, simp add: differentiable_on_def) |
28 by (metis DiffE atLeastAtMost_diff_ends differentiable_on_subset subsetI |
84 done |
29 differentiable_on_eq_differentiable_at open_greaterThanLessThan) |
|
30 |
85 |
31 lemma differentiable_imp_piecewise_differentiable: |
86 lemma differentiable_imp_piecewise_differentiable: |
32 "(\<And>x. x \<in> s \<Longrightarrow> f differentiable (at x)) |
87 "(\<And>x. x \<in> s \<Longrightarrow> f differentiable (at x within s)) |
33 \<Longrightarrow> f piecewise_differentiable_on s" |
88 \<Longrightarrow> f piecewise_differentiable_on s" |
34 by (auto simp: piecewise_differentiable_on_def differentiable_on_eq_differentiable_at |
89 by (auto simp: piecewise_differentiable_on_def differentiable_imp_continuous_on differentiable_on_def |
35 differentiable_imp_continuous_within continuous_at_imp_continuous_on) |
90 intro: differentiable_within_subset) |
36 |
91 |
37 lemma piecewise_differentiable_compose: |
92 lemma piecewise_differentiable_compose: |
38 "\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on (f ` s); |
93 "\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on (f ` s); |
39 \<And>x. finite (s \<inter> f-`{x})\<rbrakk> |
94 \<And>x. finite (s \<inter> f-`{x})\<rbrakk> |
40 \<Longrightarrow> (g o f) piecewise_differentiable_on s" |
95 \<Longrightarrow> (g o f) piecewise_differentiable_on s" |
41 apply (simp add: piecewise_differentiable_on_def, safe) |
96 apply (simp add: piecewise_differentiable_on_def, safe) |
42 apply (blast intro: continuous_on_compose2) |
97 apply (blast intro: continuous_on_compose2) |
43 apply (rename_tac A B) |
98 apply (rename_tac A B) |
44 apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f-`{x})" in exI) |
99 apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f-`{x})" in exI) |
45 using differentiable_chain_at by blast |
100 apply (blast intro: differentiable_chain_within) |
101 done |
|
46 |
102 |
47 lemma piecewise_differentiable_affine: |
103 lemma piecewise_differentiable_affine: |
48 fixes m::real |
104 fixes m::real |
49 assumes "f piecewise_differentiable_on ((\<lambda>x. m *\<^sub>R x + c) ` s)" |
105 assumes "f piecewise_differentiable_on ((\<lambda>x. m *\<^sub>R x + c) ` s)" |
50 shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_differentiable_on s" |
106 shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_differentiable_on s" |
67 "g piecewise_differentiable_on {c..b}" |
123 "g piecewise_differentiable_on {c..b}" |
68 "a \<le> c" "c \<le> b" "f c = g c" |
124 "a \<le> c" "c \<le> b" "f c = g c" |
69 shows "(\<lambda>x. if x \<le> c then f x else g x) piecewise_differentiable_on {a..b}" |
125 shows "(\<lambda>x. if x \<le> c then f x else g x) piecewise_differentiable_on {a..b}" |
70 proof - |
126 proof - |
71 obtain s t where st: "finite s" "finite t" |
127 obtain s t where st: "finite s" "finite t" |
72 "\<forall>x\<in>{a..c} - s. f differentiable at x" |
128 "\<forall>x\<in>{a..c} - s. f differentiable at x within {a..c}" |
73 "\<forall>x\<in>{c..b} - t. g differentiable at x" |
129 "\<forall>x\<in>{c..b} - t. g differentiable at x within {c..b}" |
74 using assms |
130 using assms |
75 by (auto simp: piecewise_differentiable_on_def) |
131 by (auto simp: piecewise_differentiable_on_def) |
132 have finabc: "finite ({a,b,c} \<union> (s \<union> t))" |
|
133 by (metis `finite s` `finite t` finite_Un finite_insert finite.emptyI) |
|
76 have "continuous_on {a..c} f" "continuous_on {c..b} g" |
134 have "continuous_on {a..c} f" "continuous_on {c..b} g" |
77 using assms piecewise_differentiable_on_def by auto |
135 using assms piecewise_differentiable_on_def by auto |
78 then have "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)" |
136 then have "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)" |
79 using continuous_on_cases [OF closed_real_atLeastAtMost [of a c], |
137 using continuous_on_cases [OF closed_real_atLeastAtMost [of a c], |
80 OF closed_real_atLeastAtMost [of c b], |
138 OF closed_real_atLeastAtMost [of c b], |
81 of f g "\<lambda>x. x\<le>c"] assms |
139 of f g "\<lambda>x. x\<le>c"] assms |
82 by (force simp: ivl_disj_un_two_touch) |
140 by (force simp: ivl_disj_un_two_touch) |
83 moreover |
141 moreover |
84 { fix x |
142 { fix x |
143 assume x: "x \<in> {a..b} - ({a,b,c} \<union> (s \<union> t))" |
|
144 have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b}" (is "?diff_fg") |
|
145 proof (cases x c rule: le_cases) |
|
146 case le show ?diff_fg |
|
147 apply (rule differentiable_transform_within [where d = "dist x c" and f = f]) |
|
148 using x le st |
|
149 apply (simp_all add: dist_real_def dist_nz [symmetric]) |
|
150 apply (rule differentiable_at_withinI) |
|
151 apply (rule differentiable_within_open [where s = "{a<..<c} - s", THEN iffD1], simp_all) |
|
152 apply (blast intro: open_greaterThanLessThan finite_imp_closed) |
|
153 apply (force elim!: differentiable_subset) |
|
154 done |
|
155 next |
|
156 case ge show ?diff_fg |
|
157 apply (rule differentiable_transform_within [where d = "dist x c" and f = g]) |
|
158 using x ge st |
|
159 apply (simp_all add: dist_real_def dist_nz [symmetric]) |
|
160 apply (rule differentiable_at_withinI) |
|
161 apply (rule differentiable_within_open [where s = "{c<..<b} - t", THEN iffD1], simp_all) |
|
162 apply (blast intro: open_greaterThanLessThan finite_imp_closed) |
|
163 apply (force elim!: differentiable_subset) |
|
164 done |
|
165 qed |
|
166 } |
|
167 then have "\<exists>s. finite s \<and> |
|
168 (\<forall>x\<in>{a..b} - s. (\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b})" |
|
169 by (meson finabc) |
|
170 ultimately show ?thesis |
|
171 by (simp add: piecewise_differentiable_on_def) |
|
172 qed |
|
173 |
|
174 lemma piecewise_differentiable_neg: |
|
175 "f piecewise_differentiable_on s \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_differentiable_on s" |
|
176 by (auto simp: piecewise_differentiable_on_def continuous_on_minus) |
|
177 |
|
178 lemma piecewise_differentiable_add: |
|
179 assumes "f piecewise_differentiable_on i" |
|
180 "g piecewise_differentiable_on i" |
|
181 shows "(\<lambda>x. f x + g x) piecewise_differentiable_on i" |
|
182 proof - |
|
183 obtain s t where st: "finite s" "finite t" |
|
184 "\<forall>x\<in>i - s. f differentiable at x within i" |
|
185 "\<forall>x\<in>i - t. g differentiable at x within i" |
|
186 using assms by (auto simp: piecewise_differentiable_on_def) |
|
187 then have "finite (s \<union> t) \<and> (\<forall>x\<in>i - (s \<union> t). (\<lambda>x. f x + g x) differentiable at x within i)" |
|
188 by auto |
|
189 moreover have "continuous_on i f" "continuous_on i g" |
|
190 using assms piecewise_differentiable_on_def by auto |
|
191 ultimately show ?thesis |
|
192 by (auto simp: piecewise_differentiable_on_def continuous_on_add) |
|
193 qed |
|
194 |
|
195 lemma piecewise_differentiable_diff: |
|
196 "\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on s\<rbrakk> |
|
197 \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_differentiable_on s" |
|
198 unfolding diff_conv_add_uminus |
|
199 by (metis piecewise_differentiable_add piecewise_differentiable_neg) |
|
200 |
|
201 lemma continuous_on_joinpaths_D1: |
|
202 "continuous_on {0..1} (g1 +++ g2) \<Longrightarrow> continuous_on {0..1} g1" |
|
203 apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (op*(inverse 2))"]) |
|
204 apply (rule continuous_intros | simp)+ |
|
205 apply (auto elim!: continuous_on_subset simp: joinpaths_def) |
|
206 done |
|
207 |
|
208 lemma continuous_on_joinpaths_D2: |
|
209 "\<lbrakk>continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> continuous_on {0..1} g2" |
|
210 apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (\<lambda>x. inverse 2*x + 1/2)"]) |
|
211 apply (rule continuous_intros | simp)+ |
|
212 apply (auto elim!: continuous_on_subset simp add: joinpaths_def pathfinish_def pathstart_def Ball_def) |
|
213 done |
|
214 |
|
215 lemma piecewise_differentiable_D1: |
|
216 "(g1 +++ g2) piecewise_differentiable_on {0..1} \<Longrightarrow> g1 piecewise_differentiable_on {0..1}" |
|
217 apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D1) |
|
218 apply (rule_tac x="insert 1 ((op*2)`s)" in exI) |
|
219 apply simp |
|
220 apply (intro ballI) |
|
221 apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" |
|
222 in differentiable_transform_within) |
|
223 apply (auto simp: dist_real_def joinpaths_def) |
|
224 apply (rule differentiable_chain_within derivative_intros | simp)+ |
|
225 apply (rule differentiable_subset) |
|
226 apply (force simp:)+ |
|
227 done |
|
228 |
|
229 lemma piecewise_differentiable_D2: |
|
230 "\<lbrakk>(g1 +++ g2) piecewise_differentiable_on {0..1}; pathfinish g1 = pathstart g2\<rbrakk> |
|
231 \<Longrightarrow> g2 piecewise_differentiable_on {0..1}" |
|
232 apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D2) |
|
233 apply (rule_tac x="insert 0 ((\<lambda>x. 2*x-1)`s)" in exI) |
|
234 apply simp |
|
235 apply (intro ballI) |
|
236 apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" |
|
237 in differentiable_transform_within) |
|
238 apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: split_if_asm) |
|
239 apply (rule differentiable_chain_within derivative_intros | simp)+ |
|
240 apply (rule differentiable_subset) |
|
241 apply (force simp: divide_simps)+ |
|
242 done |
|
243 |
|
244 |
|
245 subsubsection\<open>The concept of continuously differentiable\<close> |
|
246 |
|
247 definition C1_differentiable_on :: "(real \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> real set \<Rightarrow> bool" |
|
248 (infix "C1'_differentiable'_on" 50) |
|
249 where |
|
250 "f C1_differentiable_on s \<longleftrightarrow> |
|
251 (\<exists>D. (\<forall>x \<in> s. (f has_vector_derivative (D x)) (at x)) \<and> continuous_on s D)" |
|
252 |
|
253 lemma C1_differentiable_on_eq: |
|
254 "f C1_differentiable_on s \<longleftrightarrow> |
|
255 (\<forall>x \<in> s. f differentiable at x) \<and> continuous_on s (\<lambda>x. vector_derivative f (at x))" |
|
256 unfolding C1_differentiable_on_def |
|
257 apply safe |
|
258 using differentiable_def has_vector_derivative_def apply blast |
|
259 apply (erule continuous_on_eq) |
|
260 using vector_derivative_at apply fastforce |
|
261 using vector_derivative_works apply fastforce |
|
262 done |
|
263 |
|
264 lemma C1_differentiable_on_subset: |
|
265 "f C1_differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f C1_differentiable_on s" |
|
266 unfolding C1_differentiable_on_def continuous_on_eq_continuous_within |
|
267 by (blast intro: continuous_within_subset) |
|
268 |
|
269 lemma C1_differentiable_compose: |
|
270 "\<lbrakk>f C1_differentiable_on s; g C1_differentiable_on (f ` s); |
|
271 \<And>x. finite (s \<inter> f-`{x})\<rbrakk> |
|
272 \<Longrightarrow> (g o f) C1_differentiable_on s" |
|
273 apply (simp add: C1_differentiable_on_eq, safe) |
|
274 using differentiable_chain_at apply blast |
|
275 apply (rule continuous_on_eq [of _ "\<lambda>x. vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"]) |
|
276 apply (rule Limits.continuous_on_scaleR, assumption) |
|
277 apply (metis (mono_tags, lifting) continuous_on_eq continuous_at_imp_continuous_on continuous_on_compose differentiable_imp_continuous_within o_def) |
|
278 by (simp add: vector_derivative_chain_at) |
|
279 |
|
280 lemma C1_diff_imp_diff: "f C1_differentiable_on s \<Longrightarrow> f differentiable_on s" |
|
281 by (simp add: C1_differentiable_on_eq differentiable_at_imp_differentiable_on) |
|
282 |
|
283 lemma C1_differentiable_on_ident [simp, derivative_intros]: "(\<lambda>x. x) C1_differentiable_on s" |
|
284 by (auto simp: C1_differentiable_on_eq continuous_on_const) |
|
285 |
|
286 lemma C1_differentiable_on_const [simp, derivative_intros]: "(\<lambda>z. a) C1_differentiable_on s" |
|
287 by (auto simp: C1_differentiable_on_eq continuous_on_const) |
|
288 |
|
289 lemma C1_differentiable_on_add [simp, derivative_intros]: |
|
290 "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x + g x) C1_differentiable_on s" |
|
291 unfolding C1_differentiable_on_eq by (auto intro: continuous_intros) |
|
292 |
|
293 lemma C1_differentiable_on_minus [simp, derivative_intros]: |
|
294 "f C1_differentiable_on s \<Longrightarrow> (\<lambda>x. - f x) C1_differentiable_on s" |
|
295 unfolding C1_differentiable_on_eq by (auto intro: continuous_intros) |
|
296 |
|
297 lemma C1_differentiable_on_diff [simp, derivative_intros]: |
|
298 "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x - g x) C1_differentiable_on s" |
|
299 unfolding C1_differentiable_on_eq by (auto intro: continuous_intros) |
|
300 |
|
301 lemma C1_differentiable_on_mult [simp, derivative_intros]: |
|
302 fixes f g :: "real \<Rightarrow> 'a :: real_normed_algebra" |
|
303 shows "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x * g x) C1_differentiable_on s" |
|
304 unfolding C1_differentiable_on_eq |
|
305 by (auto simp: continuous_on_add continuous_on_mult continuous_at_imp_continuous_on differentiable_imp_continuous_within) |
|
306 |
|
307 lemma C1_differentiable_on_scaleR [simp, derivative_intros]: |
|
308 "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) C1_differentiable_on s" |
|
309 unfolding C1_differentiable_on_eq |
|
310 by (rule continuous_intros | simp add: continuous_at_imp_continuous_on differentiable_imp_continuous_within)+ |
|
311 |
|
312 |
|
313 definition piecewise_C1_differentiable_on |
|
314 (infixr "piecewise'_C1'_differentiable'_on" 50) |
|
315 where "f piecewise_C1_differentiable_on i \<equiv> |
|
316 continuous_on i f \<and> |
|
317 (\<exists>s. finite s \<and> (f C1_differentiable_on (i - s)))" |
|
318 |
|
319 lemma C1_differentiable_imp_piecewise: |
|
320 "f C1_differentiable_on s \<Longrightarrow> f piecewise_C1_differentiable_on s" |
|
321 by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_at_imp_continuous_on differentiable_imp_continuous_within) |
|
322 |
|
323 lemma piecewise_C1_imp_differentiable: |
|
324 "f piecewise_C1_differentiable_on i \<Longrightarrow> f piecewise_differentiable_on i" |
|
325 by (auto simp: piecewise_C1_differentiable_on_def piecewise_differentiable_on_def |
|
326 C1_differentiable_on_def differentiable_def has_vector_derivative_def |
|
327 intro: has_derivative_at_within) |
|
328 |
|
329 lemma piecewise_C1_differentiable_compose: |
|
330 "\<lbrakk>f piecewise_C1_differentiable_on s; g piecewise_C1_differentiable_on (f ` s); |
|
331 \<And>x. finite (s \<inter> f-`{x})\<rbrakk> |
|
332 \<Longrightarrow> (g o f) piecewise_C1_differentiable_on s" |
|
333 apply (simp add: piecewise_C1_differentiable_on_def, safe) |
|
334 apply (blast intro: continuous_on_compose2) |
|
335 apply (rename_tac A B) |
|
336 apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f-`{x})" in exI) |
|
337 apply (rule conjI, blast) |
|
338 apply (rule C1_differentiable_compose) |
|
339 apply (blast intro: C1_differentiable_on_subset) |
|
340 apply (blast intro: C1_differentiable_on_subset) |
|
341 by (simp add: Diff_Int_distrib2) |
|
342 |
|
343 lemma piecewise_C1_differentiable_on_subset: |
|
344 "f piecewise_C1_differentiable_on s \<Longrightarrow> t \<le> s \<Longrightarrow> f piecewise_C1_differentiable_on t" |
|
345 by (auto simp: piecewise_C1_differentiable_on_def elim!: continuous_on_subset C1_differentiable_on_subset) |
|
346 |
|
347 lemma C1_differentiable_imp_continuous_on: |
|
348 "f C1_differentiable_on s \<Longrightarrow> continuous_on s f" |
|
349 unfolding C1_differentiable_on_eq continuous_on_eq_continuous_within |
|
350 using differentiable_at_withinI differentiable_imp_continuous_within by blast |
|
351 |
|
352 lemma C1_differentiable_on_empty [iff]: "f C1_differentiable_on {}" |
|
353 unfolding C1_differentiable_on_def |
|
354 by auto |
|
355 |
|
356 lemma piecewise_C1_differentiable_affine: |
|
357 fixes m::real |
|
358 assumes "f piecewise_C1_differentiable_on ((\<lambda>x. m * x + c) ` s)" |
|
359 shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_C1_differentiable_on s" |
|
360 proof (cases "m = 0") |
|
361 case True |
|
362 then show ?thesis |
|
363 unfolding o_def by (auto simp: piecewise_C1_differentiable_on_def continuous_on_const) |
|
364 next |
|
365 case False |
|
366 show ?thesis |
|
367 apply (rule piecewise_C1_differentiable_compose [OF C1_differentiable_imp_piecewise]) |
|
368 apply (rule assms derivative_intros | simp add: False vimage_def)+ |
|
369 using real_vector_affinity_eq [OF False, where c=c, unfolded scaleR_conv_of_real] |
|
370 apply simp |
|
371 done |
|
372 qed |
|
373 |
|
374 lemma piecewise_C1_differentiable_cases: |
|
375 fixes c::real |
|
376 assumes "f piecewise_C1_differentiable_on {a..c}" |
|
377 "g piecewise_C1_differentiable_on {c..b}" |
|
378 "a \<le> c" "c \<le> b" "f c = g c" |
|
379 shows "(\<lambda>x. if x \<le> c then f x else g x) piecewise_C1_differentiable_on {a..b}" |
|
380 proof - |
|
381 obtain s t where st: "f C1_differentiable_on ({a..c} - s)" |
|
382 "g C1_differentiable_on ({c..b} - t)" |
|
383 "finite s" "finite t" |
|
384 using assms |
|
385 by (force simp: piecewise_C1_differentiable_on_def) |
|
386 then have f_diff: "f differentiable_on {a..<c} - s" |
|
387 and g_diff: "g differentiable_on {c<..b} - t" |
|
388 by (simp_all add: C1_differentiable_on_eq differentiable_at_withinI differentiable_on_def) |
|
389 have "continuous_on {a..c} f" "continuous_on {c..b} g" |
|
390 using assms piecewise_C1_differentiable_on_def by auto |
|
391 then have cab: "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)" |
|
392 using continuous_on_cases [OF closed_real_atLeastAtMost [of a c], |
|
393 OF closed_real_atLeastAtMost [of c b], |
|
394 of f g "\<lambda>x. x\<le>c"] assms |
|
395 by (force simp: ivl_disj_un_two_touch) |
|
396 { fix x |
|
85 assume x: "x \<in> {a..b} - insert c (s \<union> t)" |
397 assume x: "x \<in> {a..b} - insert c (s \<union> t)" |
86 have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x" (is "?diff_fg") |
398 have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x" (is "?diff_fg") |
87 proof (cases x c rule: le_cases) |
399 proof (cases x c rule: le_cases) |
88 case le show ?diff_fg |
400 case le show ?diff_fg |
89 apply (rule differentiable_transform_at [of "dist x c" _ f]) |
401 apply (rule differentiable_transform_at [of "dist x c" _ f]) |
90 using dist_nz x dist_real_def le st x |
402 using x dist_real_def le st by (auto simp: C1_differentiable_on_eq) |
91 apply auto |
|
92 done |
|
93 next |
403 next |
94 case ge show ?diff_fg |
404 case ge show ?diff_fg |
95 apply (rule differentiable_transform_at [of "dist x c" _ g]) |
405 apply (rule differentiable_transform_at [of "dist x c" _ g]) |
96 using dist_nz x dist_real_def ge st x |
406 using dist_nz x dist_real_def ge st x by (auto simp: C1_differentiable_on_eq) |
97 apply auto |
|
98 done |
|
99 qed |
407 qed |
100 } |
408 } |
101 then have "\<exists>s. finite s \<and> (\<forall>x\<in>{a..b} - s. (\<lambda>x. if x \<le> c then f x else g x) differentiable at x)" |
409 then have "(\<forall>x \<in> {a..b} - insert c (s \<union> t). (\<lambda>x. if x \<le> c then f x else g x) differentiable at x)" |
410 by auto |
|
411 moreover |
|
412 { assume fcon: "continuous_on ({a<..<c} - s) (\<lambda>x. vector_derivative f (at x))" |
|
413 and gcon: "continuous_on ({c<..<b} - t) (\<lambda>x. vector_derivative g (at x))" |
|
414 have "open ({a<..<c} - s)" "open ({c<..<b} - t)" |
|
415 using st by (simp_all add: open_Diff finite_imp_closed) |
|
416 moreover have "continuous_on ({a<..<c} - s) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))" |
|
417 apply (rule continuous_on_eq [OF fcon]) |
|
418 apply (simp add:) |
|
419 apply (rule vector_derivative_at [symmetric]) |
|
420 apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_at) |
|
421 apply (simp_all add: dist_norm vector_derivative_works [symmetric]) |
|
422 using f_diff |
|
423 by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_imp_le st(1)) |
|
424 moreover have "continuous_on ({c<..<b} - t) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))" |
|
425 apply (rule continuous_on_eq [OF gcon]) |
|
426 apply (simp add:) |
|
427 apply (rule vector_derivative_at [symmetric]) |
|
428 apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_at) |
|
429 apply (simp_all add: dist_norm vector_derivative_works [symmetric]) |
|
430 using g_diff |
|
431 by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_imp_le st(2)) |
|
432 ultimately have "continuous_on ({a<..<b} - insert c (s \<union> t)) |
|
433 (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))" |
|
434 apply (rule continuous_on_subset [OF continuous_on_open_Un], auto) |
|
435 done |
|
436 } note * = this |
|
437 have "continuous_on ({a<..<b} - insert c (s \<union> t)) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))" |
|
102 using st |
438 using st |
103 by (metis (full_types) finite_Un finite_insert) |
439 by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset intro: *) |
440 ultimately have "\<exists>s. finite s \<and> ((\<lambda>x. if x \<le> c then f x else g x) C1_differentiable_on {a..b} - s)" |
|
441 apply (rule_tac x="{a,b,c} \<union> s \<union> t" in exI) |
|
442 using st by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset) |
|
443 with cab show ?thesis |
|
444 by (simp add: piecewise_C1_differentiable_on_def) |
|
445 qed |
|
446 |
|
447 lemma piecewise_C1_differentiable_neg: |
|
448 "f piecewise_C1_differentiable_on s \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_C1_differentiable_on s" |
|
449 unfolding piecewise_C1_differentiable_on_def |
|
450 by (auto intro!: continuous_on_minus C1_differentiable_on_minus) |
|
451 |
|
452 lemma piecewise_C1_differentiable_add: |
|
453 assumes "f piecewise_C1_differentiable_on i" |
|
454 "g piecewise_C1_differentiable_on i" |
|
455 shows "(\<lambda>x. f x + g x) piecewise_C1_differentiable_on i" |
|
456 proof - |
|
457 obtain s t where st: "finite s" "finite t" |
|
458 "f C1_differentiable_on (i-s)" |
|
459 "g C1_differentiable_on (i-t)" |
|
460 using assms by (auto simp: piecewise_C1_differentiable_on_def) |
|
461 then have "finite (s \<union> t) \<and> (\<lambda>x. f x + g x) C1_differentiable_on i - (s \<union> t)" |
|
462 by (auto intro: C1_differentiable_on_add elim!: C1_differentiable_on_subset) |
|
463 moreover have "continuous_on i f" "continuous_on i g" |
|
464 using assms piecewise_C1_differentiable_on_def by auto |
|
104 ultimately show ?thesis |
465 ultimately show ?thesis |
105 by (simp add: piecewise_differentiable_on_def) |
466 by (auto simp: piecewise_C1_differentiable_on_def continuous_on_add) |
106 qed |
467 qed |
107 |
468 |
108 lemma piecewise_differentiable_neg: |
469 lemma piecewise_C1_differentiable_C1_diff: |
109 "f piecewise_differentiable_on s \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_differentiable_on s" |
470 "\<lbrakk>f piecewise_C1_differentiable_on s; g piecewise_C1_differentiable_on s\<rbrakk> |
110 by (auto simp: piecewise_differentiable_on_def continuous_on_minus) |
471 \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_C1_differentiable_on s" |
111 |
|
112 lemma piecewise_differentiable_add: |
|
113 assumes "f piecewise_differentiable_on i" |
|
114 "g piecewise_differentiable_on i" |
|
115 shows "(\<lambda>x. f x + g x) piecewise_differentiable_on i" |
|
116 proof - |
|
117 obtain s t where st: "finite s" "finite t" |
|
118 "\<forall>x\<in>i - s. f differentiable at x" |
|
119 "\<forall>x\<in>i - t. g differentiable at x" |
|
120 using assms by (auto simp: piecewise_differentiable_on_def) |
|
121 then have "finite (s \<union> t) \<and> (\<forall>x\<in>i - (s \<union> t). (\<lambda>x. f x + g x) differentiable at x)" |
|
122 by auto |
|
123 moreover have "continuous_on i f" "continuous_on i g" |
|
124 using assms piecewise_differentiable_on_def by auto |
|
125 ultimately show ?thesis |
|
126 by (auto simp: piecewise_differentiable_on_def continuous_on_add) |
|
127 qed |
|
128 |
|
129 lemma piecewise_differentiable_diff: |
|
130 "\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on s\<rbrakk> |
|
131 \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_differentiable_on s" |
|
132 unfolding diff_conv_add_uminus |
472 unfolding diff_conv_add_uminus |
133 by (metis piecewise_differentiable_add piecewise_differentiable_neg) |
473 by (metis piecewise_C1_differentiable_add piecewise_C1_differentiable_neg) |
134 |
474 |
475 lemma piecewise_C1_differentiable_D1: |
|
476 fixes g1 :: "real \<Rightarrow> 'a::real_normed_field" |
|
477 assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" |
|
478 shows "g1 piecewise_C1_differentiable_on {0..1}" |
|
479 proof - |
|
480 obtain s where "finite s" |
|
481 and co12: "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))" |
|
482 and g12D: "\<forall>x\<in>{0..1} - s. g1 +++ g2 differentiable at x" |
|
483 using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) |
|
484 then have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (op * 2 ` s)" for x |
|
485 apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_at) |
|
486 using that |
|
487 apply (simp_all add: dist_real_def joinpaths_def) |
|
488 apply (rule differentiable_chain_at derivative_intros | force)+ |
|
489 done |
|
490 have [simp]: "vector_derivative (g1 \<circ> op * 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)" |
|
491 if "x \<in> {0..1} - insert 1 (op * 2 ` s)" for x |
|
492 apply (subst vector_derivative_chain_at) |
|
493 using that |
|
494 apply (rule derivative_eq_intros g1D | simp)+ |
|
495 done |
|
496 have "continuous_on ({0..1/2} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))" |
|
497 using co12 by (rule continuous_on_subset) force |
|
498 then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 o op*2) (at x))" |
|
499 apply (rule continuous_on_eq [OF _ vector_derivative_at]) |
|
500 apply (rule_tac f="g1 o op*2" and d="dist x (1/2)" in has_vector_derivative_transform_at) |
|
501 apply (simp_all add: dist_norm joinpaths_def vector_derivative_works [symmetric]) |
|
502 apply (force intro: g1D differentiable_chain_at) |
|
503 done |
|
504 have "continuous_on ({0..1} - insert 1 (op * 2 ` s)) |
|
505 ((\<lambda>x. 1/2 * vector_derivative (g1 o op*2) (at x)) o op*(1/2))" |
|
506 apply (rule continuous_intros)+ |
|
507 using coDhalf |
|
508 apply (simp add: scaleR_conv_of_real image_set_diff image_image) |
|
509 done |
|
510 then have con_g1: "continuous_on ({0..1} - insert 1 (op * 2 ` s)) (\<lambda>x. vector_derivative g1 (at x))" |
|
511 by (rule continuous_on_eq) (simp add: scaleR_conv_of_real) |
|
512 have "continuous_on {0..1} g1" |
|
513 using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast |
|
514 with `finite s` show ?thesis |
|
515 apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) |
|
516 apply (rule_tac x="insert 1 ((op*2)`s)" in exI) |
|
517 apply (simp add: g1D con_g1) |
|
518 done |
|
519 qed |
|
520 |
|
521 lemma piecewise_C1_differentiable_D2: |
|
522 fixes g2 :: "real \<Rightarrow> 'a::real_normed_field" |
|
523 assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" "pathfinish g1 = pathstart g2" |
|
524 shows "g2 piecewise_C1_differentiable_on {0..1}" |
|
525 proof - |
|
526 obtain s where "finite s" |
|
527 and co12: "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))" |
|
528 and g12D: "\<forall>x\<in>{0..1} - s. g1 +++ g2 differentiable at x" |
|
529 using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) |
|
530 then have g2D: "g2 differentiable at x" if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)" for x |
|
531 apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_at) |
|
532 using that |
|
533 apply (simp_all add: dist_real_def joinpaths_def) |
|
534 apply (auto simp: dist_real_def joinpaths_def field_simps) |
|
535 apply (rule differentiable_chain_at derivative_intros | force)+ |
|
536 apply (drule_tac x= "(x + 1) / 2" in bspec, force simp: divide_simps) |
|
537 apply assumption |
|
538 done |
|
539 have [simp]: "vector_derivative (g2 \<circ> (\<lambda>x. 2*x-1)) (at ((x+1)/2)) = 2 *\<^sub>R vector_derivative g2 (at x)" |
|
540 if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)" for x |
|
541 using that by (auto simp: vector_derivative_chain_at divide_simps g2D) |
|
542 have "continuous_on ({1/2..1} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))" |
|
543 using co12 by (rule continuous_on_subset) force |
|
544 then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) s) (\<lambda>x. vector_derivative (g2 o (\<lambda>x. 2*x-1)) (at x))" |
|
545 apply (rule continuous_on_eq [OF _ vector_derivative_at]) |
|
546 apply (rule_tac f="g2 o (\<lambda>x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_at) |
|
547 apply (auto simp: dist_real_def field_simps joinpaths_def vector_derivative_works [symmetric] |
|
548 intro!: g2D differentiable_chain_at) |
|
549 done |
|
550 have [simp]: "((\<lambda>x. (x + 1) / 2) ` ({0..1} - insert 0 ((\<lambda>x. 2 * x - 1) ` s))) = ({1/2..1} - insert (1/2) s)" |
|
551 apply (simp add: image_set_diff inj_on_def image_image) |
|
552 apply (auto simp: image_affinity_atLeastAtMost_div add_divide_distrib) |
|
553 done |
|
554 have "continuous_on ({0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)) |
|
555 ((\<lambda>x. 1/2 * vector_derivative (g2 \<circ> (\<lambda>x. 2*x-1)) (at x)) o (\<lambda>x. (x+1)/2))" |
|
556 by (rule continuous_intros | simp add: coDhalf)+ |
|
557 then have con_g2: "continuous_on ({0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)) (\<lambda>x. vector_derivative g2 (at x))" |
|
558 by (rule continuous_on_eq) (simp add: scaleR_conv_of_real) |
|
559 have "continuous_on {0..1} g2" |
|
560 using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast |
|
561 with `finite s` show ?thesis |
|
562 apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) |
|
563 apply (rule_tac x="insert 0 ((\<lambda>x. 2 * x - 1) ` s)" in exI) |
|
564 apply (simp add: g2D con_g2) |
|
565 done |
|
566 qed |
|
135 |
567 |
136 subsection \<open>Valid paths, and their start and finish\<close> |
568 subsection \<open>Valid paths, and their start and finish\<close> |
137 |
569 |
138 lemma Diff_Un_eq: "A - (B \<union> C) = A - B - C" |
570 lemma Diff_Un_eq: "A - (B \<union> C) = A - B - C" |
139 by blast |
571 by blast |
140 |
572 |
141 definition valid_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" |
573 definition valid_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" |
142 where "valid_path f \<equiv> f piecewise_differentiable_on {0..1::real}" |
574 where "valid_path f \<equiv> f piecewise_C1_differentiable_on {0..1::real}" |
143 |
575 |
144 definition closed_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" |
576 definition closed_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" |
145 where "closed_path g \<equiv> g 0 = g 1" |
577 where "closed_path g \<equiv> g 0 = g 1" |
146 |
578 |
147 lemma valid_path_compose: |
|
148 assumes "valid_path g" "f differentiable_on (path_image g)" |
|
149 shows "valid_path (f o g)" |
|
150 proof - |
|
151 { fix s :: "real set" |
|
152 assume df: "f differentiable_on g ` {0..1}" |
|
153 and cg: "continuous_on {0..1} g" |
|
154 and s: "finite s" |
|
155 and dg: "\<And>x. x\<in>{0..1} - s \<Longrightarrow> g differentiable at x" |
|
156 have dfo: "f differentiable_on g ` {0<..<1}" |
|
157 by (auto intro: differentiable_on_subset [OF df]) |
|
158 have *: "\<And>x. x \<in> {0<..<1} \<Longrightarrow> x \<notin> s \<Longrightarrow> (f o g) differentiable (at x within ({0<..<1} - s))" |
|
159 apply (rule differentiable_chain_within) |
|
160 apply (simp_all add: dg differentiable_at_withinI differentiable_chain_within) |
|
161 using df |
|
162 apply (force simp: differentiable_on_def elim: Deriv.differentiable_subset) |
|
163 done |
|
164 have oo: "open ({0<..<1} - s)" |
|
165 by (simp add: finite_imp_closed open_Diff s) |
|
166 have "\<exists>s. finite s \<and> (\<forall>x\<in>{0..1} - s. f \<circ> g differentiable at x)" |
|
167 apply (rule_tac x="{0,1} Un s" in exI) |
|
168 apply (simp add: Diff_Un_eq atLeastAtMost_diff_ends s del: Set.Un_insert_left, clarify) |
|
169 apply (rule differentiable_within_open [OF _ oo, THEN iffD1]) |
|
170 apply (auto simp: *) |
|
171 done } |
|
172 with assms show ?thesis |
|
173 by (clarsimp simp: valid_path_def piecewise_differentiable_on_def continuous_on_compose |
|
174 differentiable_imp_continuous_on path_image_def simp del: o_apply) |
|
175 qed |
|
176 |
|
177 |
|
178 subsubsection\<open>In particular, all results for paths apply\<close> |
579 subsubsection\<open>In particular, all results for paths apply\<close> |
179 |
580 |
180 lemma valid_path_imp_path: "valid_path g \<Longrightarrow> path g" |
581 lemma valid_path_imp_path: "valid_path g \<Longrightarrow> path g" |
181 by (simp add: path_def piecewise_differentiable_on_def valid_path_def) |
582 by (simp add: path_def piecewise_C1_differentiable_on_def valid_path_def) |
182 |
583 |
183 lemma connected_valid_path_image: "valid_path g \<Longrightarrow> connected(path_image g)" |
584 lemma connected_valid_path_image: "valid_path g \<Longrightarrow> connected(path_image g)" |
184 by (metis connected_path_image valid_path_imp_path) |
585 by (metis connected_path_image valid_path_imp_path) |
185 |
586 |
186 lemma compact_valid_path_image: "valid_path g \<Longrightarrow> compact(path_image g)" |
587 lemma compact_valid_path_image: "valid_path g \<Longrightarrow> compact(path_image g)" |
195 |
596 |
196 subsection\<open>Contour Integrals along a path\<close> |
597 subsection\<open>Contour Integrals along a path\<close> |
197 |
598 |
198 text\<open>This definition is for complex numbers only, and does not generalise to line integrals in a vector field\<close> |
599 text\<open>This definition is for complex numbers only, and does not generalise to line integrals in a vector field\<close> |
199 |
600 |
200 text\<open>= piecewise differentiable function on [0,1]\<close> |
601 text\<open>piecewise differentiable function on [0,1]\<close> |
201 |
602 |
202 definition has_path_integral :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool" |
603 definition has_path_integral :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool" |
203 (infixr "has'_path'_integral" 50) |
604 (infixr "has'_path'_integral" 50) |
204 where "(f has_path_integral i) g \<equiv> |
605 where "(f has_path_integral i) g \<equiv> |
205 ((\<lambda>x. f(g x) * vector_derivative g (at x within {0..1})) |
606 ((\<lambda>x. f(g x) * vector_derivative g (at x within {0..1})) |
267 |
668 |
268 lemma valid_path_imp_reverse: |
669 lemma valid_path_imp_reverse: |
269 assumes "valid_path g" |
670 assumes "valid_path g" |
270 shows "valid_path(reversepath g)" |
671 shows "valid_path(reversepath g)" |
271 proof - |
672 proof - |
272 obtain s where "finite s" "\<forall>x\<in>{0..1} - s. g differentiable at x" |
673 obtain s where "finite s" "g C1_differentiable_on ({0..1} - s)" |
273 using assms by (auto simp: valid_path_def piecewise_differentiable_on_def) |
674 using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def) |
274 then have "finite (op - 1 ` s)" "(\<forall>x\<in>{0..1} - op - 1 ` s. reversepath g differentiable at x)" |
675 then have "finite (op - 1 ` s)" "(reversepath g C1_differentiable_on ({0..1} - op - 1 ` s))" |
275 apply (auto simp: reversepath_def) |
676 apply (auto simp: reversepath_def) |
276 apply (rule differentiable_chain_at [of "\<lambda>x::real. 1-x" _ g, unfolded o_def]) |
677 apply (rule C1_differentiable_compose [of "\<lambda>x::real. 1-x" _ g, unfolded o_def]) |
277 using image_iff |
678 apply (auto simp: C1_differentiable_on_eq) |
278 apply fastforce+ |
679 apply (rule continuous_intros, force) |
680 apply (force elim!: continuous_on_subset) |
|
681 apply (simp add: finite_vimageI inj_on_def) |
|
279 done |
682 done |
280 then show ?thesis using assms |
683 then show ?thesis using assms |
281 by (auto simp: valid_path_def piecewise_differentiable_on_def path_def [symmetric]) |
684 by (auto simp: valid_path_def piecewise_C1_differentiable_on_def path_def [symmetric]) |
282 qed |
685 qed |
283 |
686 |
284 lemma valid_path_reversepath: "valid_path(reversepath g) \<longleftrightarrow> valid_path g" |
687 lemma valid_path_reversepath: "valid_path(reversepath g) \<longleftrightarrow> valid_path g" |
285 using valid_path_imp_reverse by force |
688 using valid_path_imp_reverse by force |
286 |
689 |
287 lemma has_path_integral_reversepath: |
690 lemma has_path_integral_reversepath: |
288 assumes "valid_path g" "(f has_path_integral i) g" |
691 assumes "valid_path g" "(f has_path_integral i) g" |
289 shows "(f has_path_integral (-i)) (reversepath g)" |
692 shows "(f has_path_integral (-i)) (reversepath g)" |
290 proof - |
693 proof - |
291 { fix s x |
694 { fix s x |
292 assume xs: "\<forall>x\<in>{0..1} - s. g differentiable at x" "x \<notin> op - 1 ` s" "0 \<le> x" "x \<le> 1" |
695 assume xs: "g C1_differentiable_on ({0..1} - s)" "x \<notin> op - 1 ` s" "0 \<le> x" "x \<le> 1" |
293 have "vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) = |
696 have "vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) = |
294 - vector_derivative g (at (1 - x) within {0..1})" |
697 - vector_derivative g (at (1 - x) within {0..1})" |
295 proof - |
698 proof - |
296 obtain f' where f': "(g has_vector_derivative f') (at (1 - x))" |
699 obtain f' where f': "(g has_vector_derivative f') (at (1 - x))" |
297 using xs |
700 using xs |
298 apply (drule_tac x="1-x" in bspec) |
701 by (force simp: has_vector_derivative_def C1_differentiable_on_def) |
299 apply (simp_all add: has_vector_derivative_def differentiable_def, force) |
|
300 apply (blast elim!: linear_imp_scaleR dest: has_derivative_linear) |
|
301 done |
|
302 have "(g o (\<lambda>x. 1 - x) has_vector_derivative -1 *\<^sub>R f') (at x)" |
702 have "(g o (\<lambda>x. 1 - x) has_vector_derivative -1 *\<^sub>R f') (at x)" |
303 apply (rule vector_diff_chain_within) |
703 apply (rule vector_diff_chain_within) |
304 apply (intro vector_diff_chain_within derivative_eq_intros | simp)+ |
704 apply (intro vector_diff_chain_within derivative_eq_intros | simp)+ |
305 apply (rule has_vector_derivative_at_within [OF f']) |
705 apply (rule has_vector_derivative_at_within [OF f']) |
306 done |
706 done |
314 have 01: "{0..1::real} = cbox 0 1" |
714 have 01: "{0..1::real} = cbox 0 1" |
315 by simp |
715 by simp |
316 show ?thesis using assms |
716 show ?thesis using assms |
317 apply (auto simp: has_path_integral_def) |
717 apply (auto simp: has_path_integral_def) |
318 apply (drule has_integral_affinity01 [where m= "-1" and c=1]) |
718 apply (drule has_integral_affinity01 [where m= "-1" and c=1]) |
319 apply (auto simp: reversepath_def valid_path_def piecewise_differentiable_on_def) |
719 apply (auto simp: reversepath_def valid_path_def piecewise_C1_differentiable_on_def) |
320 apply (drule has_integral_neg) |
720 apply (drule has_integral_neg) |
321 apply (rule_tac s = "(\<lambda>x. 1 - x) ` s" in has_integral_spike_finite) |
721 apply (rule_tac s = "(\<lambda>x. 1 - x) ` s" in has_integral_spike_finite) |
322 apply (auto simp: *) |
722 apply (auto simp: *) |
323 done |
723 done |
324 qed |
724 qed |
342 assumes "valid_path g1" "valid_path g2" "pathfinish g1 = pathstart g2" |
742 assumes "valid_path g1" "valid_path g2" "pathfinish g1 = pathstart g2" |
343 shows "valid_path(g1 +++ g2)" |
743 shows "valid_path(g1 +++ g2)" |
344 proof - |
744 proof - |
345 have "g1 1 = g2 0" |
745 have "g1 1 = g2 0" |
346 using assms by (auto simp: pathfinish_def pathstart_def) |
746 using assms by (auto simp: pathfinish_def pathstart_def) |
347 moreover have "(g1 o (\<lambda>x. 2*x)) piecewise_differentiable_on {0..1/2}" |
747 moreover have "(g1 o (\<lambda>x. 2*x)) piecewise_C1_differentiable_on {0..1/2}" |
348 apply (rule piecewise_differentiable_compose) |
748 apply (rule piecewise_C1_differentiable_compose) |
349 using assms |
749 using assms |
350 apply (auto simp: valid_path_def piecewise_differentiable_on_def continuous_on_joinpaths) |
750 apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths) |
351 apply (rule continuous_intros | simp)+ |
751 apply (rule continuous_intros | simp)+ |
352 apply (force intro: finite_vimageI [where h = "op*2"] inj_onI) |
752 apply (force intro: finite_vimageI [where h = "op*2"] inj_onI) |
353 done |
753 done |
354 moreover have "(g2 o (\<lambda>x. 2*x-1)) piecewise_differentiable_on {1/2..1}" |
754 moreover have "(g2 o (\<lambda>x. 2*x-1)) piecewise_C1_differentiable_on {1/2..1}" |
355 apply (rule piecewise_differentiable_compose) |
755 apply (rule piecewise_C1_differentiable_compose) |
356 using assms |
756 using assms unfolding valid_path_def piecewise_C1_differentiable_on_def |
357 apply (auto simp: valid_path_def piecewise_differentiable_on_def continuous_on_joinpaths) |
757 by (auto intro!: continuous_intros finite_vimageI [where h = "(\<lambda>x. 2*x - 1)"] inj_onI |
358 apply (rule continuous_intros | simp add: image_affinity_atLeastAtMost_diff)+ |
758 simp: image_affinity_atLeastAtMost_diff continuous_on_joinpaths) |
359 apply (force intro: finite_vimageI [where h = "(\<lambda>x. 2*x - 1)"] inj_onI) |
|
360 done |
|
361 ultimately show ?thesis |
759 ultimately show ?thesis |
362 apply (simp only: valid_path_def continuous_on_joinpaths joinpaths_def) |
760 apply (simp only: valid_path_def continuous_on_joinpaths joinpaths_def) |
363 apply (rule piecewise_differentiable_cases) |
761 apply (rule piecewise_C1_differentiable_cases) |
364 apply (auto simp: o_def) |
762 apply (auto simp: o_def) |
365 done |
763 done |
366 qed |
764 qed |
367 |
765 |
368 lemma continuous_on_joinpaths_D1: |
766 lemma valid_path_join_D1: |
369 "continuous_on {0..1} (g1 +++ g2) \<Longrightarrow> continuous_on {0..1} g1" |
767 fixes g1 :: "real \<Rightarrow> 'a::real_normed_field" |
370 apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (op*(inverse 2))"]) |
768 shows "valid_path (g1 +++ g2) \<Longrightarrow> valid_path g1" |
371 apply (simp add: joinpaths_def) |
769 unfolding valid_path_def |
372 apply (rule continuous_intros | simp)+ |
770 by (rule piecewise_C1_differentiable_D1) |
373 apply (auto elim!: continuous_on_subset) |
771 |
374 done |
772 lemma valid_path_join_D2: |
375 |
773 fixes g2 :: "real \<Rightarrow> 'a::real_normed_field" |
376 lemma continuous_on_joinpaths_D2: |
774 shows "\<lbrakk>valid_path (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> valid_path g2" |
377 "\<lbrakk>continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> continuous_on {0..1} g2" |
775 unfolding valid_path_def |
378 apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (\<lambda>x. inverse 2*x + 1/2)"]) |
776 by (rule piecewise_C1_differentiable_D2) |
379 apply (simp add: joinpaths_def pathfinish_def pathstart_def Ball_def) |
|
380 apply (rule continuous_intros | simp)+ |
|
381 apply (auto elim!: continuous_on_subset) |
|
382 done |
|
383 |
|
384 lemma piecewise_differentiable_D1: |
|
385 "(g1 +++ g2) piecewise_differentiable_on {0..1} \<Longrightarrow> g1 piecewise_differentiable_on {0..1}" |
|
386 apply (clarsimp simp add: piecewise_differentiable_on_def continuous_on_joinpaths_D1) |
|
387 apply (rule_tac x="insert 1 ((op*2)`s)" in exI) |
|
388 apply simp |
|
389 apply (intro ballI) |
|
390 apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_at) |
|
391 apply (auto simp: dist_real_def joinpaths_def) |
|
392 apply (rule differentiable_chain_at derivative_intros | force)+ |
|
393 done |
|
394 |
|
395 lemma piecewise_differentiable_D2: |
|
396 "\<lbrakk>(g1 +++ g2) piecewise_differentiable_on {0..1}; pathfinish g1 = pathstart g2\<rbrakk> |
|
397 \<Longrightarrow> g2 piecewise_differentiable_on {0..1}" |
|
398 apply (clarsimp simp add: piecewise_differentiable_on_def continuous_on_joinpaths_D2) |
|
399 apply (rule_tac x="insert 0 ((\<lambda>x. 2*x-1)`s)" in exI) |
|
400 apply simp |
|
401 apply (intro ballI) |
|
402 apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_at) |
|
403 apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: split_if_asm) |
|
404 apply (rule differentiable_chain_at derivative_intros | force simp: divide_simps)+ |
|
405 done |
|
406 |
|
407 lemma valid_path_join_D1: "valid_path (g1 +++ g2) \<Longrightarrow> valid_path g1" |
|
408 by (simp add: valid_path_def piecewise_differentiable_D1) |
|
409 |
|
410 lemma valid_path_join_D2: "\<lbrakk>valid_path (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> valid_path g2" |
|
411 by (simp add: valid_path_def piecewise_differentiable_D2) |
|
412 |
777 |
413 lemma valid_path_join_eq [simp]: |
778 lemma valid_path_join_eq [simp]: |
414 "pathfinish g1 = pathstart g2 \<Longrightarrow> (valid_path(g1 +++ g2) \<longleftrightarrow> valid_path g1 \<and> valid_path g2)" |
779 fixes g2 :: "real \<Rightarrow> 'a::real_normed_field" |
780 shows "pathfinish g1 = pathstart g2 \<Longrightarrow> (valid_path(g1 +++ g2) \<longleftrightarrow> valid_path g1 \<and> valid_path g2)" |
|
415 using valid_path_join_D1 valid_path_join_D2 valid_path_join by blast |
781 using valid_path_join_D1 valid_path_join_D2 valid_path_join by blast |
416 |
782 |
417 lemma has_path_integral_join: |
783 lemma has_path_integral_join: |
418 assumes "(f has_path_integral i1) g1" "(f has_path_integral i2) g2" |
784 assumes "(f has_path_integral i1) g1" "(f has_path_integral i2) g2" |
419 "valid_path g1" "valid_path g2" |
785 "valid_path g1" "valid_path g2" |
421 proof - |
787 proof - |
422 obtain s1 s2 |
788 obtain s1 s2 |
423 where s1: "finite s1" "\<forall>x\<in>{0..1} - s1. g1 differentiable at x" |
789 where s1: "finite s1" "\<forall>x\<in>{0..1} - s1. g1 differentiable at x" |
424 and s2: "finite s2" "\<forall>x\<in>{0..1} - s2. g2 differentiable at x" |
790 and s2: "finite s2" "\<forall>x\<in>{0..1} - s2. g2 differentiable at x" |
425 using assms |
791 using assms |
426 by (auto simp: valid_path_def piecewise_differentiable_on_def) |
792 by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) |
427 have 1: "((\<lambda>x. f (g1 x) * vector_derivative g1 (at x)) has_integral i1) {0..1}" |
793 have 1: "((\<lambda>x. f (g1 x) * vector_derivative g1 (at x)) has_integral i1) {0..1}" |
428 and 2: "((\<lambda>x. f (g2 x) * vector_derivative g2 (at x)) has_integral i2) {0..1}" |
794 and 2: "((\<lambda>x. f (g2 x) * vector_derivative g2 (at x)) has_integral i2) {0..1}" |
429 using assms |
795 using assms |
430 by (auto simp: has_path_integral) |
796 by (auto simp: has_path_integral) |
431 have i1: "((\<lambda>x. (2*f (g1 (2*x))) * vector_derivative g1 (at (2*x))) has_integral i1) {0..1/2}" |
797 have i1: "((\<lambda>x. (2*f (g1 (2*x))) * vector_derivative g1 (at (2*x))) has_integral i1) {0..1/2}" |
483 assumes "f path_integrable_on (g1 +++ g2)" "valid_path g1" |
849 assumes "f path_integrable_on (g1 +++ g2)" "valid_path g1" |
484 shows "f path_integrable_on g1" |
850 shows "f path_integrable_on g1" |
485 proof - |
851 proof - |
486 obtain s1 |
852 obtain s1 |
487 where s1: "finite s1" "\<forall>x\<in>{0..1} - s1. g1 differentiable at x" |
853 where s1: "finite s1" "\<forall>x\<in>{0..1} - s1. g1 differentiable at x" |
488 using assms by (auto simp: valid_path_def piecewise_differentiable_on_def) |
854 using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) |
489 have "(\<lambda>x. f ((g1 +++ g2) (x/2)) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}" |
855 have "(\<lambda>x. f ((g1 +++ g2) (x/2)) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}" |
490 using assms |
856 using assms |
491 apply (auto simp: path_integrable_on) |
857 apply (auto simp: path_integrable_on) |
492 apply (drule integrable_on_subcbox [where a=0 and b="1/2"]) |
858 apply (drule integrable_on_subcbox [where a=0 and b="1/2"]) |
493 apply (auto intro: integrable_affinity [of _ 0 "1/2::real" "1/2" 0, simplified]) |
859 apply (auto intro: integrable_affinity [of _ 0 "1/2::real" "1/2" 0, simplified]) |
494 done |
860 done |
495 then have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2))/2) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}" |
861 then have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2))/2) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}" |
496 by (force dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real) |
862 by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real) |
497 have g1: "\<lbrakk>0 < z; z < 1; z \<notin> s1\<rbrakk> \<Longrightarrow> |
863 have g1: "\<lbrakk>0 < z; z < 1; z \<notin> s1\<rbrakk> \<Longrightarrow> |
498 vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) = |
864 vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) = |
499 2 *\<^sub>R vector_derivative g1 (at z)" for z |
865 2 *\<^sub>R vector_derivative g1 (at z)" for z |
500 apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>(z-1)/2\<bar>" _ "(\<lambda>x. g1(2*x))"]]) |
866 apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>(z-1)/2\<bar>" _ "(\<lambda>x. g1(2*x))"]]) |
501 apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm) |
867 apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm) |
509 apply (rule integrable_spike_finite [of "{0,1} \<union> s1", OF _ _ *]) |
875 apply (rule integrable_spike_finite [of "{0,1} \<union> s1", OF _ _ *]) |
510 apply (auto simp: joinpaths_def scaleR_conv_of_real g1) |
876 apply (auto simp: joinpaths_def scaleR_conv_of_real g1) |
511 done |
877 done |
512 qed |
878 qed |
513 |
879 |
514 lemma path_integrable_joinD2: (*FIXME: could combine these proofs*) |
880 lemma path_integrable_joinD2: |
515 assumes "f path_integrable_on (g1 +++ g2)" "valid_path g2" |
881 assumes "f path_integrable_on (g1 +++ g2)" "valid_path g2" |
516 shows "f path_integrable_on g2" |
882 shows "f path_integrable_on g2" |
517 proof - |
883 proof - |
518 obtain s2 |
884 obtain s2 |
519 where s2: "finite s2" "\<forall>x\<in>{0..1} - s2. g2 differentiable at x" |
885 where s2: "finite s2" "\<forall>x\<in>{0..1} - s2. g2 differentiable at x" |
520 using assms by (auto simp: valid_path_def piecewise_differentiable_on_def) |
886 using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) |
521 have "(\<lambda>x. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}" |
887 have "(\<lambda>x. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}" |
522 using assms |
888 using assms |
523 apply (auto simp: path_integrable_on) |
889 apply (auto simp: path_integrable_on) |
524 apply (drule integrable_on_subcbox [where a="1/2" and b=1], auto) |
890 apply (drule integrable_on_subcbox [where a="1/2" and b=1], auto) |
525 apply (drule integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2", simplified]) |
891 apply (drule integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2", simplified]) |
567 lemma valid_path_shiftpath [intro]: |
933 lemma valid_path_shiftpath [intro]: |
568 assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}" |
934 assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}" |
569 shows "valid_path(shiftpath a g)" |
935 shows "valid_path(shiftpath a g)" |
570 using assms |
936 using assms |
571 apply (auto simp: valid_path_def shiftpath_alt_def) |
937 apply (auto simp: valid_path_def shiftpath_alt_def) |
572 apply (rule piecewise_differentiable_cases) |
938 apply (rule piecewise_C1_differentiable_cases) |
573 apply (auto simp: algebra_simps) |
939 apply (auto simp: algebra_simps) |
574 apply (rule piecewise_differentiable_affine [of g 1 a, simplified o_def scaleR_one]) |
940 apply (rule piecewise_C1_differentiable_affine [of g 1 a, simplified o_def scaleR_one]) |
575 apply (auto simp: pathfinish_def pathstart_def elim: piecewise_differentiable_on_subset) |
941 apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset) |
576 apply (rule piecewise_differentiable_affine [of g 1 "a-1", simplified o_def scaleR_one algebra_simps]) |
942 apply (rule piecewise_C1_differentiable_affine [of g 1 "a-1", simplified o_def scaleR_one algebra_simps]) |
577 apply (auto simp: pathfinish_def pathstart_def elim: piecewise_differentiable_on_subset) |
943 apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset) |
578 done |
944 done |
579 |
945 |
580 lemma has_path_integral_shiftpath: |
946 lemma has_path_integral_shiftpath: |
581 assumes f: "(f has_path_integral i) g" "valid_path g" |
947 assumes f: "(f has_path_integral i) g" "valid_path g" |
582 and a: "a \<in> {0..1}" |
948 and a: "a \<in> {0..1}" |
583 shows "(f has_path_integral i) (shiftpath a g)" |
949 shows "(f has_path_integral i) (shiftpath a g)" |
584 proof - |
950 proof - |
585 obtain s |
951 obtain s |
586 where s: "finite s" and g: "\<forall>x\<in>{0..1} - s. g differentiable at x" |
952 where s: "finite s" and g: "\<forall>x\<in>{0..1} - s. g differentiable at x" |
587 using assms by (auto simp: valid_path_def piecewise_differentiable_on_def) |
953 using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) |
588 have *: "((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" |
954 have *: "((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" |
589 using assms by (auto simp: has_path_integral) |
955 using assms by (auto simp: has_path_integral) |
590 then have i: "i = integral {a..1} (\<lambda>x. f (g x) * vector_derivative g (at x)) + |
956 then have i: "i = integral {a..1} (\<lambda>x. f (g x) * vector_derivative g (at x)) + |
591 integral {0..a} (\<lambda>x. f (g x) * vector_derivative g (at x))" |
957 integral {0..a} (\<lambda>x. f (g x) * vector_derivative g (at x))" |
592 apply (rule has_integral_unique) |
958 apply (rule has_integral_unique) |
656 "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}" |
1022 "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}" |
657 shows "(f has_path_integral i) g" |
1023 shows "(f has_path_integral i) g" |
658 proof - |
1024 proof - |
659 obtain s |
1025 obtain s |
660 where s: "finite s" and g: "\<forall>x\<in>{0..1} - s. g differentiable at x" |
1026 where s: "finite s" and g: "\<forall>x\<in>{0..1} - s. g differentiable at x" |
661 using assms by (auto simp: valid_path_def piecewise_differentiable_on_def) |
1027 using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) |
662 { fix x |
1028 { fix x |
663 assume x: "0 < x" "x < 1" "x \<notin> s" |
1029 assume x: "0 < x" "x < 1" "x \<notin> s" |
664 then have gx: "g differentiable at x" |
1030 then have gx: "g differentiable at x" |
665 using g by auto |
1031 using g by auto |
666 have "vector_derivative g (at x within {0..1}) = |
1032 have "vector_derivative g (at x within {0..1}) = |
702 "(linepath a b has_vector_derivative (b - a)) (at x within s)" |
1068 "(linepath a b has_vector_derivative (b - a)) (at x within s)" |
703 apply (simp add: linepath_def has_vector_derivative_def algebra_simps) |
1069 apply (simp add: linepath_def has_vector_derivative_def algebra_simps) |
704 apply (rule derivative_eq_intros | simp)+ |
1070 apply (rule derivative_eq_intros | simp)+ |
705 done |
1071 done |
706 |
1072 |
707 lemma valid_path_linepath [iff]: "valid_path (linepath a b)" |
|
708 apply (simp add: valid_path_def) |
|
709 apply (rule differentiable_on_imp_piecewise_differentiable) |
|
710 apply (simp add: differentiable_on_def differentiable_def) |
|
711 using has_vector_derivative_def has_vector_derivative_linepath_within by blast |
|
712 |
|
713 lemma vector_derivative_linepath_within: |
1073 lemma vector_derivative_linepath_within: |
714 "x \<in> {0..1} \<Longrightarrow> vector_derivative (linepath a b) (at x within {0..1}) = b - a" |
1074 "x \<in> {0..1} \<Longrightarrow> vector_derivative (linepath a b) (at x within {0..1}) = b - a" |
715 apply (rule vector_derivative_within_closed_interval [of 0 "1::real", simplified]) |
1075 apply (rule vector_derivative_within_closed_interval [of 0 "1::real", simplified]) |
716 apply (auto simp: has_vector_derivative_linepath_within) |
1076 apply (auto simp: has_vector_derivative_linepath_within) |
717 done |
1077 done |
718 |
1078 |
719 lemma vector_derivative_linepath_at: "vector_derivative (linepath a b) (at x) = b - a" |
1079 lemma vector_derivative_linepath_at [simp]: "vector_derivative (linepath a b) (at x) = b - a" |
720 by (simp add: has_vector_derivative_linepath_within vector_derivative_at) |
1080 by (simp add: has_vector_derivative_linepath_within vector_derivative_at) |
1081 |
|
1082 lemma valid_path_linepath [iff]: "valid_path (linepath a b)" |
|
1083 apply (simp add: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_on_linepath) |
|
1084 apply (rule_tac x="{}" in exI) |
|
1085 apply (simp add: differentiable_on_def differentiable_def) |
|
1086 using has_vector_derivative_def has_vector_derivative_linepath_within |
|
1087 apply (fastforce simp add: continuous_on_eq_continuous_within) |
|
1088 done |
|
721 |
1089 |
722 lemma has_path_integral_linepath: |
1090 lemma has_path_integral_linepath: |
723 shows "(f has_path_integral i) (linepath a b) \<longleftrightarrow> |
1091 shows "(f has_path_integral i) (linepath a b) \<longleftrightarrow> |
724 ((\<lambda>x. f(linepath a b x) * (b - a)) has_integral i) {0..1}" |
1092 ((\<lambda>x. f(linepath a b x) * (b - a)) has_integral i) {0..1}" |
725 by (simp add: has_path_integral vector_derivative_linepath_at) |
1093 by (simp add: has_path_integral vector_derivative_linepath_at) |
768 assumes "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" |
1136 assumes "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" |
769 shows "valid_path(subpath u v g)" |
1137 shows "valid_path(subpath u v g)" |
770 proof (cases "v=u") |
1138 proof (cases "v=u") |
771 case True |
1139 case True |
772 then show ?thesis |
1140 then show ?thesis |
773 by (simp add: valid_path_def subpath_def differentiable_on_def differentiable_on_imp_piecewise_differentiable) |
1141 unfolding valid_path_def subpath_def |
1142 by (force intro: C1_differentiable_on_const C1_differentiable_imp_piecewise) |
|
774 next |
1143 next |
775 case False |
1144 case False |
776 have "(g o (\<lambda>x. ((v-u) * x + u))) piecewise_differentiable_on {0..1}" |
1145 have "(g o (\<lambda>x. ((v-u) * x + u))) piecewise_C1_differentiable_on {0..1}" |
777 apply (rule piecewise_differentiable_compose) |
1146 apply (rule piecewise_C1_differentiable_compose) |
778 apply (simp add: differentiable_on_def differentiable_on_imp_piecewise_differentiable) |
1147 apply (simp add: C1_differentiable_imp_piecewise) |
779 apply (simp add: image_affinity_atLeastAtMost) |
1148 apply (simp add: image_affinity_atLeastAtMost) |
780 using assms False |
1149 using assms False |
781 apply (auto simp: algebra_simps valid_path_def piecewise_differentiable_on_subset) |
1150 apply (auto simp: algebra_simps valid_path_def piecewise_C1_differentiable_on_subset) |
782 apply (subst Int_commute) |
1151 apply (subst Int_commute) |
783 apply (auto simp: inj_on_def algebra_simps crossproduct_eq finite_vimage_IntI) |
1152 apply (auto simp: inj_on_def algebra_simps crossproduct_eq finite_vimage_IntI) |
784 done |
1153 done |
785 then show ?thesis |
1154 then show ?thesis |
786 by (auto simp: o_def valid_path_def subpath_def) |
1155 by (auto simp: o_def valid_path_def subpath_def) |
805 then show ?thesis |
1174 then show ?thesis |
806 using f by (simp add: path_integrable_on_def subpath_def has_path_integral) |
1175 using f by (simp add: path_integrable_on_def subpath_def has_path_integral) |
807 next |
1176 next |
808 case False |
1177 case False |
809 obtain s where s: "\<And>x. x \<in> {0..1} - s \<Longrightarrow> g differentiable at x" and fs: "finite s" |
1178 obtain s where s: "\<And>x. x \<in> {0..1} - s \<Longrightarrow> g differentiable at x" and fs: "finite s" |
810 using g by (auto simp: valid_path_def piecewise_differentiable_on_def) (blast intro: that) |
1179 using g unfolding piecewise_C1_differentiable_on_def C1_differentiable_on_eq valid_path_def by blast |
811 have *: "((\<lambda>x. f (g ((v - u) * x + u)) * vector_derivative g (at ((v - u) * x + u))) |
1180 have *: "((\<lambda>x. f (g ((v - u) * x + u)) * vector_derivative g (at ((v - u) * x + u))) |
812 has_integral (1 / (v - u)) * integral {u..v} (\<lambda>t. f (g t) * vector_derivative g (at t))) |
1181 has_integral (1 / (v - u)) * integral {u..v} (\<lambda>t. f (g t) * vector_derivative g (at t))) |
813 {0..1}" |
1182 {0..1}" |
814 using f uv |
1183 using f uv |
815 apply (simp add: path_integrable_on subpath_def has_path_integral) |
1184 apply (simp add: path_integrable_on subpath_def has_path_integral) |
967 and "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)" |
1336 and "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)" |
968 and "g piecewise_differentiable_on {a..b}" "\<And>x. x \<in> {a..b} \<Longrightarrow> g x \<in> s" |
1337 and "g piecewise_differentiable_on {a..b}" "\<And>x. x \<in> {a..b} \<Longrightarrow> g x \<in> s" |
969 shows "((\<lambda>x. f'(g x) * vector_derivative g (at x within {a..b})) |
1338 shows "((\<lambda>x. f'(g x) * vector_derivative g (at x within {a..b})) |
970 has_integral (f(g b) - f(g a))) {a..b}" |
1339 has_integral (f(g b) - f(g a))) {a..b}" |
971 proof - |
1340 proof - |
972 obtain k where k: "finite k" "\<forall>x\<in>{a..b} - k. g differentiable at x" and cg: "continuous_on {a..b} g" |
1341 obtain k where k: "finite k" "\<forall>x\<in>{a..b} - k. g differentiable (at x within {a..b})" and cg: "continuous_on {a..b} g" |
973 using assms by (auto simp: piecewise_differentiable_on_def) |
1342 using assms by (auto simp: piecewise_differentiable_on_def) |
974 have cfg: "continuous_on {a..b} (\<lambda>x. f (g x))" |
1343 have cfg: "continuous_on {a..b} (\<lambda>x. f (g x))" |
975 apply (rule continuous_on_compose [OF cg, unfolded o_def]) |
1344 apply (rule continuous_on_compose [OF cg, unfolded o_def]) |
976 using assms |
1345 using assms |
977 apply (metis complex_differentiable_def complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff) |
1346 apply (metis complex_differentiable_def complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff) |
1003 assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)" |
1372 assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)" |
1004 and "valid_path g" "path_image g \<subseteq> s" |
1373 and "valid_path g" "path_image g \<subseteq> s" |
1005 shows "(f' has_path_integral (f(pathfinish g) - f(pathstart g))) g" |
1374 shows "(f' has_path_integral (f(pathfinish g) - f(pathstart g))) g" |
1006 using assms |
1375 using assms |
1007 apply (simp add: valid_path_def path_image_def pathfinish_def pathstart_def has_path_integral_def) |
1376 apply (simp add: valid_path_def path_image_def pathfinish_def pathstart_def has_path_integral_def) |
1008 apply (auto intro!: path_integral_primitive_lemma [of 0 1 s]) |
1377 apply (auto intro!: piecewise_C1_imp_differentiable path_integral_primitive_lemma [of 0 1 s]) |
1009 done |
1378 done |
1010 |
1379 |
1011 corollary Cauchy_theorem_primitive: |
1380 corollary Cauchy_theorem_primitive: |
1012 assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)" |
1381 assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)" |
1013 and "valid_path g" "path_image g \<subseteq> s" "pathfinish g = pathstart g" |
1382 and "valid_path g" "path_image g \<subseteq> s" "pathfinish g = pathstart g" |
1060 "\<lbrakk>(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\<rbrakk> |
1429 "\<lbrakk>(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\<rbrakk> |
1061 \<Longrightarrow> ((\<lambda>x. f1 x + f2 x) has_path_integral (i1 + i2)) g" |
1430 \<Longrightarrow> ((\<lambda>x. f1 x + f2 x) has_path_integral (i1 + i2)) g" |
1062 by (simp add: has_integral_add has_path_integral_def algebra_simps) |
1431 by (simp add: has_integral_add has_path_integral_def algebra_simps) |
1063 |
1432 |
1064 lemma has_path_integral_diff: |
1433 lemma has_path_integral_diff: |
1065 shows "\<lbrakk>(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\<rbrakk> |
1434 "\<lbrakk>(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\<rbrakk> |
1066 \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) has_path_integral (i1 - i2)) g" |
1435 \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) has_path_integral (i1 - i2)) g" |
1067 by (simp add: has_integral_sub has_path_integral_def algebra_simps) |
1436 by (simp add: has_integral_sub has_path_integral_def algebra_simps) |
1068 |
1437 |
1069 lemma has_path_integral_lmul: |
1438 lemma has_path_integral_lmul: |
1070 shows "(f has_path_integral i) g |
1439 "(f has_path_integral i) g \<Longrightarrow> ((\<lambda>x. c * (f x)) has_path_integral (c*i)) g" |
1071 \<Longrightarrow> ((\<lambda>x. c * (f x)) has_path_integral (c*i)) g" |
|
1072 apply (simp add: has_path_integral_def) |
1440 apply (simp add: has_path_integral_def) |
1073 apply (drule has_integral_mult_right) |
1441 apply (drule has_integral_mult_right) |
1074 apply (simp add: algebra_simps) |
1442 apply (simp add: algebra_simps) |
1075 done |
1443 done |
1076 |
1444 |
1077 lemma has_path_integral_rmul: |
1445 lemma has_path_integral_rmul: |
1078 shows "(f has_path_integral i) g \<Longrightarrow> ((\<lambda>x. (f x) * c) has_path_integral (i*c)) g" |
1446 "(f has_path_integral i) g \<Longrightarrow> ((\<lambda>x. (f x) * c) has_path_integral (i*c)) g" |
1079 apply (drule has_path_integral_lmul) |
1447 apply (drule has_path_integral_lmul) |
1080 apply (simp add: mult.commute) |
1448 apply (simp add: mult.commute) |
1081 done |
1449 done |
1082 |
1450 |
1083 lemma has_path_integral_div: |
1451 lemma has_path_integral_div: |
1084 shows "(f has_path_integral i) g \<Longrightarrow> ((\<lambda>x. f x/c) has_path_integral (i/c)) g" |
1452 "(f has_path_integral i) g \<Longrightarrow> ((\<lambda>x. f x/c) has_path_integral (i/c)) g" |
1085 by (simp add: field_class.field_divide_inverse) (metis has_path_integral_rmul) |
1453 by (simp add: field_class.field_divide_inverse) (metis has_path_integral_rmul) |
1086 |
1454 |
1087 lemma has_path_integral_eq: |
1455 lemma has_path_integral_eq: |
1088 shows |
|
1089 "\<lbrakk>(f has_path_integral y) p; \<And>x. x \<in> path_image p \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> (g has_path_integral y) p" |
1456 "\<lbrakk>(f has_path_integral y) p; \<And>x. x \<in> path_image p \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> (g has_path_integral y) p" |
1090 apply (simp add: path_image_def has_path_integral_def) |
1457 apply (simp add: path_image_def has_path_integral_def) |
1091 by (metis (no_types, lifting) image_eqI has_integral_eq) |
1458 by (metis (no_types, lifting) image_eqI has_integral_eq) |
1092 |
1459 |
1093 lemma has_path_integral_bound_linepath: |
1460 lemma has_path_integral_bound_linepath: |
1418 and hvcon: "continuous_on {0..1} (\<lambda>t. vector_derivative h (at t))" |
1785 and hvcon: "continuous_on {0..1} (\<lambda>t. vector_derivative h (at t))" |
1419 shows "path_integral g (\<lambda>w. path_integral h (f w)) = |
1786 shows "path_integral g (\<lambda>w. path_integral h (f w)) = |
1420 path_integral h (\<lambda>z. path_integral g (\<lambda>w. f w z))" |
1787 path_integral h (\<lambda>z. path_integral g (\<lambda>w. f w z))" |
1421 proof - |
1788 proof - |
1422 have gcon: "continuous_on {0..1} g" and hcon: "continuous_on {0..1} h" |
1789 have gcon: "continuous_on {0..1} g" and hcon: "continuous_on {0..1} h" |
1423 using assms by (auto simp: valid_path_def piecewise_differentiable_on_def) |
1790 using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def) |
1424 have fgh1: "\<And>x. (\<lambda>t. f (g x) (h t)) = (\<lambda>(y1,y2). f y1 y2) o (\<lambda>t. (g x, h t))" |
1791 have fgh1: "\<And>x. (\<lambda>t. f (g x) (h t)) = (\<lambda>(y1,y2). f y1 y2) o (\<lambda>t. (g x, h t))" |
1425 by (rule ext) simp |
1792 by (rule ext) simp |
1426 have fgh2: "\<And>x. (\<lambda>t. f (g t) (h x)) = (\<lambda>(y1,y2). f y1 y2) o (\<lambda>t. (g t, h x))" |
1793 have fgh2: "\<And>x. (\<lambda>t. f (g t) (h x)) = (\<lambda>(y1,y2). f y1 y2) o (\<lambda>t. (g t, h x))" |
1427 by (rule ext) simp |
1794 by (rule ext) simp |
1428 have fcon_im1: "\<And>x. 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> continuous_on ((\<lambda>t. (g x, h t)) ` {0..1}) (\<lambda>(x, y). f x y)" |
1795 have fcon_im1: "\<And>x. 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> continuous_on ((\<lambda>t. (g x, h t)) ` {0..1}) (\<lambda>(x, y). f x y)" |
2067 ultimately show ?thesis |
2434 ultimately show ?thesis |
2068 using has_path_integral_integral by fastforce |
2435 using has_path_integral_integral by fastforce |
2069 qed |
2436 qed |
2070 |
2437 |
2071 |
2438 |
2072 |
|
2073 subsection\<open>Version allowing finite number of exceptional points\<close> |
2439 subsection\<open>Version allowing finite number of exceptional points\<close> |
2074 |
2440 |
2075 lemma Cauchy_theorem_triangle_cofinite: |
2441 lemma Cauchy_theorem_triangle_cofinite: |
2076 assumes "continuous_on (convex hull {a,b,c}) f" |
2442 assumes "continuous_on (convex hull {a,b,c}) f" |
2077 and "finite s" |
2443 and "finite s" |
2081 proof (induction "card s" arbitrary: a b c s rule: less_induct) |
2447 proof (induction "card s" arbitrary: a b c s rule: less_induct) |
2082 case (less s a b c) |
2448 case (less s a b c) |
2083 show ?case |
2449 show ?case |
2084 proof (cases "s={}") |
2450 proof (cases "s={}") |
2085 case True with less show ?thesis |
2451 case True with less show ?thesis |
2086 by (simp add: holomorphic_on_def complex_differentiable_at_within |
2452 by (fastforce simp: holomorphic_on_def complex_differentiable_at_within |
2087 Cauchy_theorem_triangle_interior) |
2453 Cauchy_theorem_triangle_interior) |
2088 next |
2454 next |
2089 case False |
2455 case False |
2090 then obtain d s' where d: "s = insert d s'" "d \<notin> s'" |
2456 then obtain d s' where d: "s = insert d s'" "d \<notin> s'" |
2091 by (meson Set.set_insert all_not_in_conv) |
2457 by (meson Set.set_insert all_not_in_conv) |
2467 (\<forall>y. norm(y - x) < d \<longrightarrow> (h has_field_derivative f y) (at y within s))" |
2833 (\<forall>y. norm(y - x) < d \<longrightarrow> (h has_field_derivative f y) (at y within s))" |
2468 shows "f path_integrable_on g" |
2834 shows "f path_integrable_on g" |
2469 using g |
2835 using g |
2470 apply (simp add: valid_path_def path_image_def path_integrable_on_def has_path_integral_def |
2836 apply (simp add: valid_path_def path_image_def path_integrable_on_def has_path_integral_def |
2471 has_integral_localized_vector_derivative integrable_on_def [symmetric]) |
2837 has_integral_localized_vector_derivative integrable_on_def [symmetric]) |
2472 apply (auto intro: path_integral_local_primitive_any [OF _ dh]) |
2838 using path_integral_local_primitive_any [OF _ dh] |
2473 done |
2839 by (meson image_subset_iff piecewise_C1_imp_differentiable) |
2474 |
2840 |
2475 |
2841 |
2476 text\<open>In particular if a function is holomorphic\<close> |
2842 text\<open>In particular if a function is holomorphic\<close> |
2477 |
2843 |
2478 lemma path_integrable_holomorphic: |
2844 lemma path_integrable_holomorphic: |
2597 "cmod (h t - p t) < ee (p u) / 3" |
2963 "cmod (h t - p t) < ee (p u) / 3" |
2598 by linarith+ |
2964 by linarith+ |
2599 then have "g t \<in> ball(p u) (ee(p u))" "h t \<in> ball(p u) (ee(p u))" |
2965 then have "g t \<in> ball(p u) (ee(p u))" "h t \<in> ball(p u) (ee(p u))" |
2600 using norm_diff_triangle_ineq [of "g t" "p t" "p t" "p u"] |
2966 using norm_diff_triangle_ineq [of "g t" "p t" "p t" "p u"] |
2601 norm_diff_triangle_ineq [of "h t" "p t" "p t" "p u"] ptu eepi u |
2967 norm_diff_triangle_ineq [of "h t" "p t" "p t" "p u"] ptu eepi u |
2602 by (force simp add: dist_norm ball_def norm_minus_commute)+ |
2968 by (force simp: dist_norm ball_def norm_minus_commute)+ |
2603 then have "g t \<in> s" "h t \<in> s" using ee u k |
2969 then have "g t \<in> s" "h t \<in> s" using ee u k |
2604 by (auto simp: path_image_def ball_def) |
2970 by (auto simp: path_image_def ball_def) |
2605 } |
2971 } |
2606 then have ghs: "path_image g \<subseteq> s" "path_image h \<subseteq> s" |
2972 then have ghs: "path_image g \<subseteq> s" "path_image h \<subseteq> s" |
2607 by (auto simp: path_image_def) |
2973 by (auto simp: path_image_def) |
2632 case 0 show ?case by simp |
2998 case 0 show ?case by simp |
2633 next |
2999 next |
2634 case (Suc n) |
3000 case (Suc n) |
2635 obtain t where t: "t \<in> k" and "p (n/N) \<in> ball(p t) (ee(p t) / 3)" |
3001 obtain t where t: "t \<in> k" and "p (n/N) \<in> ball(p t) (ee(p t) / 3)" |
2636 using `path_image p \<subseteq> \<Union>D` [THEN subsetD, where c="p (n/N)"] D_eq N Suc.prems |
3002 using `path_image p \<subseteq> \<Union>D` [THEN subsetD, where c="p (n/N)"] D_eq N Suc.prems |
2637 by (force simp add: path_image_def) |
3003 by (force simp: path_image_def) |
2638 then have ptu: "cmod (p t - p (n/N)) < ee (p t) / 3" |
3004 then have ptu: "cmod (p t - p (n/N)) < ee (p t) / 3" |
2639 by (simp add: dist_norm) |
3005 by (simp add: dist_norm) |
2640 have e3le: "e/3 \<le> ee (p t) / 3" using fin_eep t |
3006 have e3le: "e/3 \<le> ee (p t) / 3" using fin_eep t |
2641 by (simp add: e_def) |
3007 by (simp add: e_def) |
2642 { fix x |
3008 { fix x |
2777 \<longrightarrow> path_integral h f = path_integral g f))" |
3143 \<longrightarrow> path_integral h f = path_integral g f))" |
2778 using path_integral_nearby [OF assms, where Ends=True] |
3144 using path_integral_nearby [OF assms, where Ends=True] |
2779 using path_integral_nearby [OF assms, where Ends=False] |
3145 using path_integral_nearby [OF assms, where Ends=False] |
2780 by simp_all |
3146 by simp_all |
2781 |
3147 |
3148 thm has_vector_derivative_polynomial_function |
|
3149 corollary differentiable_polynomial_function: |
|
3150 fixes p :: "real \<Rightarrow> 'a::euclidean_space" |
|
3151 shows "polynomial_function p \<Longrightarrow> p differentiable_on s" |
|
3152 by (meson has_vector_derivative_polynomial_function differentiable_at_imp_differentiable_on differentiable_def has_vector_derivative_def) |
|
3153 |
|
3154 lemma C1_differentiable_polynomial_function: |
|
3155 fixes p :: "real \<Rightarrow> 'a::euclidean_space" |
|
3156 shows "polynomial_function p \<Longrightarrow> p C1_differentiable_on s" |
|
3157 by (metis continuous_on_polymonial_function C1_differentiable_on_def has_vector_derivative_polynomial_function) |
|
3158 |
|
2782 lemma valid_path_polynomial_function: |
3159 lemma valid_path_polynomial_function: |
2783 fixes p :: "real \<Rightarrow> 'b::euclidean_space" |
3160 fixes p :: "real \<Rightarrow> 'a::euclidean_space" |
2784 shows "polynomial_function p \<Longrightarrow> valid_path p" |
3161 shows "polynomial_function p \<Longrightarrow> valid_path p" |
2785 apply (simp add: valid_path_def) |
3162 by (force simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_polymonial_function C1_differentiable_polynomial_function) |
2786 apply (rule differentiable_on_imp_piecewise_differentiable [OF differentiable_at_imp_differentiable_on]) |
|
2787 using differentiable_def has_vector_derivative_def |
|
2788 apply (blast intro: dest: has_vector_derivative_polynomial_function) |
|
2789 done |
|
2790 |
3163 |
2791 lemma path_integral_bound_exists: |
3164 lemma path_integral_bound_exists: |
2792 assumes s: "open s" |
3165 assumes s: "open s" |
2793 and g: "valid_path g" |
3166 and g: "valid_path g" |
2794 and pag: "path_image g \<subseteq> s" |
3167 and pag: "path_image g \<subseteq> s" |