author  eberlm <eberlm@in.tum.de> 
Thu, 30 Nov 2017 16:59:59 +0100  
changeset 67107  cef76a19125e 
parent 66884  c2128ab11f61 
child 67237  1fe0ec14a90a 
permissions  rwrr 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

2 

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

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

4 

63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63589
diff
changeset

5 
theory Cauchy_Integral_Theorem 
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63589
diff
changeset

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

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

8 

62620
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

9 
subsection\<open>Homeomorphisms of arc images\<close> 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

10 

d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

11 
lemma homeomorphism_arc: 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

12 
fixes g :: "real \<Rightarrow> 'a::t2_space" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

13 
assumes "arc g" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

14 
obtains h where "homeomorphism {0..1} (path_image g) g h" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

15 
using assms by (force simp add: arc_def homeomorphism_compact path_def path_image_def) 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

16 

d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

17 
lemma homeomorphic_arc_image_interval: 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

18 
fixes g :: "real \<Rightarrow> 'a::t2_space" and a::real 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

19 
assumes "arc g" "a < b" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

20 
shows "(path_image g) homeomorphic {a..b}" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

21 
proof  
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

22 
have "(path_image g) homeomorphic {0..1::real}" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

23 
by (meson assms(1) homeomorphic_def homeomorphic_sym homeomorphism_arc) 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

24 
also have "... homeomorphic {a..b}" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

25 
using assms by (force intro: homeomorphic_closed_intervals_real) 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

26 
finally show ?thesis . 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

27 
qed 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

28 

d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

29 
lemma homeomorphic_arc_images: 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

30 
fixes g :: "real \<Rightarrow> 'a::t2_space" and h :: "real \<Rightarrow> 'b::t2_space" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

31 
assumes "arc g" "arc h" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

32 
shows "(path_image g) homeomorphic (path_image h)" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

33 
proof  
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

34 
have "(path_image g) homeomorphic {0..1::real}" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

35 
by (meson assms homeomorphic_def homeomorphic_sym homeomorphism_arc) 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

36 
also have "... homeomorphic (path_image h)" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

37 
by (meson assms homeomorphic_def homeomorphism_arc) 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

38 
finally show ?thesis . 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

39 
qed 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

40 

65037
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

41 
lemma path_connected_arc_complement: 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

42 
fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

43 
assumes "arc \<gamma>" "2 \<le> DIM('a)" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

44 
shows "path_connected( path_image \<gamma>)" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

45 
proof  
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

46 
have "path_image \<gamma> homeomorphic {0..1::real}" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

47 
by (simp add: assms homeomorphic_arc_image_interval) 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

48 
then 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

49 
show ?thesis 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

50 
apply (rule path_connected_complement_homeomorphic_convex_compact) 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

51 
apply (auto simp: assms) 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

52 
done 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

53 
qed 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

54 

2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

55 
lemma connected_arc_complement: 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

56 
fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

57 
assumes "arc \<gamma>" "2 \<le> DIM('a)" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

58 
shows "connected( path_image \<gamma>)" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

59 
by (simp add: assms path_connected_arc_complement path_connected_imp_connected) 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

60 

2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

61 
lemma inside_arc_empty: 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

62 
fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

63 
assumes "arc \<gamma>" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

64 
shows "inside(path_image \<gamma>) = {}" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

65 
proof (cases "DIM('a) = 1") 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

66 
case True 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

67 
then show ?thesis 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

68 
using assms connected_arc_image connected_convex_1_gen inside_convex by blast 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

69 
next 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

70 
case False 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

71 
show ?thesis 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

72 
proof (rule inside_bounded_complement_connected_empty) 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

73 
show "connected ( path_image \<gamma>)" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

74 
apply (rule connected_arc_complement [OF assms]) 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

75 
using False 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

76 
by (metis DIM_ge_Suc0 One_nat_def Suc_1 not_less_eq_eq order_class.order.antisym) 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

77 
show "bounded (path_image \<gamma>)" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

78 
by (simp add: assms bounded_arc_image) 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

79 
qed 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

80 
qed 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

81 

2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

82 
lemma inside_simple_curve_imp_closed: 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

83 
fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

84 
shows "\<lbrakk>simple_path \<gamma>; x \<in> inside(path_image \<gamma>)\<rbrakk> \<Longrightarrow> pathfinish \<gamma> = pathstart \<gamma>" 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

85 
using arc_simple_path inside_arc_empty by blast 
2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

86 

2cf841ff23be
some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents:
65036
diff
changeset

87 

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

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

89 

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

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

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

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

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

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

95 

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

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

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

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

99 

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

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

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

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

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

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

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

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

107 

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

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

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

110 
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

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

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

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

114 

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

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

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

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

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

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

120 

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

123 

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

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

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

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

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

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

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

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

131 
apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f`{x})" in exI) 
65036
ab7e11730ad8
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
paulson <lp15@cam.ac.uk>
parents:
64788
diff
changeset

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

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

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

137 
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

138 
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

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

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

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

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

143 
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

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

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

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

147 
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

148 
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

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

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

151 

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

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

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

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

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

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

157 
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

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

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

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

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

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

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

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

166 
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

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

168 
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

169 
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

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

171 
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

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

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

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

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

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

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

178 
case le show ?diff_fg 
63955  179 
proof (rule differentiable_transform_within [where d = "dist x c" and f = f]) 
180 
have "f differentiable at x within ({a<..<c}  s)" 

181 
apply (rule differentiable_at_withinI) 

182 
using x le st 

66793
deabce3ccf1f
new material about connectedness, etc.
paulson <lp15@cam.ac.uk>
parents:
66708
diff
changeset

183 
by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real le st(3) x) 
63955  184 
moreover have "open ({a<..<c}  s)" 
185 
by (blast intro: open_greaterThanLessThan \<open>finite s\<close> finite_imp_closed) 

186 
ultimately show "f differentiable at x within {a..b}" 

63969
f4b4fba60b1d
HOLAnalysis: move Library/Convex to Convex_Euclidean_Space
hoelzl
parents:
63955
diff
changeset

187 
using x le by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI) 
63955  188 
qed (use x le st dist_real_def in auto) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

190 
case ge show ?diff_fg 
63955  191 
proof (rule differentiable_transform_within [where d = "dist x c" and f = g]) 
192 
have "g differentiable at x within ({c<..<b}  t)" 

193 
apply (rule differentiable_at_withinI) 

194 
using x ge st 

66793
deabce3ccf1f
new material about connectedness, etc.
paulson <lp15@cam.ac.uk>
parents:
66708
diff
changeset

195 
by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real) 
63955  196 
moreover have "open ({c<..<b}  t)" 
197 
by (blast intro: open_greaterThanLessThan \<open>finite t\<close> finite_imp_closed) 

198 
ultimately show "g differentiable at x within {a..b}" 

63969
f4b4fba60b1d
HOLAnalysis: move Library/Convex to Convex_Euclidean_Space
hoelzl
parents:
63955
diff
changeset

199 
using x ge by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI) 
63955  200 
qed (use x ge st dist_real_def in auto) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

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

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

209 

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

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

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

212 
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

213 

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

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

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

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

217 
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

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

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

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

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

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

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

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

225 
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

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

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

228 
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

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

230 

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

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

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

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

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

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

236 

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

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

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

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

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

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

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

243 

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

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

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

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

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

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

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

250 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

264 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

279 

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

280 

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

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

282 

62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

283 
text \<open> 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

284 
John Harrison writes as follows: 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

285 

62456  286 
``The usual assumption in complex analysis texts is that a path \<open>\<gamma>\<close> should be piecewise 
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

287 
continuously differentiable, which ensures that the path integral exists at least for any continuous 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

288 
f, since all piecewise continuous functions are integrable. However, our notion of validity is 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

289 
weaker, just piecewise differentiability... [namely] continuity plus differentiability except on a 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

290 
ﬁnite set ... [Our] underlying theory of integration is the KurzweilHenstock theory. In contrast to 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

291 
the Riemann or Lebesgue theory (but in common with a simple notion based on antiderivatives), this 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

292 
can integrate all derivatives.'' 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

293 

62534
6855b348e828
complex_differentiable > field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset

294 
"Formalizing basic complex analysis." From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. 
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

295 
Studies in Logic, Grammar and Rhetoric 10.23 (2007): 151165. 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

296 

86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

297 
And indeed he does not assume that his derivatives are continuous, but the penalty is unreasonably 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

298 
difficult proofs concerning winding numbers. We need a selfcontained and straightforward theorem 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

299 
asserting that all derivatives can be integrated before we can adopt Harrison's choice.\<close> 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

300 

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

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

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

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

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

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

306 

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

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

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

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

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

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

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

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

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

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

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

317 

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

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

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

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

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

322 

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

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

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

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

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

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

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

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

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

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

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

333 

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

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

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

336 

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

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

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

339 

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

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

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

342 

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

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

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

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

346 

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

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

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

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

350 

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

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

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

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

354 

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

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

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

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

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

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

360 

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

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

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

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

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

365 

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

366 

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

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

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

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

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

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

372 

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

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

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

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

376 

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

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

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

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

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

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

382 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

396 

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

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

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

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

400 

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

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

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

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

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

405 

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

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

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

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

409 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

427 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

454 
case le show ?diff_fg 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

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

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

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

458 
case ge show ?diff_fg 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

473 
apply (rule vector_derivative_at [symmetric]) 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

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

475 
apply (simp_all add: dist_norm vector_derivative_works [symmetric]) 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

476 
apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff linorder_not_le order_less_irrefl st(1)) 
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

477 
apply auto 
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

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

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

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

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

482 
apply (rule vector_derivative_at [symmetric]) 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

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

484 
apply (simp_all add: dist_norm vector_derivative_works [symmetric]) 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

485 
apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff less_irrefl not_le st(2)) 
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

486 
apply auto 
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

502 

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

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

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

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

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

507 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

524 

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

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

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

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

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

530 

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

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

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

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

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

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

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

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

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

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

540 
then have g1D: "g1 differentiable at x" if "x \<in> {0..1}  insert 1 (op * 2 ` s)" for x 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

555 
apply (rule continuous_on_eq [OF _ vector_derivative_at]) 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

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

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

558 
apply (force intro: g1D differentiable_chain_at) 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

570 
using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast 
61222  571 
with \<open>finite s\<close> show ?thesis 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

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

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

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

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

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

577 

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

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

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

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

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

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

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

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

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

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

587 
then have g2D: "g2 differentiable at x" if "x \<in> {0..1}  insert 0 ((\<lambda>x. 2*x1) ` s)" for x 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

602 
apply (rule continuous_on_eq [OF _ vector_derivative_at]) 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

617 
using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast 
61222  618 
with \<open>finite s\<close> show ?thesis 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

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

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

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

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

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

624 

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

625 
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

626 

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

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

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

629 

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

630 
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

631 
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

632 

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

633 
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

634 

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

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

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

637 

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

638 
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

639 
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

640 

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

641 
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

642 
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

643 

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

644 
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

645 
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

646 

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

647 
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

648 
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

649 

62540
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

650 
proposition valid_path_compose: 
62623
dbc62f86a1a9
rationalisation of theorem names esp about "real Archimedian" etc.
paulson <lp15@cam.ac.uk>
parents:
62620
diff
changeset

651 
assumes "valid_path g" 
64394  652 
and der: "\<And>x. x \<in> path_image g \<Longrightarrow> f field_differentiable (at x)" 
62540
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

653 
and con: "continuous_on (path_image g) (deriv f)" 
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

654 
shows "valid_path (f o g)" 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

655 
proof  
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

656 
obtain s where "finite s" and g_diff: "g C1_differentiable_on {0..1}  s" 
62837  657 
using \<open>valid_path g\<close> unfolding valid_path_def piecewise_C1_differentiable_on_def by auto 
62540
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

658 
have "f \<circ> g differentiable at t" when "t\<in>{0..1}  s" for t 
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

659 
proof (rule differentiable_chain_at) 
62837  660 
show "g differentiable at t" using \<open>valid_path g\<close> 
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

661 
by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1}  s\<close> that) 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

662 
next 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

663 
have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis 
64394  664 
then show "f differentiable at (g t)" 
665 
using der[THEN field_differentiable_imp_differentiable] by auto 

62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

666 
qed 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

667 
moreover have "continuous_on ({0..1}  s) (\<lambda>x. vector_derivative (f \<circ> g) (at x))" 
62540
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

668 
proof (rule continuous_on_eq [where f = "\<lambda>x. vector_derivative g (at x) * deriv f (g x)"], 
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

669 
rule continuous_intros) 
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

670 
show "continuous_on ({0..1}  s) (\<lambda>x. vector_derivative g (at x))" 
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

671 
using g_diff C1_differentiable_on_eq by auto 
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

672 
next 
62623
dbc62f86a1a9
rationalisation of theorem names esp about "real Archimedian" etc.
paulson <lp15@cam.ac.uk>
parents:
62620
diff
changeset

673 
have "continuous_on {0..1} (\<lambda>x. deriv f (g x))" 
dbc62f86a1a9
rationalisation of theorem names esp about "real Archimedian" etc.
paulson <lp15@cam.ac.uk>
parents:
62620
diff
changeset

674 
using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def] 
62837  675 
\<open>valid_path g\<close> piecewise_C1_differentiable_on_def valid_path_def 
62540
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

676 
by blast 
62623
dbc62f86a1a9
rationalisation of theorem names esp about "real Archimedian" etc.
paulson <lp15@cam.ac.uk>
parents:
62620
diff
changeset

677 
then show "continuous_on ({0..1}  s) (\<lambda>x. deriv f (g x))" 
62540
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

678 
using continuous_on_subset by blast 
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

679 
next 
62540
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

680 
show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f \<circ> g) (at t)" 
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

681 
when "t \<in> {0..1}  s" for t 
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

682 
proof (rule vector_derivative_chain_at_general[symmetric]) 
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

683 
show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that) 
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

684 
next 
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

685 
have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis 
64394  686 
then show "f field_differentiable at (g t)" using der by auto 
62540
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

687 
qed 
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

688 
qed 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

689 
ultimately have "f o g C1_differentiable_on {0..1}  s" 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

690 
using C1_differentiable_on_eq by blast 
64394  691 
moreover have "path (f \<circ> g)" 
692 
apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]]) 

693 
using der 

694 
by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at) 

62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

695 
ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def 
62837  696 
using \<open>finite s\<close> by auto 
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

697 
qed 
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

698 

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

699 

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

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

701 

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

702 
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

703 

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

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

705 

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

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

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

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

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

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

711 

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

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

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

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

715 

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

716 
definition contour_integral 
62463
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

717 
where "contour_integral g f \<equiv> @i. (f has_contour_integral i) g \<or> ~ f contour_integrable_on g \<and> i=0" 
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

718 

547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

719 
lemma not_integrable_contour_integral: "~ f contour_integrable_on g \<Longrightarrow> contour_integral g f = 0" 
62534
6855b348e828
complex_differentiable > field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset

720 
unfolding contour_integrable_on_def contour_integral_def by blast 
62463
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

721 

547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

722 
lemma contour_integral_unique: "(f has_contour_integral i) g \<Longrightarrow> contour_integral g f = i" 
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

723 
apply (simp add: contour_integral_def has_contour_integral_def contour_integrable_on_def) 
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

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

725 

62131
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62101
diff
changeset

726 
corollary has_contour_integral_eqpath: 
62397
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset

727 
"\<lbrakk>(f has_contour_integral y) p; f contour_integrable_on \<gamma>; 
62131
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62101
diff
changeset

728 
contour_integral p f = contour_integral \<gamma> f\<rbrakk> 
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62101
diff
changeset

729 
\<Longrightarrow> (f has_contour_integral y) \<gamma>" 
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62101
diff
changeset

730 
using contour_integrable_on_def contour_integral_unique by auto 
1baed43f453e
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents:
62101
diff
changeset

731 

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

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

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

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

735 

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

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

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

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

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

740 

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

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

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

743 

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

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

745 

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

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

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

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

749 
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

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

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

752 

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

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

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

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

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

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

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

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

760 
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

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

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

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

764 

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

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

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

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

768 
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

769 

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

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

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

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

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

774 

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

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

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

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

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

779 

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

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

781 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

799 

62540
f2fc5485e3b0
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents:
62534
diff
changeset

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

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

802 

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

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

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

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

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

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

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

809 
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

810 
 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

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

812 
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

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

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

815 
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

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

817 
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

818 
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

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

820 
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

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

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

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

824 
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

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

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

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

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

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

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

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

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

833 
apply (drule has_integral_neg) 
65587
16a8991ab398
New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset

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

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

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

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

838 

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

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

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

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

842 

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

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

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

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

846 

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

847 
lemma contour_integral_reversepath: 
62463
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

848 
assumes "valid_path g" 
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

849 
shows "contour_integral (reversepath g) f =  (contour_integral g f)" 
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

850 
proof (cases "f contour_integrable_on g") 
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

851 
case True then show ?thesis 
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

852 
by (simp add: assms contour_integral_unique has_contour_integral_integral has_contour_integral_reversepath) 
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

853 
next 
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

854 
case False then have "~ f contour_integrable_on (reversepath g)" 
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

855 
by (simp add: assms contour_integrable_reversepath_eq) 
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

856 
with False show ?thesis by (simp add: not_integrable_contour_integral) 
547c5c6e66d4
the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

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

858 

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

859 

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

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

861 

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

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

863 
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

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

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

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

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

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

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

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

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

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

873 
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

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

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

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

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

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

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

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

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

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

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

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

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

886 

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

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

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

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

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

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

892 

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

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

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

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

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

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

898 

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

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

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

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

902 
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

903 

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

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

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

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

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

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

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

910 
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

911 
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

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

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

914 
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

915 
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

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

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

918 
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

919 
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

920 
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

921 
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

922 
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

923 
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

924 
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

925 
2 *\<^sub>R vector_derivative g1 (at (z*2))" for z 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

926 
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g1(2*x))" and d = "\<bar>z  1/2\<bar>"]]) 
62390  927 
apply (simp_all add: dist_real_def abs_if split: if_split_asm) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

928 
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

929 
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

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

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

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

933 
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

934 
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

935 
2 *\<^sub>R vector_derivative g2 (at (z*2  1))" for z 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

936 
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g2 (2*x  1))" and d = "\<bar>z  1/2\<bar>"]]) 
62390  937 
apply (simp_all add: dist_real_def abs_if split: if_split_asm) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

938 
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

939 
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

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

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

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

943 
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

944 
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

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

946 
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

947 
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

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

949 
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

950 
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

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

952 
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

953 
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

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

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

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

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

958 
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

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

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

961 

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

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

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

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

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

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

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

968 

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

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

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

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

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

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

974 
where s1: "finite s1" "\<forall>x\<in>{0..1}  s1. g1 differentiable at x" 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

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

976 
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

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

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

979 
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

980 
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

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

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

983 
by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

984 
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

985 
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

986 
2 *\<^sub>R vector_derivative g1 (at z)" for z 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

987 
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g1(2*x))" and d = "\<bar>(z1)/2\<bar>"]]) 
62390  988 
apply (simp_all add: field_simps dist_real_def abs_if split: if_split_asm) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

989 
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

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

991 
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

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

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

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

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

996 
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

997 
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

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

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

1000 

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

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

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

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

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

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

1006 
where s2: "finite s2" "\<forall>x\<in>{0..1}  s2. g2 differentiable at x" 
61190
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

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

1008 
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

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

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

1011 
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

1012 
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

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

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

1015 
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

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

1017 
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

1018 
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

1019 
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

1020 
2 *\<^sub>R vector_derivative g2 (at z)" for z 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

1021 
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g2(2*x1))" and d = "\<bar>z/2\<bar>"]]) 
62390  1022 
apply (simp_all add: field_simps dist_real_def abs_if split: if_split_asm) 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1023 
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

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

1025 
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

1026 
vector_derivative_works add_divide_distrib) 
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 
show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

1031 
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

1032 
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

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 

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

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

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

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

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

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

1041 

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

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

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

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

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

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

1047 

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

1050 

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

1051 
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

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

1053 

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

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

1055 
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

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

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

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

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

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

1061 
apply (rule piecewise_C1_differentiable_affine [of g 1 a, simplified o_def scaleR_one]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

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

1063 
apply (rule piecewise_C1_differentiable_affine [of g 1 "a1", simplified o_def scaleR_one algebra_simps]) 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

1064 
apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset) 
60809 