author  paulson <lp15@cam.ac.uk> 
Mon, 23 Nov 2015 16:57:54 +0000  
changeset 61738  c4f6031f1310 
parent 61711  21d7910d6816 
child 61762  d50b993b4fb9 
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 

61711
21d7910d6816
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

3 
text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close> 
21d7910d6816
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

4 

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

5 
theory Cauchy_Integral_Thm 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

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

8 

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

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

10 

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

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

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

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

14 
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

15 
(\<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

16 

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

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

18 
"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

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

20 

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

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

22 
"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

23 
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

24 
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

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

26 
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

27 
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

28 

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

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

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

31 
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

32 
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

33 
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

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

35 

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

36 
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

37 
"(\<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

38 
\<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

39 
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

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

41 

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

44 

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

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

46 
"\<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

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

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

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

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

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

52 
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

53 
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

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

55 

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

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

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

58 
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

59 
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

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

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

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

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

64 
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

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

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

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

68 
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

69 
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

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

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

72 

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

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

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

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

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

77 
"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

78 
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

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

80 
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

81 
"\<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

82 
"\<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

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

84 
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

85 
have finabc: "finite ({a,b,c} \<union> (s \<union> t))" 
61222  86 
by (metis \<open>finite s\<close> \<open>finite t\<close> finite_Un finite_insert finite.emptyI) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

87 
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

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

89 
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

90 
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

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

92 
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

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

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

95 
{ 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

96 
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

97 
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

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

99 
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

100 
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

101 
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

102 
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

103 
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

104 
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

105 
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

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

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

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

109 
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

110 
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

111 
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

112 
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

113 
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

114 
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

115 
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

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

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

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

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

120 
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

121 
(\<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

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

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

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

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

126 

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

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

128 
"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

129 
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

130 

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

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

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

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

134 
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

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

136 
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

137 
"\<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

138 
"\<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

139 
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

140 
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

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

142 
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

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

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

145 
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

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

147 

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

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

149 
"\<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

150 
\<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

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

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

153 

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

154 
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

155 
"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

156 
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

157 
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

158 
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

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

160 

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

161 
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

162 
"\<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

163 
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

164 
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

165 
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

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

167 

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

168 
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

169 
"(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

170 
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

171 
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

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

173 
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

174 
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

175 
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

176 
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

177 
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

178 
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

179 
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

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

181 

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

182 
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

183 
"\<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

184 
\<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

185 
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

186 
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

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

188 
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

189 
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

190 
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

191 
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

192 
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

193 
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

194 
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

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

196 

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 
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

199 

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

200 
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

201 
(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

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

203 
"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

204 
(\<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

205 

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

206 
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

207 
"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

208 
(\<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

209 
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

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

211 
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

212 
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

213 
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

214 
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

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

216 

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

217 
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

218 
"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

219 
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

220 
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

221 

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

222 
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

223 
"\<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

224 
\<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

225 
\<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

226 
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

227 
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

228 
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

229 
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

230 
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

231 
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

232 

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

233 
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

234 
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

235 

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

236 
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

237 
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

238 

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

239 
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

240 
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

241 

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

242 
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

243 
"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

244 
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

245 

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

246 
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

247 
"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

248 
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

249 

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

250 
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

251 
"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

252 
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

253 

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

254 
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

255 
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

256 
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

257 
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

258 
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

259 

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

260 
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

261 
"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

262 
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

263 
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

264 

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

265 

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

266 
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

267 
(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

268 
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

269 
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

270 
(\<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

271 

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

272 
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

273 
"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

274 
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

275 

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

276 
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

277 
"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

278 
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

279 
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

280 
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

281 

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

282 
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

283 
"\<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

284 
\<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

285 
\<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

286 
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

287 
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

288 
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

289 
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

290 
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

291 
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

292 
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

293 
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

294 
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

295 

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

296 
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

297 
"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

298 
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

299 

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

300 
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

301 
"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

302 
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

303 
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

304 

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

305 
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

306 
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

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

308 

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

309 
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

310 
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

311 
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

312 
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

313 
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

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

315 
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

316 
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

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

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

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

320 
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

321 
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

322 
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

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

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

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

326 

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

327 
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

328 
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

329 
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

330 
"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

331 
"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

332 
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

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

334 
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

335 
"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

336 
"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

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

338 
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

339 
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

340 
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

341 
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

342 
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

343 
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

344 
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

345 
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

346 
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

347 
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

348 
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

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

350 
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

351 
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

352 
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

353 
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

354 
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

355 
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

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

357 
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

358 
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

359 
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

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

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

362 
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

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

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

365 
{ 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

366 
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

367 
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

368 
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

369 
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

370 
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

371 
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

372 
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

373 
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

374 
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

375 
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

376 
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

377 
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

378 
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

379 
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

380 
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

381 
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

382 
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

383 
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

384 
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

385 
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

386 
(\<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

387 
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

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

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

390 
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

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

392 
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

393 
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

394 
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

395 
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

396 
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

397 
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

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

399 

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

400 
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

401 
"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

402 
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

403 
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

404 

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

405 
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

406 
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

407 
"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

408 
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

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

410 
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

411 
"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

412 
"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

413 
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

414 
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

415 
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

416 
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

417 
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

418 
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

419 
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

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

421 

61204  422 
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

423 
"\<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

424 
\<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

425 
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

426 
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

427 

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

428 
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

429 
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

430 
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

431 
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

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

433 
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

434 
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

435 
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

436 
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

437 
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

438 
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

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

440 
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

441 
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

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

443 
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

444 
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

445 
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

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

447 
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

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

449 
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

450 
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

451 
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

452 
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

453 
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

454 
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

455 
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

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

457 
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

458 
((\<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

459 
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

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

461 
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

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

463 
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

464 
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

465 
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

466 
using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast 
61222  467 
with \<open>finite s\<close> 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

468 
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

469 
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

470 
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

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

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

473 

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

474 
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

475 
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

476 
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

477 
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

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

479 
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

480 
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

481 
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

482 
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

483 
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

484 
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

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

486 
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

487 
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

488 
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

489 
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

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

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

492 
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

493 
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

494 
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

495 
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

496 
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

497 
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

498 
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

499 
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

500 
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

501 
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

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

503 
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

504 
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

505 
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

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

507 
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

508 
((\<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

509 
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

510 
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

511 
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

512 
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

513 
using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast 
61222  514 
with \<open>finite s\<close> 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

515 
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

516 
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

517 
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

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

519 
qed 
60809
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 
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

522 

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

523 
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

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

525 

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

526 
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

527 
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

528 

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

529 
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

530 
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

531 

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

532 
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

533 

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

534 
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

535 
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

536 

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

537 
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

538 
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

539 

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

540 
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

541 
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

542 

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

543 
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

544 
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

545 

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

546 
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

547 
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

548 

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

551 

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

552 
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

553 

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

554 
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

555 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

556 
definition has_contour_integral :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

557 
(infixr "has'_contour'_integral" 50) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

559 
((\<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

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

561 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

562 
definition contour_integrable_on 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

563 
(infixr "contour'_integrable'_on" 50) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

564 
where "f contour_integrable_on g \<equiv> \<exists>i. (f has_contour_integral i) g" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

565 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

566 
definition contour_integral 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

567 
where "contour_integral g f \<equiv> @i. (f has_contour_integral i) g" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

568 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

569 
lemma contour_integral_unique: "(f has_contour_integral i) g \<Longrightarrow> contour_integral g f = i" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

570 
by (auto simp: contour_integral_def has_contour_integral_def integral_def [symmetric]) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

571 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

572 
lemma has_contour_integral_integral: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

573 
"f contour_integrable_on i \<Longrightarrow> (f has_contour_integral (contour_integral i f)) i" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

574 
by (metis contour_integral_unique contour_integrable_on_def) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

575 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

576 
lemma has_contour_integral_unique: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

578 
using has_integral_unique 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

579 
by (auto simp: has_contour_integral_def) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

580 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

581 
lemma has_contour_integral_integrable: "(f has_contour_integral i) g \<Longrightarrow> f contour_integrable_on g" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

582 
using contour_integrable_on_def by blast 
60809
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 
(* 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

585 

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

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

587 
"\<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

588 
\<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

589 
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

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

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

592 

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

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

594 
"((\<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

595 
((\<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

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

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

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

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

600 
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

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

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

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

604 

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

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

606 
"(\<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

607 
(\<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

608 
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

609 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

610 
lemma has_contour_integral: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

612 
((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

613 
by (simp add: has_integral_localized_vector_derivative has_contour_integral_def) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

614 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

615 
lemma contour_integrable_on: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

617 
(\<lambda>t. f(g t) * vector_derivative g (at t)) integrable_on {0..1}" 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

618 
by (simp add: has_contour_integral integrable_on_def contour_integrable_on_def) 
60809
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 
subsection\<open>Reversing a path\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

621 

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

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

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

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

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

626 
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

627 
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

628 
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

629 
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

630 
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

631 
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

632 
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

633 
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

634 
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

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

636 
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

637 
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

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

639 

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

640 
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

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

642 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

643 
lemma has_contour_integral_reversepath: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

644 
assumes "valid_path g" "(f has_contour_integral i) g" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

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

647 
{ 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

648 
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

649 
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

650 
 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

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

652 
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

653 
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

654 
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

655 
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

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

657 
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

658 
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

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

660 
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

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

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

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

664 
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

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

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

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

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

669 
show ?thesis using assms 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

671 
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

672 
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

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

674 
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

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

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

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

678 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

679 
lemma contour_integrable_reversepath: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

680 
"valid_path g \<Longrightarrow> f contour_integrable_on g \<Longrightarrow> f contour_integrable_on (reversepath g)" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

681 
using has_contour_integral_reversepath contour_integrable_on_def by blast 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

682 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

683 
lemma contour_integrable_reversepath_eq: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

684 
"valid_path g \<Longrightarrow> (f contour_integrable_on (reversepath g) \<longleftrightarrow> f contour_integrable_on g)" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

685 
using contour_integrable_reversepath valid_path_reversepath by fastforce 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

686 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

687 
lemma contour_integral_reversepath: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

688 
"\<lbrakk>valid_path g; f contour_integrable_on g\<rbrakk> \<Longrightarrow> contour_integral (reversepath g) f = (contour_integral g f)" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

689 
using has_contour_integral_reversepath contour_integrable_on_def contour_integral_unique by blast 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

690 

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

693 

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

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

695 
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

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

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

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

699 
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

700 
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

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

702 
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

703 
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

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

705 
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

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

707 
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

708 
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

709 
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

710 
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

711 
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

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

713 
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

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

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

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

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

718 

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

719 
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

720 
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

721 
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

722 
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

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

724 

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

725 
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

726 
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

727 
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

728 
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

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

730 

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

731 
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

732 
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

733 
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

734 
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

735 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

736 
lemma has_contour_integral_join: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

738 
"valid_path g1" "valid_path g2" 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

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

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

742 
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

743 
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

744 
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

745 
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

746 
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

747 
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

748 
using assms 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

750 
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

751 
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

752 
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

753 
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

754 
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

755 
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

756 
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

757 
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

758 
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

759 
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

760 
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

761 
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

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

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

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

765 
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

766 
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

767 
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

768 
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

769 
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

770 
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

771 
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

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

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

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

775 
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

776 
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

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

778 
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

779 
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

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

781 
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

782 
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

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

784 
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

785 
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

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

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

788 
show ?thesis 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

790 
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

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

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

793 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

794 
lemma contour_integrable_joinI: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

796 
"valid_path g1" "valid_path g2" 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

798 
using assms 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

799 
by (meson has_contour_integral_join contour_integrable_on_def) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

800 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

801 
lemma contour_integrable_joinD1: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

802 
assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g1" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

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

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

806 
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

807 
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

808 
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

809 
using assms 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

811 
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

812 
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

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

814 
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

815 
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

816 
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

817 
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

818 
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

819 
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

820 
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

821 
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

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

823 
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

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

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

826 
using s1 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

828 
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

829 
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

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

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

832 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

833 
lemma contour_integrable_joinD2: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

834 
assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g2" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

835 
shows "f contour_integrable_on g2" 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

838 
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

839 
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

840 
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

841 
using assms 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

843 
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

844 
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

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

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

847 
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

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

849 
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

850 
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

851 
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

852 
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

853 
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

854 
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

855 
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

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

857 
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

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

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

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

861 
using s2 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

863 
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

864 
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

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

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

867 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

868 
lemma contour_integrable_join [simp]: 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

870 
"\<lbrakk>valid_path g1; valid_path g2\<rbrakk> 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

871 
\<Longrightarrow> f contour_integrable_on (g1 +++ g2) \<longleftrightarrow> f contour_integrable_on g1 \<and> f contour_integrable_on g2" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

872 
using contour_integrable_joinD1 contour_integrable_joinD2 contour_integrable_joinI by blast 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

873 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

874 
lemma contour_integral_join [simp]: 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

875 
shows 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

876 
"\<lbrakk>f contour_integrable_on g1; f contour_integrable_on g2; valid_path g1; valid_path g2\<rbrakk> 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

877 
\<Longrightarrow> contour_integral (g1 +++ g2) f = contour_integral g1 f + contour_integral g2 f" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

878 
by (simp add: has_contour_integral_integral has_contour_integral_join contour_integral_unique) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

879 

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 
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

882 

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

883 
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

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

885 

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

886 
lemma valid_path_shiftpath [intro]: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

887 
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

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

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

890 
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

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

892 
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

893 
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

894 
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

895 
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

896 
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

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

898 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

899 
lemma has_contour_integral_shiftpath: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

901 
and a: "a \<in> {0..1}" 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

902 
shows "(f has_contour_integral i) (shiftpath a g)" 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

905 
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

906 
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

907 
have *: "((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

908 
using assms by (auto simp: has_contour_integral) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

909 
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

910 
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

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

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

913 
apply (subst Integration.integral_combine) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

916 
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

917 
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

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

919 
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

920 
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

921 
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

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

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

924 
apply (drule_tac x="x+a" in bspec) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

925 
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

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

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

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

929 
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

930 
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

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

932 
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

933 
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

934 
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

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

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

937 
apply (drule_tac x="x+a1" in bspec) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

938 
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

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

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

941 
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

942 
using * a by (fastforce intro: integrable_subinterval_real) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

943 
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

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

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

946 
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

947 
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

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

949 
[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

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

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

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

953 
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

954 
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

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

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

957 
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

958 
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

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

960 
[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

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

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

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

964 
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

965 
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

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

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

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

969 
using a 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

970 
by (auto simp: i has_contour_integral intro: has_integral_combine [where c = "1a"]) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

972 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

973 
lemma has_contour_integral_shiftpath_D: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

974 
assumes "(f has_contour_integral i) (shiftpath a g)" 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

975 
"valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}" 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

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

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

979 
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

980 
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

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

982 
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

983 
then have gx: "g differentiable at x" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

985 
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

986 
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

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

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

989 
[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

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

991 
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

992 
vector_derivative_within_interior vector_derivative_works [symmetric]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

993 
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

994 
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

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

996 
} note vd = this 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

997 
have fi: "(f has_contour_integral i) (shiftpath (1  a) (shiftpath a g))" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

998 
using assms by (auto intro!: has_contour_integral_shiftpath) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

999 
show ?thesis 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1000 
apply (simp add: has_contour_integral_def) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1001 
apply (rule has_integral_spike_finite [of "{0,1} \<union> s", OF _ _ fi [unfolded has_contour_integral_def]]) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

1006 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

1008 
assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}" 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1009 
shows "(f has_contour_integral i) (shiftpath a g) \<longleftrightarrow> (f has_contour_integral i) g" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1010 
using assms has_contour_integral_shiftpath has_contour_integral_shiftpath_D by blast 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1011 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

1013 
assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}" 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1014 
shows "contour_integral (shiftpath a g) f = contour_integral g f" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1015 
using assms by (simp add: contour_integral_def has_contour_integral_shiftpath_eq) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1016 

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 
subsection\<open>More about straightline paths\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1019 

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

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

1021 
"(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

1022 
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

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

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

1025 

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

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

1027 
"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

1028 
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

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

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

1031 

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

1032 
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

1033 
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

1034 

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

1035 
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

1036 
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

1037 
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

1038 
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

1039 
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

1040 
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

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

1042 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1043 
lemma has_contour_integral_linepath: 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1044 
shows "(f has_contour_integral i) (linepath a b) \<longleftrightarrow> 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1045 
((\<lambda>x. f(linepath a b x) * (b  a)) has_integral i) {0..1}" 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

1047 

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

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

1049 
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

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

1051 

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

1052 
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

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

1054 

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

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

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

1057 
assumes a: "a \<in> convex hull s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1058 
and b: "b \<in> convex hull s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1059 
and x: "0\<le>x" "x\<le>1" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1060 
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

1061 
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

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

1063 
apply (auto simp: linepath_image_01 [symmetric]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1065 

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

1066 
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

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

1068 

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

1069 
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

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

1071 

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

1072 
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

1073 
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

1074 

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

1075 
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

1076 
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

1077 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1078 
lemma has_contour_integral_trivial [iff]: "(f has_contour_integral 0) (linepath a a)" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1079 
by (simp add: has_contour_integral_linepath) 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1080 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

1081 
lemma contour_integral_trivial [simp]: "contour_integral (linepath a a) f = 0" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset

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

1083 

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

1084 