author  paulson 
Mon, 21 Sep 2015 19:52:13 +0100  
changeset 61204  3e491e34a62e 
parent 61200  a5674da43c2b 
child 61222  05d28dc76e5c 
permissions  rwrr 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1 
section \<open>Complex path integrals and Cauchy's integral theorem\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

2 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

3 
theory Cauchy_Integral_Thm 
61104
3c2d4636cebc
new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents:
60809
diff
changeset

4 
imports Complex_Transcendental Weierstrass 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

5 
begin 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

6 

61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

7 
subsection \<open>Piecewise differentiable functions\<close> 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

8 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

9 
definition piecewise_differentiable_on 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

10 
(infixr "piecewise'_differentiable'_on" 50) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

11 
where "f piecewise_differentiable_on i \<equiv> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

12 
continuous_on i f \<and> 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

13 
(\<exists>s. finite s \<and> (\<forall>x \<in> i  s. f differentiable (at x within i)))" 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

14 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

15 
lemma piecewise_differentiable_on_imp_continuous_on: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

16 
"f piecewise_differentiable_on s \<Longrightarrow> continuous_on s f" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

17 
by (simp add: piecewise_differentiable_on_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

18 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

19 
lemma piecewise_differentiable_on_subset: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

20 
"f piecewise_differentiable_on s \<Longrightarrow> t \<le> s \<Longrightarrow> f piecewise_differentiable_on t" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

21 
using continuous_on_subset 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

22 
unfolding piecewise_differentiable_on_def 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

23 
apply safe 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

24 
apply (blast intro: elim: continuous_on_subset) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

25 
by (meson Diff_iff differentiable_within_subset subsetCE) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

26 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

27 
lemma differentiable_on_imp_piecewise_differentiable: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

28 
fixes a:: "'a::{linorder_topology,real_normed_vector}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

29 
shows "f differentiable_on {a..b} \<Longrightarrow> f piecewise_differentiable_on {a..b}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

30 
apply (simp add: piecewise_differentiable_on_def differentiable_imp_continuous_on) 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

31 
apply (rule_tac x="{a,b}" in exI, simp add: differentiable_on_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

32 
done 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

33 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

34 
lemma differentiable_imp_piecewise_differentiable: 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

35 
"(\<And>x. x \<in> s \<Longrightarrow> f differentiable (at x within s)) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

36 
\<Longrightarrow> f piecewise_differentiable_on s" 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

37 
by (auto simp: piecewise_differentiable_on_def differentiable_imp_continuous_on differentiable_on_def 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

38 
intro: differentiable_within_subset) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

39 

61204  40 
lemma piecewise_differentiable_const [iff]: "(\<lambda>x. z) piecewise_differentiable_on s" 
41 
by (simp add: differentiable_imp_piecewise_differentiable) 

42 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

43 
lemma piecewise_differentiable_compose: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

44 
"\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on (f ` s); 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

45 
\<And>x. finite (s \<inter> f`{x})\<rbrakk> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

46 
\<Longrightarrow> (g o f) piecewise_differentiable_on s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

47 
apply (simp add: piecewise_differentiable_on_def, safe) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

48 
apply (blast intro: continuous_on_compose2) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

49 
apply (rename_tac A B) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

50 
apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f`{x})" in exI) 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

51 
apply (blast intro: differentiable_chain_within) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

52 
done 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

53 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

54 
lemma piecewise_differentiable_affine: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

55 
fixes m::real 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

56 
assumes "f piecewise_differentiable_on ((\<lambda>x. m *\<^sub>R x + c) ` s)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

57 
shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_differentiable_on s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

58 
proof (cases "m = 0") 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

59 
case True 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

60 
then show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

61 
unfolding o_def 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

62 
by (force intro: differentiable_imp_piecewise_differentiable differentiable_const) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

63 
next 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

64 
case False 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

65 
show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

66 
apply (rule piecewise_differentiable_compose [OF differentiable_imp_piecewise_differentiable]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

67 
apply (rule assms derivative_intros  simp add: False vimage_def real_vector_affinity_eq)+ 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

68 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

69 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

70 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

71 
lemma piecewise_differentiable_cases: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

72 
fixes c::real 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

73 
assumes "f piecewise_differentiable_on {a..c}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

74 
"g piecewise_differentiable_on {c..b}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

75 
"a \<le> c" "c \<le> b" "f c = g c" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

76 
shows "(\<lambda>x. if x \<le> c then f x else g x) piecewise_differentiable_on {a..b}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

77 
proof  
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

78 
obtain s t where st: "finite s" "finite t" 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

79 
"\<forall>x\<in>{a..c}  s. f differentiable at x within {a..c}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

80 
"\<forall>x\<in>{c..b}  t. g differentiable at x within {c..b}" 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

81 
using assms 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

82 
by (auto simp: piecewise_differentiable_on_def) 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

83 
have finabc: "finite ({a,b,c} \<union> (s \<union> t))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

84 
by (metis `finite s` `finite t` finite_Un finite_insert finite.emptyI) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

85 
have "continuous_on {a..c} f" "continuous_on {c..b} g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

86 
using assms piecewise_differentiable_on_def by auto 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

87 
then have "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

88 
using continuous_on_cases [OF closed_real_atLeastAtMost [of a c], 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

89 
OF closed_real_atLeastAtMost [of c b], 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

90 
of f g "\<lambda>x. x\<le>c"] assms 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

91 
by (force simp: ivl_disj_un_two_touch) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

92 
moreover 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

93 
{ fix x 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

94 
assume x: "x \<in> {a..b}  ({a,b,c} \<union> (s \<union> t))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

95 
have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b}" (is "?diff_fg") 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

96 
proof (cases x c rule: le_cases) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

97 
case le show ?diff_fg 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

98 
apply (rule differentiable_transform_within [where d = "dist x c" and f = f]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

99 
using x le st 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

100 
apply (simp_all add: dist_real_def dist_nz [symmetric]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

101 
apply (rule differentiable_at_withinI) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

102 
apply (rule differentiable_within_open [where s = "{a<..<c}  s", THEN iffD1], simp_all) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

103 
apply (blast intro: open_greaterThanLessThan finite_imp_closed) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

104 
apply (force elim!: differentiable_subset) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

105 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

106 
next 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

107 
case ge show ?diff_fg 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

108 
apply (rule differentiable_transform_within [where d = "dist x c" and f = g]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

109 
using x ge st 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

110 
apply (simp_all add: dist_real_def dist_nz [symmetric]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

111 
apply (rule differentiable_at_withinI) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

112 
apply (rule differentiable_within_open [where s = "{c<..<b}  t", THEN iffD1], simp_all) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

113 
apply (blast intro: open_greaterThanLessThan finite_imp_closed) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

114 
apply (force elim!: differentiable_subset) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

115 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

116 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

117 
} 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

118 
then have "\<exists>s. finite s \<and> 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

119 
(\<forall>x\<in>{a..b}  s. (\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b})" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

120 
by (meson finabc) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

121 
ultimately show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

122 
by (simp add: piecewise_differentiable_on_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

123 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

124 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

125 
lemma piecewise_differentiable_neg: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

126 
"f piecewise_differentiable_on s \<Longrightarrow> (\<lambda>x. (f x)) piecewise_differentiable_on s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

127 
by (auto simp: piecewise_differentiable_on_def continuous_on_minus) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

128 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

129 
lemma piecewise_differentiable_add: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

130 
assumes "f piecewise_differentiable_on i" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

131 
"g piecewise_differentiable_on i" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

132 
shows "(\<lambda>x. f x + g x) piecewise_differentiable_on i" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

133 
proof  
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

134 
obtain s t where st: "finite s" "finite t" 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

135 
"\<forall>x\<in>i  s. f differentiable at x within i" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

136 
"\<forall>x\<in>i  t. g differentiable at x within i" 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

137 
using assms by (auto simp: piecewise_differentiable_on_def) 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

138 
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)" 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

139 
by auto 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

140 
moreover have "continuous_on i f" "continuous_on i g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

141 
using assms piecewise_differentiable_on_def by auto 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

142 
ultimately show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

143 
by (auto simp: piecewise_differentiable_on_def continuous_on_add) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

144 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

145 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

146 
lemma piecewise_differentiable_diff: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

147 
"\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on s\<rbrakk> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

148 
\<Longrightarrow> (\<lambda>x. f x  g x) piecewise_differentiable_on s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

149 
unfolding diff_conv_add_uminus 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

150 
by (metis piecewise_differentiable_add piecewise_differentiable_neg) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

151 

61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

152 
lemma continuous_on_joinpaths_D1: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

153 
"continuous_on {0..1} (g1 +++ g2) \<Longrightarrow> continuous_on {0..1} g1" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

154 
apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (op*(inverse 2))"]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

155 
apply (rule continuous_intros  simp)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

156 
apply (auto elim!: continuous_on_subset simp: joinpaths_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

157 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

158 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

159 
lemma continuous_on_joinpaths_D2: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

160 
"\<lbrakk>continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> continuous_on {0..1} g2" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

161 
apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (\<lambda>x. inverse 2*x + 1/2)"]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

162 
apply (rule continuous_intros  simp)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

163 
apply (auto elim!: continuous_on_subset simp add: joinpaths_def pathfinish_def pathstart_def Ball_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

164 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

165 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

166 
lemma piecewise_differentiable_D1: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

167 
"(g1 +++ g2) piecewise_differentiable_on {0..1} \<Longrightarrow> g1 piecewise_differentiable_on {0..1}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

168 
apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D1) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

169 
apply (rule_tac x="insert 1 ((op*2)`s)" in exI) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

170 
apply simp 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

171 
apply (intro ballI) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

172 
apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

173 
in differentiable_transform_within) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

174 
apply (auto simp: dist_real_def joinpaths_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

175 
apply (rule differentiable_chain_within derivative_intros  simp)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

176 
apply (rule differentiable_subset) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

177 
apply (force simp:)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

178 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

179 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

180 
lemma piecewise_differentiable_D2: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

181 
"\<lbrakk>(g1 +++ g2) piecewise_differentiable_on {0..1}; pathfinish g1 = pathstart g2\<rbrakk> 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

182 
\<Longrightarrow> g2 piecewise_differentiable_on {0..1}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

183 
apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D2) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

184 
apply (rule_tac x="insert 0 ((\<lambda>x. 2*x1)`s)" in exI) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

185 
apply simp 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

186 
apply (intro ballI) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

187 
apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

188 
in differentiable_transform_within) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

189 
apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: split_if_asm) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

190 
apply (rule differentiable_chain_within derivative_intros  simp)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

191 
apply (rule differentiable_subset) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

192 
apply (force simp: divide_simps)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

193 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

194 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

195 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

196 
subsubsection\<open>The concept of continuously differentiable\<close> 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

197 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

198 
definition C1_differentiable_on :: "(real \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> real set \<Rightarrow> bool" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

199 
(infix "C1'_differentiable'_on" 50) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

200 
where 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

201 
"f C1_differentiable_on s \<longleftrightarrow> 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

202 
(\<exists>D. (\<forall>x \<in> s. (f has_vector_derivative (D x)) (at x)) \<and> continuous_on s D)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

203 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

204 
lemma C1_differentiable_on_eq: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

205 
"f C1_differentiable_on s \<longleftrightarrow> 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

206 
(\<forall>x \<in> s. f differentiable at x) \<and> continuous_on s (\<lambda>x. vector_derivative f (at x))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

207 
unfolding C1_differentiable_on_def 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

208 
apply safe 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

209 
using differentiable_def has_vector_derivative_def apply blast 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

210 
apply (erule continuous_on_eq) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

211 
using vector_derivative_at apply fastforce 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

212 
using vector_derivative_works apply fastforce 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

213 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

214 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

215 
lemma C1_differentiable_on_subset: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

216 
"f C1_differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

217 
unfolding C1_differentiable_on_def continuous_on_eq_continuous_within 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

218 
by (blast intro: continuous_within_subset) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

219 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

220 
lemma C1_differentiable_compose: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

221 
"\<lbrakk>f C1_differentiable_on s; g C1_differentiable_on (f ` s); 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

222 
\<And>x. finite (s \<inter> f`{x})\<rbrakk> 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

223 
\<Longrightarrow> (g o f) C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

224 
apply (simp add: C1_differentiable_on_eq, safe) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

225 
using differentiable_chain_at apply blast 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

226 
apply (rule continuous_on_eq [of _ "\<lambda>x. vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

227 
apply (rule Limits.continuous_on_scaleR, assumption) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

228 
apply (metis (mono_tags, lifting) continuous_on_eq continuous_at_imp_continuous_on continuous_on_compose differentiable_imp_continuous_within o_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

229 
by (simp add: vector_derivative_chain_at) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

230 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

231 
lemma C1_diff_imp_diff: "f C1_differentiable_on s \<Longrightarrow> f differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

232 
by (simp add: C1_differentiable_on_eq differentiable_at_imp_differentiable_on) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

233 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

234 
lemma C1_differentiable_on_ident [simp, derivative_intros]: "(\<lambda>x. x) C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

235 
by (auto simp: C1_differentiable_on_eq continuous_on_const) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

236 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

237 
lemma C1_differentiable_on_const [simp, derivative_intros]: "(\<lambda>z. a) C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

238 
by (auto simp: C1_differentiable_on_eq continuous_on_const) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

239 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

240 
lemma C1_differentiable_on_add [simp, derivative_intros]: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

241 
"f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x + g x) C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

242 
unfolding C1_differentiable_on_eq by (auto intro: continuous_intros) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

243 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

244 
lemma C1_differentiable_on_minus [simp, derivative_intros]: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

245 
"f C1_differentiable_on s \<Longrightarrow> (\<lambda>x.  f x) C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

246 
unfolding C1_differentiable_on_eq by (auto intro: continuous_intros) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

247 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

248 
lemma C1_differentiable_on_diff [simp, derivative_intros]: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

249 
"f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x  g x) C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

250 
unfolding C1_differentiable_on_eq by (auto intro: continuous_intros) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

251 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

252 
lemma C1_differentiable_on_mult [simp, derivative_intros]: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

253 
fixes f g :: "real \<Rightarrow> 'a :: real_normed_algebra" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

254 
shows "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x * g x) C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

255 
unfolding C1_differentiable_on_eq 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

256 
by (auto simp: continuous_on_add continuous_on_mult continuous_at_imp_continuous_on differentiable_imp_continuous_within) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

257 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

258 
lemma C1_differentiable_on_scaleR [simp, derivative_intros]: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

259 
"f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

260 
unfolding C1_differentiable_on_eq 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

261 
by (rule continuous_intros  simp add: continuous_at_imp_continuous_on differentiable_imp_continuous_within)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

262 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

263 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

264 
definition piecewise_C1_differentiable_on 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

265 
(infixr "piecewise'_C1'_differentiable'_on" 50) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

266 
where "f piecewise_C1_differentiable_on i \<equiv> 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

267 
continuous_on i f \<and> 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

268 
(\<exists>s. finite s \<and> (f C1_differentiable_on (i  s)))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

269 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

270 
lemma C1_differentiable_imp_piecewise: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

271 
"f C1_differentiable_on s \<Longrightarrow> f piecewise_C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

272 
by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_at_imp_continuous_on differentiable_imp_continuous_within) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

273 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

274 
lemma piecewise_C1_imp_differentiable: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

275 
"f piecewise_C1_differentiable_on i \<Longrightarrow> f piecewise_differentiable_on i" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

276 
by (auto simp: piecewise_C1_differentiable_on_def piecewise_differentiable_on_def 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

277 
C1_differentiable_on_def differentiable_def has_vector_derivative_def 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

278 
intro: has_derivative_at_within) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

279 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

280 
lemma piecewise_C1_differentiable_compose: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

281 
"\<lbrakk>f piecewise_C1_differentiable_on s; g piecewise_C1_differentiable_on (f ` s); 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

282 
\<And>x. finite (s \<inter> f`{x})\<rbrakk> 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

283 
\<Longrightarrow> (g o f) piecewise_C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

284 
apply (simp add: piecewise_C1_differentiable_on_def, safe) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

285 
apply (blast intro: continuous_on_compose2) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

286 
apply (rename_tac A B) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

287 
apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f`{x})" in exI) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

288 
apply (rule conjI, blast) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

289 
apply (rule C1_differentiable_compose) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

290 
apply (blast intro: C1_differentiable_on_subset) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

291 
apply (blast intro: C1_differentiable_on_subset) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

292 
by (simp add: Diff_Int_distrib2) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

293 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

294 
lemma piecewise_C1_differentiable_on_subset: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

295 
"f piecewise_C1_differentiable_on s \<Longrightarrow> t \<le> s \<Longrightarrow> f piecewise_C1_differentiable_on t" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

296 
by (auto simp: piecewise_C1_differentiable_on_def elim!: continuous_on_subset C1_differentiable_on_subset) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

297 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

298 
lemma C1_differentiable_imp_continuous_on: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

299 
"f C1_differentiable_on s \<Longrightarrow> continuous_on s f" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

300 
unfolding C1_differentiable_on_eq continuous_on_eq_continuous_within 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

301 
using differentiable_at_withinI differentiable_imp_continuous_within by blast 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

302 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

303 
lemma C1_differentiable_on_empty [iff]: "f C1_differentiable_on {}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

304 
unfolding C1_differentiable_on_def 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

305 
by auto 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

306 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

307 
lemma piecewise_C1_differentiable_affine: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

308 
fixes m::real 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

309 
assumes "f piecewise_C1_differentiable_on ((\<lambda>x. m * x + c) ` s)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

310 
shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

311 
proof (cases "m = 0") 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

312 
case True 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

313 
then show ?thesis 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

314 
unfolding o_def by (auto simp: piecewise_C1_differentiable_on_def continuous_on_const) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

315 
next 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

316 
case False 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

317 
show ?thesis 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

318 
apply (rule piecewise_C1_differentiable_compose [OF C1_differentiable_imp_piecewise]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

319 
apply (rule assms derivative_intros  simp add: False vimage_def)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

320 
using real_vector_affinity_eq [OF False, where c=c, unfolded scaleR_conv_of_real] 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

321 
apply simp 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

322 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

323 
qed 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

324 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

325 
lemma piecewise_C1_differentiable_cases: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

326 
fixes c::real 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

327 
assumes "f piecewise_C1_differentiable_on {a..c}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

328 
"g piecewise_C1_differentiable_on {c..b}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

329 
"a \<le> c" "c \<le> b" "f c = g c" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

330 
shows "(\<lambda>x. if x \<le> c then f x else g x) piecewise_C1_differentiable_on {a..b}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

331 
proof  
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

332 
obtain s t where st: "f C1_differentiable_on ({a..c}  s)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

333 
"g C1_differentiable_on ({c..b}  t)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

334 
"finite s" "finite t" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

335 
using assms 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

336 
by (force simp: piecewise_C1_differentiable_on_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

337 
then have f_diff: "f differentiable_on {a..<c}  s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

338 
and g_diff: "g differentiable_on {c<..b}  t" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

339 
by (simp_all add: C1_differentiable_on_eq differentiable_at_withinI differentiable_on_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

340 
have "continuous_on {a..c} f" "continuous_on {c..b} g" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

341 
using assms piecewise_C1_differentiable_on_def by auto 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

342 
then have cab: "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

343 
using continuous_on_cases [OF closed_real_atLeastAtMost [of a c], 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

344 
OF closed_real_atLeastAtMost [of c b], 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

345 
of f g "\<lambda>x. x\<le>c"] assms 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

346 
by (force simp: ivl_disj_un_two_touch) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

347 
{ fix x 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

348 
assume x: "x \<in> {a..b}  insert c (s \<union> t)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

349 
have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x" (is "?diff_fg") 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

350 
proof (cases x c rule: le_cases) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

351 
case le show ?diff_fg 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

352 
apply (rule differentiable_transform_at [of "dist x c" _ f]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

353 
using x dist_real_def le st by (auto simp: C1_differentiable_on_eq) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

354 
next 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

355 
case ge show ?diff_fg 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

356 
apply (rule differentiable_transform_at [of "dist x c" _ g]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

357 
using dist_nz x dist_real_def ge st x by (auto simp: C1_differentiable_on_eq) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

358 
qed 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

359 
} 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

360 
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)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

361 
by auto 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

362 
moreover 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

363 
{ assume fcon: "continuous_on ({a<..<c}  s) (\<lambda>x. vector_derivative f (at x))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

364 
and gcon: "continuous_on ({c<..<b}  t) (\<lambda>x. vector_derivative g (at x))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

365 
have "open ({a<..<c}  s)" "open ({c<..<b}  t)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

366 
using st by (simp_all add: open_Diff finite_imp_closed) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

367 
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))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

368 
apply (rule continuous_on_eq [OF fcon]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

369 
apply (simp add:) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

370 
apply (rule vector_derivative_at [symmetric]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

371 
apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_at) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

372 
apply (simp_all add: dist_norm vector_derivative_works [symmetric]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

373 
using f_diff 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

374 
by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_imp_le st(1)) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

375 
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))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

376 
apply (rule continuous_on_eq [OF gcon]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

377 
apply (simp add:) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

378 
apply (rule vector_derivative_at [symmetric]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

379 
apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_at) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

380 
apply (simp_all add: dist_norm vector_derivative_works [symmetric]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

381 
using g_diff 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

382 
by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_imp_le st(2)) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

383 
ultimately have "continuous_on ({a<..<b}  insert c (s \<union> t)) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

384 
(\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

385 
apply (rule continuous_on_subset [OF continuous_on_open_Un], auto) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

386 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

387 
} note * = this 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

388 
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))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

389 
using st 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

390 
by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset intro: *) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

391 
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)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

392 
apply (rule_tac x="{a,b,c} \<union> s \<union> t" in exI) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

393 
using st by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

394 
with cab show ?thesis 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

395 
by (simp add: piecewise_C1_differentiable_on_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

396 
qed 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

397 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

398 
lemma piecewise_C1_differentiable_neg: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

399 
"f piecewise_C1_differentiable_on s \<Longrightarrow> (\<lambda>x. (f x)) piecewise_C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

400 
unfolding piecewise_C1_differentiable_on_def 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

401 
by (auto intro!: continuous_on_minus C1_differentiable_on_minus) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

402 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

403 
lemma piecewise_C1_differentiable_add: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

404 
assumes "f piecewise_C1_differentiable_on i" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

405 
"g piecewise_C1_differentiable_on i" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

406 
shows "(\<lambda>x. f x + g x) piecewise_C1_differentiable_on i" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

407 
proof  
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

408 
obtain s t where st: "finite s" "finite t" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

409 
"f C1_differentiable_on (is)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

410 
"g C1_differentiable_on (it)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

411 
using assms by (auto simp: piecewise_C1_differentiable_on_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

412 
then have "finite (s \<union> t) \<and> (\<lambda>x. f x + g x) C1_differentiable_on i  (s \<union> t)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

413 
by (auto intro: C1_differentiable_on_add elim!: C1_differentiable_on_subset) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

414 
moreover have "continuous_on i f" "continuous_on i g" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

415 
using assms piecewise_C1_differentiable_on_def by auto 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

416 
ultimately show ?thesis 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

417 
by (auto simp: piecewise_C1_differentiable_on_def continuous_on_add) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

418 
qed 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

419 

61204  420 
lemma piecewise_C1_differentiable_diff: 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

421 
"\<lbrakk>f piecewise_C1_differentiable_on s; g piecewise_C1_differentiable_on s\<rbrakk> 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

422 
\<Longrightarrow> (\<lambda>x. f x  g x) piecewise_C1_differentiable_on s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

423 
unfolding diff_conv_add_uminus 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

424 
by (metis piecewise_C1_differentiable_add piecewise_C1_differentiable_neg) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

425 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

426 
lemma piecewise_C1_differentiable_D1: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

427 
fixes g1 :: "real \<Rightarrow> 'a::real_normed_field" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

428 
assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

429 
shows "g1 piecewise_C1_differentiable_on {0..1}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

430 
proof  
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

431 
obtain s where "finite s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

432 
and co12: "continuous_on ({0..1}  s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

433 
and g12D: "\<forall>x\<in>{0..1}  s. g1 +++ g2 differentiable at x" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

434 
using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

435 
then have g1D: "g1 differentiable at x" if "x \<in> {0..1}  insert 1 (op * 2 ` s)" for x 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

436 
apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_at) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

437 
using that 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

438 
apply (simp_all add: dist_real_def joinpaths_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

439 
apply (rule differentiable_chain_at derivative_intros  force)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

440 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

441 
have [simp]: "vector_derivative (g1 \<circ> op * 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

442 
if "x \<in> {0..1}  insert 1 (op * 2 ` s)" for x 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

443 
apply (subst vector_derivative_chain_at) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

444 
using that 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

445 
apply (rule derivative_eq_intros g1D  simp)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

446 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

447 
have "continuous_on ({0..1/2}  insert (1/2) s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

448 
using co12 by (rule continuous_on_subset) force 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

449 
then have coDhalf: "continuous_on ({0..1/2}  insert (1/2) s) (\<lambda>x. vector_derivative (g1 o op*2) (at x))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

450 
apply (rule continuous_on_eq [OF _ vector_derivative_at]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

451 
apply (rule_tac f="g1 o op*2" and d="dist x (1/2)" in has_vector_derivative_transform_at) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

452 
apply (simp_all add: dist_norm joinpaths_def vector_derivative_works [symmetric]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

453 
apply (force intro: g1D differentiable_chain_at) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

454 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

455 
have "continuous_on ({0..1}  insert 1 (op * 2 ` s)) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

456 
((\<lambda>x. 1/2 * vector_derivative (g1 o op*2) (at x)) o op*(1/2))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

457 
apply (rule continuous_intros)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

458 
using coDhalf 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

459 
apply (simp add: scaleR_conv_of_real image_set_diff image_image) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

460 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

461 
then have con_g1: "continuous_on ({0..1}  insert 1 (op * 2 ` s)) (\<lambda>x. vector_derivative g1 (at x))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

462 
by (rule continuous_on_eq) (simp add: scaleR_conv_of_real) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

463 
have "continuous_on {0..1} g1" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

464 
using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

465 
with `finite s` show ?thesis 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

466 
apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

467 
apply (rule_tac x="insert 1 ((op*2)`s)" in exI) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

468 
apply (simp add: g1D con_g1) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

469 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

470 
qed 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

471 

2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

472 
lemma piecewise_C1_differentiable_D2: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

473 
fixes g2 :: "real \<Rightarrow> 'a::real_normed_field" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

474 
assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" "pathfinish g1 = pathstart g2" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

475 
shows "g2 piecewise_C1_differentiable_on {0..1}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

476 
proof  
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

477 
obtain s where "finite s" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

478 
and co12: "continuous_on ({0..1}  s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

479 
and g12D: "\<forall>x\<in>{0..1}  s. g1 +++ g2 differentiable at x" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

480 
using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

481 
then have g2D: "g2 differentiable at x" if "x \<in> {0..1}  insert 0 ((\<lambda>x. 2*x1) ` s)" for x 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

482 
apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_at) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

483 
using that 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

484 
apply (simp_all add: dist_real_def joinpaths_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

485 
apply (auto simp: dist_real_def joinpaths_def field_simps) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

486 
apply (rule differentiable_chain_at derivative_intros  force)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

487 
apply (drule_tac x= "(x + 1) / 2" in bspec, force simp: divide_simps) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

488 
apply assumption 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

489 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

490 
have [simp]: "vector_derivative (g2 \<circ> (\<lambda>x. 2*x1)) (at ((x+1)/2)) = 2 *\<^sub>R vector_derivative g2 (at x)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

491 
if "x \<in> {0..1}  insert 0 ((\<lambda>x. 2*x1) ` s)" for x 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

492 
using that by (auto simp: vector_derivative_chain_at divide_simps g2D) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

493 
have "continuous_on ({1/2..1}  insert (1/2) s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

494 
using co12 by (rule continuous_on_subset) force 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

495 
then have coDhalf: "continuous_on ({1/2..1}  insert (1/2) s) (\<lambda>x. vector_derivative (g2 o (\<lambda>x. 2*x1)) (at x))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

496 
apply (rule continuous_on_eq [OF _ vector_derivative_at]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

497 
apply (rule_tac f="g2 o (\<lambda>x. 2*x1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_at) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

498 
apply (auto simp: dist_real_def field_simps joinpaths_def vector_derivative_works [symmetric] 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

499 
intro!: g2D differentiable_chain_at) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

500 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

501 
have [simp]: "((\<lambda>x. (x + 1) / 2) ` ({0..1}  insert 0 ((\<lambda>x. 2 * x  1) ` s))) = ({1/2..1}  insert (1/2) s)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

502 
apply (simp add: image_set_diff inj_on_def image_image) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

503 
apply (auto simp: image_affinity_atLeastAtMost_div add_divide_distrib) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

504 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

505 
have "continuous_on ({0..1}  insert 0 ((\<lambda>x. 2*x1) ` s)) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

506 
((\<lambda>x. 1/2 * vector_derivative (g2 \<circ> (\<lambda>x. 2*x1)) (at x)) o (\<lambda>x. (x+1)/2))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

507 
by (rule continuous_intros  simp add: coDhalf)+ 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

508 
then have con_g2: "continuous_on ({0..1}  insert 0 ((\<lambda>x. 2*x1) ` s)) (\<lambda>x. vector_derivative g2 (at x))" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

509 
by (rule continuous_on_eq) (simp add: scaleR_conv_of_real) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

510 
have "continuous_on {0..1} g2" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

511 
using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

512 
with `finite s` show ?thesis 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

513 
apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

514 
apply (rule_tac x="insert 0 ((\<lambda>x. 2 * x  1) ` s)" in exI) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

515 
apply (simp add: g2D con_g2) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

516 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

517 
qed 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

518 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

519 
subsection \<open>Valid paths, and their start and finish\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

520 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

521 
lemma Diff_Un_eq: "A  (B \<union> C) = A  B  C" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

522 
by blast 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

523 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

524 
definition valid_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

525 
where "valid_path f \<equiv> f piecewise_C1_differentiable_on {0..1::real}" 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

526 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

527 
definition closed_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

528 
where "closed_path g \<equiv> g 0 = g 1" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

529 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

530 
subsubsection\<open>In particular, all results for paths apply\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

531 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

532 
lemma valid_path_imp_path: "valid_path g \<Longrightarrow> path g" 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

533 
by (simp add: path_def piecewise_C1_differentiable_on_def valid_path_def) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

534 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

535 
lemma connected_valid_path_image: "valid_path g \<Longrightarrow> connected(path_image g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

536 
by (metis connected_path_image valid_path_imp_path) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

537 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

538 
lemma compact_valid_path_image: "valid_path g \<Longrightarrow> compact(path_image g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

539 
by (metis compact_path_image valid_path_imp_path) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

540 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

541 
lemma bounded_valid_path_image: "valid_path g \<Longrightarrow> bounded(path_image g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

542 
by (metis bounded_path_image valid_path_imp_path) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

543 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

544 
lemma closed_valid_path_image: "valid_path g \<Longrightarrow> closed(path_image g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

545 
by (metis closed_path_image valid_path_imp_path) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

546 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

547 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

548 
subsection\<open>Contour Integrals along a path\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

549 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

550 
text\<open>This definition is for complex numbers only, and does not generalise to line integrals in a vector field\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

551 

61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

552 
text\<open>piecewise differentiable function on [0,1]\<close> 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

553 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

554 
definition has_path_integral :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

555 
(infixr "has'_path'_integral" 50) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

556 
where "(f has_path_integral i) g \<equiv> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

557 
((\<lambda>x. f(g x) * vector_derivative g (at x within {0..1})) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

558 
has_integral i) {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

559 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

560 
definition path_integrable_on 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

561 
(infixr "path'_integrable'_on" 50) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

562 
where "f path_integrable_on g \<equiv> \<exists>i. (f has_path_integral i) g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

563 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

564 
definition path_integral 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

565 
where "path_integral g f \<equiv> @i. (f has_path_integral i) g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

566 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

567 
lemma path_integral_unique: "(f has_path_integral i) g \<Longrightarrow> path_integral g f = i" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

568 
by (auto simp: path_integral_def has_path_integral_def integral_def [symmetric]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

569 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

570 
lemma has_path_integral_integral: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

571 
"f path_integrable_on i \<Longrightarrow> (f has_path_integral (path_integral i f)) i" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

572 
by (metis path_integral_unique path_integrable_on_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

573 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

574 
lemma has_path_integral_unique: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

575 
"(f has_path_integral i) g \<Longrightarrow> (f has_path_integral j) g \<Longrightarrow> i = j" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

576 
using has_integral_unique 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

577 
by (auto simp: has_path_integral_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

578 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

579 
lemma has_path_integral_integrable: "(f has_path_integral i) g \<Longrightarrow> f path_integrable_on g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

580 
using path_integrable_on_def by blast 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

581 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

582 
(* Show that we can forget about the localized derivative.*) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

583 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

584 
lemma vector_derivative_within_interior: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

585 
"\<lbrakk>x \<in> interior s; NO_MATCH UNIV s\<rbrakk> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

586 
\<Longrightarrow> vector_derivative f (at x within s) = vector_derivative f (at x)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

587 
apply (simp add: vector_derivative_def has_vector_derivative_def has_derivative_def netlimit_within_interior) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

588 
apply (subst lim_within_interior, auto) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

589 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

590 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

591 
lemma has_integral_localized_vector_derivative: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

592 
"((\<lambda>x. f (g x) * vector_derivative g (at x within {a..b})) has_integral i) {a..b} \<longleftrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

593 
((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {a..b}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

594 
proof  
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

595 
have "{a..b}  {a,b} = interior {a..b}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

596 
by (simp add: atLeastAtMost_diff_ends) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

597 
show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

598 
apply (rule has_integral_spike_eq [of "{a,b}"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

599 
apply (auto simp: vector_derivative_within_interior) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

600 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

601 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

602 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

603 
lemma integrable_on_localized_vector_derivative: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

604 
"(\<lambda>x. f (g x) * vector_derivative g (at x within {a..b})) integrable_on {a..b} \<longleftrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

605 
(\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on {a..b}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

606 
by (simp add: integrable_on_def has_integral_localized_vector_derivative) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

607 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

608 
lemma has_path_integral: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

609 
"(f has_path_integral i) g \<longleftrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

610 
((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

611 
by (simp add: has_integral_localized_vector_derivative has_path_integral_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

612 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

613 
lemma path_integrable_on: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

614 
"f path_integrable_on g \<longleftrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

615 
(\<lambda>t. f(g t) * vector_derivative g (at t)) integrable_on {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

616 
by (simp add: has_path_integral integrable_on_def path_integrable_on_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

617 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

618 
subsection\<open>Reversing a path\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

619 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

620 
lemma valid_path_imp_reverse: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

621 
assumes "valid_path g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

622 
shows "valid_path(reversepath g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

623 
proof  
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

624 
obtain s where "finite s" "g C1_differentiable_on ({0..1}  s)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

625 
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

626 
then have "finite (op  1 ` s)" "(reversepath g C1_differentiable_on ({0..1}  op  1 ` s))" 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

627 
apply (auto simp: reversepath_def) 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

628 
apply (rule C1_differentiable_compose [of "\<lambda>x::real. 1x" _ g, unfolded o_def]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

629 
apply (auto simp: C1_differentiable_on_eq) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

630 
apply (rule continuous_intros, force) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

631 
apply (force elim!: continuous_on_subset) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

632 
apply (simp add: finite_vimageI inj_on_def) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

633 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

634 
then show ?thesis using assms 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

635 
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def path_def [symmetric]) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

636 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

637 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

638 
lemma valid_path_reversepath: "valid_path(reversepath g) \<longleftrightarrow> valid_path g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

639 
using valid_path_imp_reverse by force 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

640 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

641 
lemma has_path_integral_reversepath: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

642 
assumes "valid_path g" "(f has_path_integral i) g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

643 
shows "(f has_path_integral (i)) (reversepath g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

644 
proof  
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

645 
{ fix s x 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

646 
assume xs: "g C1_differentiable_on ({0..1}  s)" "x \<notin> op  1 ` s" "0 \<le> x" "x \<le> 1" 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

647 
have "vector_derivative (\<lambda>x. g (1  x)) (at x within {0..1}) = 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

648 
 vector_derivative g (at (1  x) within {0..1})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

649 
proof  
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

650 
obtain f' where f': "(g has_vector_derivative f') (at (1  x))" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

651 
using xs 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

652 
by (force simp: has_vector_derivative_def C1_differentiable_on_def) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

653 
have "(g o (\<lambda>x. 1  x) has_vector_derivative 1 *\<^sub>R f') (at x)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

654 
apply (rule vector_diff_chain_within) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

655 
apply (intro vector_diff_chain_within derivative_eq_intros  simp)+ 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

656 
apply (rule has_vector_derivative_at_within [OF f']) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

657 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

658 
then have mf': "((\<lambda>x. g (1  x)) has_vector_derivative f') (at x)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

659 
by (simp add: o_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

660 
show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

661 
using xs 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

662 
by (auto simp: vector_derivative_at_within_ivl [OF mf'] vector_derivative_at_within_ivl [OF f']) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

663 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

664 
} note * = this 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

665 
have 01: "{0..1::real} = cbox 0 1" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

666 
by simp 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

667 
show ?thesis using assms 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

668 
apply (auto simp: has_path_integral_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

669 
apply (drule has_integral_affinity01 [where m= "1" and c=1]) 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

670 
apply (auto simp: reversepath_def valid_path_def piecewise_C1_differentiable_on_def) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

671 
apply (drule has_integral_neg) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

672 
apply (rule_tac s = "(\<lambda>x. 1  x) ` s" in has_integral_spike_finite) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

673 
apply (auto simp: *) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

674 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

675 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

676 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

677 
lemma path_integrable_reversepath: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

678 
"valid_path g \<Longrightarrow> f path_integrable_on g \<Longrightarrow> f path_integrable_on (reversepath g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

679 
using has_path_integral_reversepath path_integrable_on_def by blast 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

680 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

681 
lemma path_integrable_reversepath_eq: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

682 
"valid_path g \<Longrightarrow> (f path_integrable_on (reversepath g) \<longleftrightarrow> f path_integrable_on g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

683 
using path_integrable_reversepath valid_path_reversepath by fastforce 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

684 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

685 
lemma path_integral_reversepath: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

686 
"\<lbrakk>valid_path g; f path_integrable_on g\<rbrakk> \<Longrightarrow> path_integral (reversepath g) f = (path_integral g f)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

687 
using has_path_integral_reversepath path_integrable_on_def path_integral_unique by blast 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

688 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

689 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

690 
subsection\<open>Joining two paths together\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

691 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

692 
lemma valid_path_join: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

693 
assumes "valid_path g1" "valid_path g2" "pathfinish g1 = pathstart g2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

694 
shows "valid_path(g1 +++ g2)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

695 
proof  
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

696 
have "g1 1 = g2 0" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

697 
using assms by (auto simp: pathfinish_def pathstart_def) 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

698 
moreover have "(g1 o (\<lambda>x. 2*x)) piecewise_C1_differentiable_on {0..1/2}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

699 
apply (rule piecewise_C1_differentiable_compose) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

700 
using assms 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

701 
apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

702 
apply (rule continuous_intros  simp)+ 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

703 
apply (force intro: finite_vimageI [where h = "op*2"] inj_onI) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

704 
done 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

705 
moreover have "(g2 o (\<lambda>x. 2*x1)) piecewise_C1_differentiable_on {1/2..1}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

706 
apply (rule piecewise_C1_differentiable_compose) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

707 
using assms unfolding valid_path_def piecewise_C1_differentiable_on_def 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

708 
by (auto intro!: continuous_intros finite_vimageI [where h = "(\<lambda>x. 2*x  1)"] inj_onI 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

709 
simp: image_affinity_atLeastAtMost_diff continuous_on_joinpaths) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

710 
ultimately show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

711 
apply (simp only: valid_path_def continuous_on_joinpaths joinpaths_def) 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

712 
apply (rule piecewise_C1_differentiable_cases) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

713 
apply (auto simp: o_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

714 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

715 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

716 

61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

717 
lemma valid_path_join_D1: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

718 
fixes g1 :: "real \<Rightarrow> 'a::real_normed_field" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

719 
shows "valid_path (g1 +++ g2) \<Longrightarrow> valid_path g1" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

720 
unfolding valid_path_def 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

721 
by (rule piecewise_C1_differentiable_D1) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

722 

61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

723 
lemma valid_path_join_D2: 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

724 
fixes g2 :: "real \<Rightarrow> 'a::real_normed_field" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

725 
shows "\<lbrakk>valid_path (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> valid_path g2" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

726 
unfolding valid_path_def 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

727 
by (rule piecewise_C1_differentiable_D2) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

728 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

729 
lemma valid_path_join_eq [simp]: 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

730 
fixes g2 :: "real \<Rightarrow> 'a::real_normed_field" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

731 
shows "pathfinish g1 = pathstart g2 \<Longrightarrow> (valid_path(g1 +++ g2) \<longleftrightarrow> valid_path g1 \<and> valid_path g2)" 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

732 
using valid_path_join_D1 valid_path_join_D2 valid_path_join by blast 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

733 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

734 
lemma has_path_integral_join: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

735 
assumes "(f has_path_integral i1) g1" "(f has_path_integral i2) g2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

736 
"valid_path g1" "valid_path g2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

737 
shows "(f has_path_integral (i1 + i2)) (g1 +++ g2)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

738 
proof  
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

739 
obtain s1 s2 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

740 
where s1: "finite s1" "\<forall>x\<in>{0..1}  s1. g1 differentiable at x" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

741 
and s2: "finite s2" "\<forall>x\<in>{0..1}  s2. g2 differentiable at x" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

742 
using assms 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

743 
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

744 
have 1: "((\<lambda>x. f (g1 x) * vector_derivative g1 (at x)) has_integral i1) {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

745 
and 2: "((\<lambda>x. f (g2 x) * vector_derivative g2 (at x)) has_integral i2) {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

746 
using assms 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

747 
by (auto simp: has_path_integral) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

748 
have i1: "((\<lambda>x. (2*f (g1 (2*x))) * vector_derivative g1 (at (2*x))) has_integral i1) {0..1/2}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

749 
and i2: "((\<lambda>x. (2*f (g2 (2*x  1))) * vector_derivative g2 (at (2*x  1))) has_integral i2) {1/2..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

750 
using has_integral_affinity01 [OF 1, where m= 2 and c=0, THEN has_integral_cmul [where c=2]] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

751 
has_integral_affinity01 [OF 2, where m= 2 and c="1", THEN has_integral_cmul [where c=2]] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

752 
by (simp_all only: image_affinity_atLeastAtMost_div_diff, simp_all add: scaleR_conv_of_real mult_ac) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

753 
have g1: "\<lbrakk>0 \<le> z; z*2 < 1; z*2 \<notin> s1\<rbrakk> \<Longrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

754 
vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x  1)) (at z) = 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

755 
2 *\<^sub>R vector_derivative g1 (at (z*2))" for z 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

756 
apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>z  1/2\<bar>" _ "(\<lambda>x. g1(2*x))"]]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

757 
apply (simp_all add: dist_real_def abs_if split: split_if_asm) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

758 
apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x" 2 _ g1, simplified o_def]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

759 
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

760 
using s1 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

761 
apply (auto simp: algebra_simps vector_derivative_works) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

762 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

763 
have g2: "\<lbrakk>1 < z*2; z \<le> 1; z*2  1 \<notin> s2\<rbrakk> \<Longrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

764 
vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x  1)) (at z) = 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

765 
2 *\<^sub>R vector_derivative g2 (at (z*2  1))" for z 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

766 
apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>z  1/2\<bar>" _ "(\<lambda>x. g2 (2*x  1))"]]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

767 
apply (simp_all add: dist_real_def abs_if split: split_if_asm) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

768 
apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x  1" 2 _ g2, simplified o_def]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

769 
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

770 
using s2 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

771 
apply (auto simp: algebra_simps vector_derivative_works) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

772 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

773 
have "((\<lambda>x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i1) {0..1/2}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

774 
apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) (op*2 ` s1)"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

775 
using s1 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

776 
apply (force intro: finite_vimageI [where h = "op*2"] inj_onI) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

777 
apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g1) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

778 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

779 
moreover have "((\<lambda>x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i2) {1/2..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

780 
apply (rule has_integral_spike_finite [OF _ _ i2, of "insert (1/2) ((\<lambda>x. 2*x1) ` s2)"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

781 
using s2 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

782 
apply (force intro: finite_vimageI [where h = "\<lambda>x. 2*x1"] inj_onI) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

783 
apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g2) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

784 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

785 
ultimately 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

786 
show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

787 
apply (simp add: has_path_integral) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

788 
apply (rule has_integral_combine [where c = "1/2"], auto) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

789 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

790 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

791 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

792 
lemma path_integrable_joinI: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

793 
assumes "f path_integrable_on g1" "f path_integrable_on g2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

794 
"valid_path g1" "valid_path g2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

795 
shows "f path_integrable_on (g1 +++ g2)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

796 
using assms 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

797 
by (meson has_path_integral_join path_integrable_on_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

798 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

799 
lemma path_integrable_joinD1: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

800 
assumes "f path_integrable_on (g1 +++ g2)" "valid_path g1" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

801 
shows "f path_integrable_on g1" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

802 
proof  
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

803 
obtain s1 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

804 
where s1: "finite s1" "\<forall>x\<in>{0..1}  s1. g1 differentiable at x" 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

805 
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

806 
have "(\<lambda>x. f ((g1 +++ g2) (x/2)) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

807 
using assms 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

808 
apply (auto simp: path_integrable_on) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

809 
apply (drule integrable_on_subcbox [where a=0 and b="1/2"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

810 
apply (auto intro: integrable_affinity [of _ 0 "1/2::real" "1/2" 0, simplified]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

811 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

812 
then have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2))/2) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}" 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

813 
by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

814 
have g1: "\<lbrakk>0 < z; z < 1; z \<notin> s1\<rbrakk> \<Longrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

815 
vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x  1)) (at (z/2)) = 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

816 
2 *\<^sub>R vector_derivative g1 (at z)" for z 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

817 
apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>(z1)/2\<bar>" _ "(\<lambda>x. g1(2*x))"]]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

818 
apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

819 
apply (rule vector_diff_chain_at [of "\<lambda>x. x*2" 2 _ g1, simplified o_def]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

820 
using s1 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

821 
apply (auto simp: vector_derivative_works has_vector_derivative_def has_derivative_def bounded_linear_mult_left) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

822 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

823 
show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

824 
using s1 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

825 
apply (auto simp: path_integrable_on) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

826 
apply (rule integrable_spike_finite [of "{0,1} \<union> s1", OF _ _ *]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

827 
apply (auto simp: joinpaths_def scaleR_conv_of_real g1) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

828 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

829 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

830 

61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

831 
lemma path_integrable_joinD2: 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

832 
assumes "f path_integrable_on (g1 +++ g2)" "valid_path g2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

833 
shows "f path_integrable_on g2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

834 
proof  
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

835 
obtain s2 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

836 
where s2: "finite s2" "\<forall>x\<in>{0..1}  s2. g2 differentiable at x" 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

837 
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

838 
have "(\<lambda>x. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

839 
using assms 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

840 
apply (auto simp: path_integrable_on) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

841 
apply (drule integrable_on_subcbox [where a="1/2" and b=1], auto) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

842 
apply (drule integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2", simplified]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

843 
apply (simp add: image_affinity_atLeastAtMost_diff) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

844 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

845 
then have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2 + 1/2))/2) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

846 
integrable_on {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

847 
by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

848 
have g2: "\<lbrakk>0 < z; z < 1; z \<notin> s2\<rbrakk> \<Longrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

849 
vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x  1)) (at (z/2+1/2)) = 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

850 
2 *\<^sub>R vector_derivative g2 (at z)" for z 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

851 
apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>z/2\<bar>" _ "(\<lambda>x. g2(2*x1))"]]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

852 
apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

853 
apply (rule vector_diff_chain_at [of "\<lambda>x. x*21" 2 _ g2, simplified o_def]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

854 
using s2 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

855 
apply (auto simp: has_vector_derivative_def has_derivative_def bounded_linear_mult_left 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

856 
vector_derivative_works add_divide_distrib) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

857 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

858 
show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

859 
using s2 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

860 
apply (auto simp: path_integrable_on) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

861 
apply (rule integrable_spike_finite [of "{0,1} \<union> s2", OF _ _ *]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

862 
apply (auto simp: joinpaths_def scaleR_conv_of_real g2) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

863 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

864 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

865 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

866 
lemma path_integrable_join [simp]: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

867 
shows 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

868 
"\<lbrakk>valid_path g1; valid_path g2\<rbrakk> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

869 
\<Longrightarrow> f path_integrable_on (g1 +++ g2) \<longleftrightarrow> f path_integrable_on g1 \<and> f path_integrable_on g2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

870 
using path_integrable_joinD1 path_integrable_joinD2 path_integrable_joinI by blast 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

871 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

872 
lemma path_integral_join [simp]: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

873 
shows 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

874 
"\<lbrakk>f path_integrable_on g1; f path_integrable_on g2; valid_path g1; valid_path g2\<rbrakk> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

875 
\<Longrightarrow> path_integral (g1 +++ g2) f = path_integral g1 f + path_integral g2 f" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

876 
by (simp add: has_path_integral_integral has_path_integral_join path_integral_unique) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

877 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

878 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

879 
subsection\<open>Shifting the starting point of a (closed) path\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

880 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

881 
lemma shiftpath_alt_def: "shiftpath a f = (\<lambda>x. if x \<le> 1a then f (a + x) else f (a + x  1))" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

882 
by (auto simp: shiftpath_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

883 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

884 
lemma valid_path_shiftpath [intro]: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

885 
assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

886 
shows "valid_path(shiftpath a g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

887 
using assms 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

888 
apply (auto simp: valid_path_def shiftpath_alt_def) 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

889 
apply (rule piecewise_C1_differentiable_cases) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

890 
apply (auto simp: algebra_simps) 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

891 
apply (rule piecewise_C1_differentiable_affine [of g 1 a, simplified o_def scaleR_one]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

892 
apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

893 
apply (rule piecewise_C1_differentiable_affine [of g 1 "a1", simplified o_def scaleR_one algebra_simps]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

894 
apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

895 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

896 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

897 
lemma has_path_integral_shiftpath: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

898 
assumes f: "(f has_path_integral i) g" "valid_path g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

899 
and a: "a \<in> {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

900 
shows "(f has_path_integral i) (shiftpath a g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

901 
proof  
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

902 
obtain s 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

903 
where s: "finite s" and g: "\<forall>x\<in>{0..1}  s. g differentiable at x" 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

904 
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

905 
have *: "((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

906 
using assms by (auto simp: has_path_integral) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

907 
then have i: "i = integral {a..1} (\<lambda>x. f (g x) * vector_derivative g (at x)) + 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

908 
integral {0..a} (\<lambda>x. f (g x) * vector_derivative g (at x))" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

909 
apply (rule has_integral_unique) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

910 
apply (subst add.commute) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

911 
apply (subst Integration.integral_combine) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

912 
using assms * integral_unique by auto 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

913 
{ fix x 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

914 
have "0 \<le> x \<Longrightarrow> x + a < 1 \<Longrightarrow> x \<notin> (\<lambda>x. x  a) ` s \<Longrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

915 
vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a))" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

916 
unfolding shiftpath_def 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

917 
apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist(1a) x" _ "(\<lambda>x. g(a+x))"]]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

918 
apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

919 
apply (rule vector_diff_chain_at [of "\<lambda>x. x+a" 1 _ g, simplified o_def scaleR_one]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

920 
apply (intro derivative_eq_intros  simp)+ 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

921 
using g 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

922 
apply (drule_tac x="x+a" in bspec) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

923 
using a apply (auto simp: has_vector_derivative_def vector_derivative_works image_def add.commute) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

924 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

925 
} note vd1 = this 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

926 
{ fix x 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

927 
have "1 < x + a \<Longrightarrow> x \<le> 1 \<Longrightarrow> x \<notin> (\<lambda>x. x  a + 1) ` s \<Longrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

928 
vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a  1))" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

929 
unfolding shiftpath_def 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

930 
apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist (1a) x" _ "(\<lambda>x. g(a+x1))"]]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

931 
apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

932 
apply (rule vector_diff_chain_at [of "\<lambda>x. x+a1" 1 _ g, simplified o_def scaleR_one]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

933 
apply (intro derivative_eq_intros  simp)+ 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

934 
using g 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

935 
apply (drule_tac x="x+a1" in bspec) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

936 
using a apply (auto simp: has_vector_derivative_def vector_derivative_works image_def add.commute) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

937 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

938 
} note vd2 = this 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

939 
have va1: "(\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on ({a..1})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

940 
using * a by (fastforce intro: integrable_subinterval_real) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

941 
have v0a: "(\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on ({0..a})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

942 
apply (rule integrable_subinterval_real) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

943 
using * a by auto 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

944 
have "((\<lambda>x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x)) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

945 
has_integral integral {a..1} (\<lambda>x. f (g x) * vector_derivative g (at x))) {0..1  a}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

946 
apply (rule has_integral_spike_finite 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

947 
[where s = "{1a} \<union> (\<lambda>x. xa) ` s" and f = "\<lambda>x. f(g(a+x)) * vector_derivative g (at(a+x))"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

948 
using s apply blast 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

949 
using a apply (auto simp: algebra_simps vd1) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

950 
apply (force simp: shiftpath_def add.commute) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

951 
using has_integral_affinity [where m=1 and c=a, simplified, OF integrable_integral [OF va1]] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

952 
apply (simp add: image_affinity_atLeastAtMost_diff [where m=1 and c=a, simplified] add.commute) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

953 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

954 
moreover 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

955 
have "((\<lambda>x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x)) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

956 
has_integral integral {0..a} (\<lambda>x. f (g x) * vector_derivative g (at x))) {1  a..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

957 
apply (rule has_integral_spike_finite 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

958 
[where s = "{1a} \<union> (\<lambda>x. xa+1) ` s" and f = "\<lambda>x. f(g(a+x1)) * vector_derivative g (at(a+x1))"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

959 
using s apply blast 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

960 
using a apply (auto simp: algebra_simps vd2) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

961 
apply (force simp: shiftpath_def add.commute) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

962 
using has_integral_affinity [where m=1 and c="a1", simplified, OF integrable_integral [OF v0a]] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

963 
apply (simp add: image_affinity_atLeastAtMost [where m=1 and c="1a", simplified]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

964 
apply (simp add: algebra_simps) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

965 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

966 
ultimately show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

967 
using a 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

968 
by (auto simp: i has_path_integral intro: has_integral_combine [where c = "1a"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

969 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

970 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

971 
lemma has_path_integral_shiftpath_D: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

972 
assumes "(f has_path_integral i) (shiftpath a g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

973 
"valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

974 
shows "(f has_path_integral i) g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

975 
proof  
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

976 
obtain s 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

977 
where s: "finite s" and g: "\<forall>x\<in>{0..1}  s. g differentiable at x" 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

978 
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

979 
{ fix x 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

980 
assume x: "0 < x" "x < 1" "x \<notin> s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

981 
then have gx: "g differentiable at x" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

982 
using g by auto 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

983 
have "vector_derivative g (at x within {0..1}) = 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

984 
vector_derivative (shiftpath (1  a) (shiftpath a g)) (at x within {0..1})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

985 
apply (rule vector_derivative_at_within_ivl 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

986 
[OF has_vector_derivative_transform_within_open 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

987 
[of "{0<..<1}s" _ "(shiftpath (1  a) (shiftpath a g))"]]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

988 
using s g assms x 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

989 
apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

990 
vector_derivative_within_interior vector_derivative_works [symmetric]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

991 
apply (rule Derivative.differentiable_transform_at [of "min x (1x)", OF _ _ gx]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

992 
apply (auto simp: dist_real_def shiftpath_shiftpath abs_if) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

993 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

994 
} note vd = this 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

995 
have fi: "(f has_path_integral i) (shiftpath (1  a) (shiftpath a g))" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

996 
using assms by (auto intro!: has_path_integral_shiftpath) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

997 
show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

998 
apply (simp add: has_path_integral_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

999 
apply (rule has_integral_spike_finite [of "{0,1} \<union> s", OF _ _ fi [unfolded has_path_integral_def]]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1000 
using s assms vd 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1001 
apply (auto simp: Path_Connected.shiftpath_shiftpath) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1002 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1003 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1004 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1005 
lemma has_path_integral_shiftpath_eq: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1006 
assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1007 
shows "(f has_path_integral i) (shiftpath a g) \<longleftrightarrow> (f has_path_integral i) g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1008 
using assms has_path_integral_shiftpath has_path_integral_shiftpath_D by blast 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1009 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1010 
lemma path_integral_shiftpath: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1011 
assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1012 
shows "path_integral (shiftpath a g) f = path_integral g f" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1013 
using assms by (simp add: path_integral_def has_path_integral_shiftpath_eq) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1014 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1015 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1016 
subsection\<open>More about straightline paths\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1017 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1018 
lemma has_vector_derivative_linepath_within: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1019 
"(linepath a b has_vector_derivative (b  a)) (at x within s)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1020 
apply (simp add: linepath_def has_vector_derivative_def algebra_simps) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1021 
apply (rule derivative_eq_intros  simp)+ 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1022 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1023 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1024 
lemma vector_derivative_linepath_within: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1025 
"x \<in> {0..1} \<Longrightarrow> vector_derivative (linepath a b) (at x within {0..1}) = b  a" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1026 
apply (rule vector_derivative_within_closed_interval [of 0 "1::real", simplified]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1027 
apply (auto simp: has_vector_derivative_linepath_within) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1028 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1029 

61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1030 
lemma vector_derivative_linepath_at [simp]: "vector_derivative (linepath a b) (at x) = b  a" 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1031 
by (simp add: has_vector_derivative_linepath_within vector_derivative_at) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1032 

61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1033 
lemma valid_path_linepath [iff]: "valid_path (linepath a b)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1034 
apply (simp add: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_on_linepath) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1035 
apply (rule_tac x="{}" in exI) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1036 
apply (simp add: differentiable_on_def differentiable_def) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1037 
using has_vector_derivative_def has_vector_derivative_linepath_within 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1038 
apply (fastforce simp add: continuous_on_eq_continuous_within) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1039 
done 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1040 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1041 
lemma has_path_integral_linepath: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1042 
shows "(f has_path_integral i) (linepath a b) \<longleftrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1043 
((\<lambda>x. f(linepath a b x) * (b  a)) has_integral i) {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1044 
by (simp add: has_path_integral vector_derivative_linepath_at) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1045 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1046 
lemma linepath_in_path: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1047 
shows "x \<in> {0..1} \<Longrightarrow> linepath a b x \<in> closed_segment a b" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1048 
by (auto simp: segment linepath_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1049 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1050 
lemma linepath_image_01: "linepath a b ` {0..1} = closed_segment a b" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1051 
by (auto simp: segment linepath_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1052 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1053 
lemma linepath_in_convex_hull: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1054 
fixes x::real 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1055 
assumes a: "a \<in> convex hull s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1056 
and b: "b \<in> convex hull s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1057 
and x: "0\<le>x" "x\<le>1" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1058 
shows "linepath a b x \<in> convex hull s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1059 
apply (rule closed_segment_subset_convex_hull [OF a b, THEN subsetD]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1060 
using x 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1061 
apply (auto simp: linepath_image_01 [symmetric]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1062 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1063 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1064 
lemma Re_linepath: "Re(linepath (of_real a) (of_real b) x) = (1  x)*a + x*b" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1065 
by (simp add: linepath_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1066 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1067 
lemma Im_linepath: "Im(linepath (of_real a) (of_real b) x) = 0" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1068 
by (simp add: linepath_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1069 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1070 
lemma linepath_of_real: "(linepath (of_real a) (of_real b) x) = of_real ((1  x)*a + x*b)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1071 
by (simp add: scaleR_conv_of_real linepath_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1072 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1073 
lemma of_real_linepath: "of_real (linepath a b x) = linepath (of_real a) (of_real b) x" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1074 
by (metis linepath_of_real mult.right_neutral of_real_def real_scaleR_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1075 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1076 
lemma has_path_integral_trivial [iff]: "(f has_path_integral 0) (linepath a a)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1077 
by (simp add: has_path_integral_linepath) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1078 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1079 
lemma path_integral_trivial [simp]: "path_integral (linepath a a) f = 0" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1080 
using has_path_integral_trivial path_integral_unique by blast 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1081 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1082 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1083 
subsection\<open>Relation to subpath construction\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1084 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1085 
lemma valid_path_subpath: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1086 
fixes g :: "real \<Rightarrow> 'a :: real_normed_vector" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1087 
assumes "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1088 
shows "valid_path(subpath u v g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1089 
proof (cases "v=u") 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1090 
case True 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1091 
then show ?thesis 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1092 
unfolding valid_path_def subpath_def 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1093 
by (force intro: C1_differentiable_on_const C1_differentiable_imp_piecewise) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1094 
next 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1095 
case False 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1096 
have "(g o (\<lambda>x. ((vu) * x + u))) piecewise_C1_differentiable_on {0..1}" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1097 
apply (rule piecewise_C1_differentiable_compose) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1098 
apply (simp add: C1_differentiable_imp_piecewise) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1099 
apply (simp add: image_affinity_atLeastAtMost) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1100 
using assms False 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1101 
apply (auto simp: algebra_simps valid_path_def piecewise_C1_differentiable_on_subset) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1102 
apply (subst Int_commute) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1103 
apply (auto simp: inj_on_def algebra_simps crossproduct_eq finite_vimage_IntI) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1104 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1105 
then show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1106 
by (auto simp: o_def valid_path_def subpath_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1107 
qed 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1108 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1109 
lemma has_path_integral_subpath_refl [iff]: "(f has_path_integral 0) (subpath u u g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1110 
by (simp add: has_path_integral subpath_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1111 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1112 
lemma path_integrable_subpath_refl [iff]: "f path_integrable_on (subpath u u g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1113 
using has_path_integral_subpath_refl path_integrable_on_def by blast 