author  paulson <lp15@cam.ac.uk> 
Tue, 28 Jul 2015 16:16:13 +0100  
changeset 60809  457abb82fb9e 
child 61104  3c2d4636cebc 
permissions  rwrr 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

2 

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

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

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

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

6 

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

7 

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

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

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

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

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

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

13 

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

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

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

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

17 

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

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

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

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

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

22 

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

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

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

25 
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

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

27 
apply (rule_tac x="{a,b}" in exI, simp) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

28 
by (metis DiffE atLeastAtMost_diff_ends differentiable_on_subset subsetI 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

30 

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

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

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

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

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

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

36 

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

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

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

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

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

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

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

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

44 
apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f`{x})" in exI) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

46 

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

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

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

49 
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

50 
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

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

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

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

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

55 
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

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

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

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

59 
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

60 
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

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

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

63 

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

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

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

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

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

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

69 
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

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

71 
obtain s t where st: "finite s" "finite t" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

72 
"\<forall>x\<in>{a..c}  s. f differentiable at x" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

76 
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

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

78 
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

79 
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

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

81 
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

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

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

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

85 
assume x: "x \<in> {a..b}  insert c (s \<union> t)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

89 
apply (rule differentiable_transform_at [of "dist x c" _ f]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

95 
apply (rule differentiable_transform_at [of "dist x c" _ g]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

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

103 
by (metis (full_types) finite_Un finite_insert) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

107 

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

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

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

110 
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

111 

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

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

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

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

115 
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

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

117 
obtain s t where st: "finite s" "finite t" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

121 
then have "finite (s \<union> t) \<and> (\<forall>x\<in>i  (s \<union> t). (\<lambda>x. f x + g x) differentiable at x)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

123 
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

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

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

126 
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

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

128 

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

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

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

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

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

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

134 

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

135 

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

136 
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

137 

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

138 
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

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

140 

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

141 
definition valid_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

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

143 

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

144 
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

145 
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

146 

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

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

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

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

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

151 
{ fix s :: "real set" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

152 
assume df: "f differentiable_on g ` {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

155 
and dg: "\<And>x. x\<in>{0..1}  s \<Longrightarrow> g differentiable at x" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

156 
have dfo: "f differentiable_on g ` {0<..<1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

157 
by (auto intro: differentiable_on_subset [OF df]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

158 
have *: "\<And>x. x \<in> {0<..<1} \<Longrightarrow> x \<notin> s \<Longrightarrow> (f o g) differentiable (at x within ({0<..<1}  s))" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

160 
apply (simp_all add: dg differentiable_at_withinI differentiable_chain_within) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

164 
have oo: "open ({0<..<1}  s)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

166 
have "\<exists>s. finite s \<and> (\<forall>x\<in>{0..1}  s. f \<circ> g differentiable at x)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

167 
apply (rule_tac x="{0,1} Un s" in exI) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

168 
apply (simp add: Diff_Un_eq atLeastAtMost_diff_ends s del: Set.Un_insert_left, clarify) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

169 
apply (rule differentiable_within_open [OF _ oo, THEN iffD1]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

173 
by (clarsimp simp: valid_path_def piecewise_differentiable_on_def continuous_on_compose 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

174 
differentiable_imp_continuous_on path_image_def simp del: o_apply) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

176 

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

177 

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

178 
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

179 

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

180 
lemma valid_path_imp_path: "valid_path g \<Longrightarrow> path g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

182 

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

183 
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

184 
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

185 

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

186 
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

187 
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

188 

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

189 
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

190 
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

191 

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

192 
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

193 
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

194 

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

195 

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

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

197 

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

198 
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

199 

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

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

201 

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

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

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

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

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

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

207 

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

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

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

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

211 

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

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

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

214 

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

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

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

217 

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

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

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

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

221 

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

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

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

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

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

226 

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

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

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

229 

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

230 
(* 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

231 

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

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

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

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

235 
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

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

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

238 

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

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

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

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

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

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

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

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

246 
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

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

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

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

250 

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

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

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

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

254 
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

255 

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

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

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

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

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

260 

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

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

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

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

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

265 

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

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

267 

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

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

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

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

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

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

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

274 
then have "finite (op  1 ` s)" "(\<forall>x\<in>{0..1}  op  1 ` s. reversepath g differentiable at x)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

276 
apply (rule differentiable_chain_at [of "\<lambda>x::real. 1x" _ g, unfolded o_def]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

283 

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

284 
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

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

286 

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

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

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

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

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

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

292 
assume xs: "\<forall>x\<in>{0..1}  s. g differentiable at x" "x \<notin> op  1 ` s" "0 \<le> x" "x \<le> 1" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

293 
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

294 
 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

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

296 
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

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

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

299 
apply (simp_all add: has_vector_derivative_def differentiable_def, force) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

300 
apply (blast elim!: linear_imp_scaleR dest: has_derivative_linear) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

302 
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

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

304 
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

305 
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

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

307 
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

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

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

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

311 
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

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

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

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

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

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

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

318 
apply (drule has_integral_affinity01 [where m= "1" and c=1]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

321 
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

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

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

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

325 

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

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

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

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

329 

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

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

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

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

333 

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

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

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

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

337 

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

338 

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

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

340 

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

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

342 
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

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

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

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

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

347 
moreover have "(g1 o (\<lambda>x. 2*x)) piecewise_differentiable_on {0..1/2}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

352 
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

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

354 
moreover have "(g2 o (\<lambda>x. 2*x1)) piecewise_differentiable_on {1/2..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

367 

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

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

369 
"continuous_on {0..1} (g1 +++ g2) \<Longrightarrow> continuous_on {0..1} g1" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

370 
apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (op*(inverse 2))"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

373 
apply (auto elim!: continuous_on_subset) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

375 

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

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

377 
"\<lbrakk>continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> continuous_on {0..1} g2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

378 
apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (\<lambda>x. inverse 2*x + 1/2)"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

379 
apply (simp add: joinpaths_def pathfinish_def pathstart_def Ball_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

381 
apply (auto elim!: continuous_on_subset) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

383 

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

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

385 
"(g1 +++ g2) piecewise_differentiable_on {0..1} \<Longrightarrow> g1 piecewise_differentiable_on {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

387 
apply (rule_tac x="insert 1 ((op*2)`s)" in exI) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

390 
apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_at) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

392 
apply (rule differentiable_chain_at derivative_intros  force)+ 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

394 

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

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

396 
"\<lbrakk>(g1 +++ g2) piecewise_differentiable_on {0..1}; pathfinish g1 = pathstart g2\<rbrakk> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

397 
\<Longrightarrow> g2 piecewise_differentiable_on {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

399 
apply (rule_tac x="insert 0 ((\<lambda>x. 2*x1)`s)" in exI) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

402 
apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_at) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

403 
apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: split_if_asm) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

406 

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

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

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

409 

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

410 
lemma valid_path_join_D2: "\<lbrakk>valid_path (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> valid_path g2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

412 

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

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

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

415 
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

416 

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

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

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

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

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

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

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

423 
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

424 
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

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

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

427 
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

428 
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

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

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

431 
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

432 
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

433 
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

434 
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

435 
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

436 
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

437 
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

438 
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

439 
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

440 
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

441 
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

442 
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

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

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

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

446 
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

447 
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

448 
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

449 
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

450 
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

451 
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

452 
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

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

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

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

456 
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

457 
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

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

459 
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

460 
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

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

462 
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

463 
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

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

465 
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

466 
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

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

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

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

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

471 
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

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

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

474 

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

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

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

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

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

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

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

481 

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

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

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

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

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

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

487 
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

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

489 
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

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

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

492 
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

493 
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

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

495 
then have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2))/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

496 
by (force 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

497 
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

498 
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

499 
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

500 
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

501 
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

502 
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

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

504 
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

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

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

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

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

509 
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

510 
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

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

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

513 

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

514 
lemma path_integrable_joinD2: (*FIXME: could combine these proofs*) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

521 
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

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

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

524 
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

525 
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

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

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

528 
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

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

530 
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

531 
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

532 
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

533 
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

534 
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

535 
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

536 
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

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

538 
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

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

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

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

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

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

544 
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

545 
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

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

547 
qed 
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 
lemma path_integrable_join [simp]: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

554 

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

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

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

557 
"\<lbrakk>f path_integrable_on g1; f path_integrable_on g2; valid_path g1; valid_path g2\<rbrakk> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

558 
\<Longrightarrow> path_integral (g1 +++ g2) f = path_integral g1 f + path_integral g2 f" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

560 

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

561 

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

562 
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

563 

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

564 
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

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

566 

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

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

568 
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

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

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

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

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

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

574 
apply (rule piecewise_differentiable_affine [of g 1 a, simplified o_def scaleR_one]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

575 
apply (auto simp: pathfinish_def pathstart_def elim: piecewise_differentiable_on_subset) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

576 
apply (rule piecewise_differentiable_affine [of g 1 "a1", simplified o_def scaleR_one algebra_simps]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

577 
apply (auto simp: pathfinish_def pathstart_def elim: piecewise_differentiable_on_subset) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

579 

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

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

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

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

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

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

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

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

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

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

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

590 
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

591 
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

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

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

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

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

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

597 
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

598 
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

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

600 
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

601 
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

602 
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

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

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

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

606 
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

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

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

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

610 
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

611 
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

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

613 
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

614 
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

615 
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

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

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

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

619 
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

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

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

622 
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

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

624 
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

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

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

627 
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

628 
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

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

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

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

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

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

634 
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

635 
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

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

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

638 
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

639 
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

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

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

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

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

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

645 
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

646 
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

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

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

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

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

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

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

653 

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

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

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

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

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

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

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

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

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

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

663 
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

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

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

666 
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

667 
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

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

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

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

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

672 
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

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

674 
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

675 
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

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

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

678 
have fi: "(f has_path_integral i) (shiftpath (1  a) (shiftpath a g))" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

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

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

687 

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

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

689 
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

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

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

692 

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

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

694 
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

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

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

697 

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

698 

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

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

700 

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

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

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

703 
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

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

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

706 

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

707 
lemma valid_path_linepath [iff]: "valid_path (linepath a b)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

712 

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

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

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

715 
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

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

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

718 

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

719 
lemma vector_derivative_linepath_at: "vector_derivative (linepath a b) (at x) = b  a" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

720 
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

721 

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

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

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

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

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

726 

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

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

728 
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

729 
by (auto simp: segment linepath_def) 
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 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

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

733 

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

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

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

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

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

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

739 
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

740 
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

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

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

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

744 

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

745 
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

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

747 

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

748 
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

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

750 

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

751 
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

752 
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

753 

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

754 
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

755 
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

756 

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

757 
lemma has_path_integral_trivial [iff]: "(f has_path_integral 0) (linepath a a)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

759 

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

760 
lemma path_integral_trivial [simp]: "path_integral (linepath a a) f = 0" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

762 

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

763 

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

764 
subsection\<open>Relation to subpath construction\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

765 

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

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

767 
fixes g :: "real \<Rightarrow> 'a :: real_normed_vector" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

768 
assumes "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

773 
by (simp add: valid_path_def subpath_def differentiable_on_def differentiable_on_imp_piecewise_differentiable) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

776 
have "(g o (\<lambda>x. ((vu) * x + u))) piecewise_differentiable_on {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

788 

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

789 
lemma has_path_integral_subpath_refl [iff]: "(f has_path_integral 0) (subpath u u g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

791 

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

792 
lemma path_integrable_subpath_refl [iff]: "f path_integrable_on (subpath u u g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

794 

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

795 
lemma path_integral_subpath_refl [simp]: "path_integral (subpath u u g) f = 0" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

797 

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

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

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

800 
and uv: "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

801 
shows "(f has_path_integral integral {u..v} (\<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

802 
(subpath u v g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

809 
obtain s where s: "\<And>x. x \<in> {0..1}  s \<Longrightarrow> g differentiable at x" and fs: "finite s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

810 
using g by (auto simp: valid_path_def piecewise_differentiable_on_def) (blast intro: that) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

811 
have *: "((\<lambda>x. f (g ((v  u) * x + u)) * vector_derivative g (at ((v  u) * x + u))) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

812 
has_integral (1 / (v  u)) * integral {u..v} (\<lambda>t. f (g t) * vector_derivative g (at t))) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

816 
apply (drule integrable_on_subcbox [where a=u and b=v, simplified]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

818 
apply (drule has_integral_affinity [where m="vu" and c=u, simplified]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

819 
apply (simp_all add: False image_affinity_atLeastAtMost_div_diff scaleR_conv_of_real) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

823 
have "x \<in> {0..1} \<Longrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

824 
x \<notin> (\<lambda>t. (vu) *\<^sub>R t + u) ` s \<Longrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

825 
vector_derivative (\<lambda>x. g ((vu) * x + u)) (at x) = (vu) *\<^sub>R vector_derivative g (at ((vu) * x + u))" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

826 
apply (rule vector_derivative_at [OF vector_diff_chain_at [simplified o_def]]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

828 
apply (cut_tac s [of "(v  u) * x + u"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

829 
using uv mult_left_le [of x "vu"] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

834 
apply (cut_tac has_integral_cmul [OF *, where c = "vu"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

837 
apply (rule_tac s = "(\<lambda>t. ((vu) *\<^sub>R t + u)) ` s" in has_integral_spike_finite) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

838 
apply (auto simp: inj_on_def False finite_vimageI vd scaleR_conv_of_real) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

841 

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

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

843 
assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

844 
shows "f path_integrable_on (subpath u v g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

845 
apply (cases u v rule: linorder_class.le_cases) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

846 
apply (metis path_integrable_on_def has_path_integral_subpath [OF assms]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

853 

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

854 
lemma has_integral_integrable_integral: "(f has_integral i) s \<longleftrightarrow> f integrable_on s \<and> integral s f = i" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

856 

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

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

858 
assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

859 
shows "(((\<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

860 
has_integral path_integral (subpath u v g) f) {u..v}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

863 
apply (rule integrable_on_subcbox [where a=u and b=v and s = "{0..1}", simplified]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

864 
apply (auto simp: path_integral_unique [OF has_path_integral_subpath] path_integrable_on) 
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 

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

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

868 
assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

869 
shows "path_integral (subpath u v g) f = 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

870 
integral {u..v} (\<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

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

872 

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

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

874 
assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "w \<in> {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

876 
shows "path_integral (subpath u v g) f + path_integral (subpath v w g) f = 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

877 
path_integral (subpath u w g) f" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

880 
apply (rule integrable_on_subcbox [where a=u and b=w and s = "{0..1}", simplified]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

883 

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

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

885 
assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "w \<in> {0..1}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

886 
shows "path_integral (subpath u v g) f + path_integral (subpath v w g) f = 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

887 
path_integral (subpath u w g) f" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

888 
proof (cases "u\<noteq>v \<and> v\<noteq>w \<and> u\<noteq>w") 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

890 
have *: "subpath v u g = reversepath(subpath u v g) \<and> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

891 
subpath w u g = reversepath(subpath u w g) \<and> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

892 
subpath w v g = reversepath(subpath v w g)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

894 
have "u < v \<and> v < w \<or> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

895 
u < w \<and> w < v \<or> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

896 
v < u \<and> u < w \<or> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

897 
v < w \<and> w < u \<or> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

898 
w < u \<and> u < v \<or> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

899 
w < v \<and> v < u" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

902 
using path_integral_subpath_combine_less [of f g u v w] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

903 
path_integral_subpath_combine_less [of f g u w v] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

904 
path_integral_subpath_combine_less [of f g v u w] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

905 
path_integral_subpath_combine_less [of f g v w u] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

906 
path_integral_subpath_combine_less [of f g w u v] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

907 
path_integral_subpath_combine_less [of f g w v u] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

918 
by (metis eq_neg_iff_add_eq_0 path_integrable_subpath path_integral_reversepath reversepath_subpath valid_path_subpath) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

920 

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

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

922 
shows "path_integral g f = integral {0..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

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

924 

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

925 

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

926 
subsection\<open>Segments via convex hulls\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

927 

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

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

929 
"closed_segment a b \<subseteq> (convex hull {a,b,c})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

930 
"closed_segment a c \<subseteq> (convex hull {a,b,c})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

931 
"closed_segment b c \<subseteq> (convex hull {a,b,c})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

932 
"closed_segment b a \<subseteq> (convex hull {a,b,c})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

933 
"closed_segment c a \<subseteq> (convex hull {a,b,c})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

934 
"closed_segment c b \<subseteq> (convex hull {a,b,c})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

935 
by (auto simp: segment_convex_hull linepath_of_real elim!: rev_subsetD [OF _ hull_mono]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

936 

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

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

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

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

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

941 
have "(1  inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \<in> convex hull s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

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

949 

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

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

951 
"s \<subseteq> convex hull t \<Longrightarrow> convex hull s \<subseteq> convex hull t" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

953 

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

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

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

956 
shows "a \<notin> interior(convex hull {a,b,c})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

957 
"b \<notin> interior(convex hull {a,b,c})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

958 
"c \<notin> interior(convex hull {a,b,c})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

960 

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

961 

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

962 
text\<open>Cauchy's theorem where there's a primitive\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

963 

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

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

965 
fixes f :: "complex \<Rightarrow> complex" and g :: "real \<Rightarrow> complex" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

966 
assumes "a \<le> b" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

968 
and "g piecewise_differentiable_on {a..b}" "\<And>x. x \<in> {a..b} \<Longrightarrow> g x \<in> s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

970 
has_integral (f(g b)  f(g a))) {a..b}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

972 
obtain k where k: "finite k" "\<forall>x\<in>{a..b}  k. g differentiable at x" and cg: "continuous_on {a..b} g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

975 
apply (rule continuous_on_compose [OF cg, unfolded o_def]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

977 
apply (metis complex_differentiable_def complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

980 
assume a: "a < x" and b: "x < b" and xk: "x \<notin> k" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

981 
then have "g differentiable at x within {a..b}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

983 
then have "(g has_vector_derivative vector_derivative g (at x within {a..b})) (at x within {a..b})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

985 
then have gdiff: "(g has_derivative (\<lambda>u. u * vector_derivative g (at x within {a..b}))) (at x within {a..b})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

987 
have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {a..b})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

988 
using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

989 
then have fdiff: "(f has_derivative op * (f' (g x))) (at (g x) within g ` {a..b})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

992 
using diff_chain_within [OF gdiff fdiff] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

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

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

1001 

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

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

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

1004 
and "valid_path g" "path_image g \<subseteq> s" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

1007 
apply (simp add: valid_path_def path_image_def pathfinish_def pathstart_def has_path_integral_def) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1008 
apply (auto intro!: path_integral_primitive_lemma [of 0 1 s]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1010 

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

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

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

1013 
and "valid_path g" "path_image g \<subseteq> s" "pathfinish g = pathstart g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

1016 
by (metis diff_self path_integral_primitive) 
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 

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

1019 
text\<open>Existence of path integral for continuous function\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1021 
assumes "continuous_on (closed_segment a b) f" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1022 
shows "f path_integrable_on (linepath a b)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1024 
have "continuous_on {0..1} ((\<lambda>x. f x * (b  a)) o linepath a b)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1025 
apply (rule continuous_on_compose [OF continuous_on_linepath], simp add: linepath_image_01) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

1029 
apply (simp add: path_integrable_on_def has_path_integral_def integrable_on_def [symmetric]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1030 
apply (rule integrable_continuous [of 0 "1::real", simplified]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1031 
apply (rule continuous_on_eq [where f = "\<lambda>x. f(linepath a b x)*(b  a)"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

1035 

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

1036 
lemma has_field_der_id: "((\<lambda>x. x\<^sup>2 / 2) has_field_derivative x) (at x)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

1039 

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

1040 
lemma path_integral_id [simp]: "path_integral (linepath a b) (\<lambda>y. y) = (b^2  a^2)/2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1042 
using path_integral_primitive [of UNIV "\<lambda>x. x^2/2" "\<lambda>x. x" "linepath a b"] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

1045 

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

1046 
lemma path_integrable_on_const [iff]: "(\<lambda>x. c) path_integrable_on (linepath a b)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1048 

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

1049 
lemma path_integrable_on_id [iff]: "(\<lambda>x. x) path_integrable_on (linepath a b)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1050 
by (simp add: continuous_on_id path_integrable_continuous_linepath) 
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 

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

1053 
subsection\<open>Arithmetical combining theorems\<close> 
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 has_path_integral_neg: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

1058 

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

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

1060 
"\<lbrakk>(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\<rbrakk> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1061 
\<Longrightarrow> ((\<lambda>x. f1 x + f2 x) has_path_integral (i1 + i2)) g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1063 

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

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

1065 
shows "\<lbrakk>(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\<rbrakk> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1066 
\<Longrightarrow> ((\<lambda>x. f1 x  f2 x) has_path_integral (i1  i2)) g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1067 
by (simp add: has_integral_sub has_path_integral_def algebra_simps) 
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 has_path_integral_lmul: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1071 
\<Longrightarrow> ((\<lambda>x. c * (f x)) has_path_integral (c*i)) g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

1076 

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

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

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

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

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

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

1082 

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

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

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

1085 
by (simp add: field_class.field_divide_inverse) (metis has_path_integral_rmul) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1086 

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

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

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

1089 
"\<lbrakk>(f has_path_integral y) p; \<And>x. x \<in> path_image p \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> (g has_path_integral y) p" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1091 
by (metis (no_types, lifting) image_eqI has_integral_eq) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1092 

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

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

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

1095 
"0 \<le> B" "\<And>x. x \<in> closed_segment a b \<Longrightarrow> norm(f x) \<le> B" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1096 
shows "norm i \<le> B * norm(b  a)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

1100 
have "norm (f (linepath a b x)) * 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1101 
norm (vector_derivative (linepath a b) (at x within {0..1})) \<le> B * norm (b  a)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1102 
by (auto intro: mult_mono simp: assms linepath_in_path of_real_linepath vector_derivative_linepath_within x) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1104 
have "norm i \<le> (B * norm (b  a)) * content (cbox 0 (1::real))" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1106 
[of _ "\<lambda>x. f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

1113 

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

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

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

1116 
fixes a :: real and f :: "complex \<Rightarrow> real" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

1119 
"0 \<le> B" "\<And>x::real. x \<in> closed_segment a b  k \<Longrightarrow> norm(f x) \<le> B" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1120 
shows "norm i \<le> B*norm(b  a)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1122 

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

1123 
lemma has_path_integral_const_linepath: "((\<lambda>x. c) has_path_integral c*(b  a))(linepath a b)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1125 
by (metis content_real diff_0_right has_integral_const_real lambda_one of_real_1 scaleR_conv_of_real zero_le_one) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1126 

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

1127 
lemma has_path_integral_0: "((\<lambda>x. 0) has_path_integral 0) g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1129 

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

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

1131 
"(\<And>z. z \<in> path_image g \<Longrightarrow> f z = 0) \<Longrightarrow> (f has_path_integral 0) g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1132 
by (rule has_path_integral_eq [OF has_path_integral_0]) auto 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1133 

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

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

1135 
"\<lbrakk>finite s; \<And>a. a \<in> s \<Longrightarrow> (f a has_path_integral i a) p\<rbrakk> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1136 
\<Longrightarrow> ((\<lambda>x. setsum (\<lambda>a. f a x) s) has_path_integral setsum i s) p" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1137 
by (induction s rule: finite_induct) (auto simp: has_path_integral_0 has_path_integral_add) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1138 

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

1139 

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

1140 
subsection \<open>Operations on path integrals\<close> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1141 

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

1142 
lemma path_integral_const_linepath [simp]: "path_integral (linepath a b) (\<lambda>x. c) = c*(b  a)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1143 
by (rule path_integral_unique [OF has_path_integral_const_linepath]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1144 

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

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

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

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

1148 

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

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

1150 
"f1 path_integrable_on g \<Longrightarrow> f2 path_integrable_on g \<Longrightarrow> path_integral g (\<lambda>x. f1 x + f2 x) = 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1151 
path_integral g f1 + path_integral g f2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1153 

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

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

1155 
"f1 path_integrable_on g \<Longrightarrow> f2 path_integrable_on g \<Longrightarrow> path_integral g (\<lambda>x. f1 x  f2 x) = 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1156 
path_integral g f1  path_integral g f2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1158 

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

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

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

1161 
\<Longrightarrow> path_integral g (\<lambda>x. c * f x) = c*path_integral g f" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1163 

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

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

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

1166 
\<Longrightarrow> path_integral g (\<lambda>x. f x * c) = path_integral g f * c" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1168 

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

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

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

1171 
\<Longrightarrow> path_integral g (\<lambda>x. f x / c) = path_integral g f / c" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1173 

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

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

1175 
"(\<And>x. x \<in> path_image p \<Longrightarrow> f x = g x) \<Longrightarrow> path_integral p f = path_integral p g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1177 

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

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

1179 
"(\<And>z. z \<in> path_image g \<Longrightarrow> f z = 0) \<Longrightarrow> path_integral g f = 0" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1181 

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

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

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

1184 
"\<lbrakk>f path_integrable_on (linepath a b); 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1185 
0 \<le> B; \<And>x. x \<in> closed_segment a b \<Longrightarrow> norm(f x) \<le> B\<rbrakk> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1186 
\<Longrightarrow> norm(path_integral (linepath a b) f) \<le> B*norm(b  a)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1188 
apply (auto simp: has_path_integral_integral) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1189 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1190 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1191 
lemma path_integral_0: "path_integral g (\<lambda>x. 0) = 0" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1192 
by (simp add: path_integral_unique has_path_integral_0) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1193 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1194 
lemma path_integral_setsum: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1195 
"\<lbrakk>finite s; \<And>a. a \<in> s \<Longrightarrow> (f a) path_integrable_on p\<rbrakk> 