author  paulson <lp15@cam.ac.uk> 
Fri, 18 Sep 2015 16:27:37 +0100  
changeset 61190  2bd401e364f9 
parent 61104  3c2d4636cebc 
child 61200  a5674da43c2b 
permissions  rwrr 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

2 

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

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

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

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

6 

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

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

8 

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

9 
lemma inj_mult_left [simp]: "inj (op* x) \<longleftrightarrow> x \<noteq> (0::'a::idom)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

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

11 

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

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

13 
"s = t \<Longrightarrow> (\<And>x. x \<in> t =simp=> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

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

15 

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

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

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

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

19 
shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {} 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

20 
else if 0 \<le> m then {a/m + c .. b/m + c} 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

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

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

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

24 

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

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

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

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

28 
using continuous_on_open_Union [of "{s,t}"] by auto 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

29 

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

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

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

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

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

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

35 

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

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

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

38 
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

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

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

41 
by (simp add: vector_derivative_at has_vector_derivative_mult 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

42 

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

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

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

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

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

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

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

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

50 

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

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

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

53 
assumes "f differentiable at x" "(g differentiable 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

54 
shows "vector_derivative (g \<circ> 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

55 
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

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

57 

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

58 

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

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

60 

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

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

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

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

64 
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

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

66 

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

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

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

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

70 

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

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

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

73 
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

74 
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

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

76 
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

77 
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

78 

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

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

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

81 
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

82 
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

83 
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

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

85 

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

86 
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

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

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

89 
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

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

91 

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

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

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

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

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

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

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

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

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

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

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

102 

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

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

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

105 
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

106 
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

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

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

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

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

111 
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

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

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

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

115 
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

116 
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

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

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

119 

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

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

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

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

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

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

125 
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

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

127 
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

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

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

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

131 
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

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

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

134 
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

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

136 
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

137 
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

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

139 
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

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

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

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

143 
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

144 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

167 
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

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

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

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

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

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

173 

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

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

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

176 
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

177 

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

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

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

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

181 
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

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

183 
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

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

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

186 
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

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

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

189 
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

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

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

192 
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

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

194 

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

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

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

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

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

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

200 

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

201 
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

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

203 
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

204 
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

205 
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

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

207 

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

208 
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

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

210 
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

211 
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

212 
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

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

214 

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

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

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

217 
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

218 
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

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

220 
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

221 
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

222 
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

223 
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

224 
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

225 
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

226 
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

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

228 

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

229 
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

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

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

232 
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

233 
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

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

235 
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

236 
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

237 
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

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

239 
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

240 
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

241 
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

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 

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

245 
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

246 

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

247 
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

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

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

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

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

252 

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

253 
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

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

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

256 
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

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

258 
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

259 
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

260 
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

261 
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

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

263 

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

264 
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

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

266 
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

267 
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

268 

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

269 
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

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

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

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

273 
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

274 
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

275 
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

276 
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

277 
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

278 
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

279 

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

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

281 
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

282 

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

283 
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

284 
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

285 

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

286 
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

287 
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

288 

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

289 
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

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

291 
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

292 

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

293 
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

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

295 
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

296 

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

297 
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

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

299 
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

300 

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

301 
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

302 
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

303 
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

304 
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

305 
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

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

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

309 
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

310 
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

311 

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

312 

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

313 
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

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

315 
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

316 
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

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

318 

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

319 
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

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

321 
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

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

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

325 
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

326 
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

327 
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

328 

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

329 
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

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

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

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

333 
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

334 
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

335 
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

336 
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

337 
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

338 
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

339 
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

340 
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

341 
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

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

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

345 
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

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

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

349 
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

350 
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

351 

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

352 
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

353 
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

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

355 

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

356 
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

357 
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

358 
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

359 
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

360 
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

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

362 
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

363 
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

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

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

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

367 
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

368 
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

369 
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

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

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

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

373 

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

374 
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

375 
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

376 
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

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

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

379 
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

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

381 
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

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

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

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

385 
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

386 
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

387 
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

388 
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

389 
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

390 
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

391 
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

392 
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

393 
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

394 
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

395 
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

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

397 
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

398 
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

399 
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

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

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

402 
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

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

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

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

406 
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

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

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

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

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

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

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

413 
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

414 
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

415 
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

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

417 
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

418 
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

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

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

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

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

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

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

425 
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

426 
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

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

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

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

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

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

432 
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

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

434 
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

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

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

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

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

439 
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

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

441 
apply (rule_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

442 
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

443 
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

444 
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

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

446 

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

447 
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

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

449 
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

450 
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

451 

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

452 
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

453 
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

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

455 
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

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

457 
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

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

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

460 
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

461 
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

462 
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

463 
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

464 
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

465 
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

466 
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

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

468 

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

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

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

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

472 
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

473 
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

474 

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

475 
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

476 
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

477 
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

478 
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

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

480 
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

481 
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

482 
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

483 
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

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

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

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

487 
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

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

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

490 
have [simp]: "vector_derivative (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

491 
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

492 
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

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

494 
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

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

496 
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

497 
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

498 
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

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

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

501 
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

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

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

504 
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

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

506 
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

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

508 
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

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

510 
then have con_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

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

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

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

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

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

516 
apply (rule_tac x="insert 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

517 
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

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

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

520 

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

521 
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

522 
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

523 
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

524 
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

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

526 
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

527 
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

528 
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

529 
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

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

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

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

533 
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

534 
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

535 
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

536 
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

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

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

539 
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

540 
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

541 
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

542 
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

543 
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

544 
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

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

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

547 
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

548 
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

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

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

551 
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

552 
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

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

554 
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

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

556 
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

557 
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

558 
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

559 
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

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

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

562 
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

563 
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

564 
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

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

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

567 

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

568 
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

569 

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

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

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

572 

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

573 
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

574 
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

575 

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

576 
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

577 
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

578 

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

579 
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

580 

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

581 
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

582 
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

583 

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

584 
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

585 
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

586 

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

587 
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

588 
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

589 

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

590 
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

591 
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

592 

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

593 
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

594 
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

595 

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

596 

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

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

598 

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

599 
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

600 

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

601 
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

602 

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

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

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

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

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

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

608 

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

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

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

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

612 

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

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

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

615 

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

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

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

618 

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

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

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

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

622 

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

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

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

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

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

627 

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

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

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

630 

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

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

632 

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

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

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

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

636 
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

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

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

639 

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

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

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

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

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

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

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

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

647 
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

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

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

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

651 

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

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

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

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

655 
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

656 

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

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

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

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

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

661 

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

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

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

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

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

666 

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

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

668 

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

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

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

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

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

673 
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

674 
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

675 
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

676 
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

677 
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

678 
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

679 
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

680 
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

681 
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

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

683 
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

684 
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

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

686 

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

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

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

689 

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

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

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

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

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

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

695 
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

696 
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

697 
 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

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

699 
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

700 
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

701 
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

702 
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

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

704 
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

705 
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

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

707 
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

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

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

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

711 
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

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

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

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

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

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

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

718 
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

719 
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

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

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

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

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

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

725 

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

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

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

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

729 

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

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

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

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

733 

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

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

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

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

737 

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

738 

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

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

740 

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

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

742 
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

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

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

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

746 
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

747 
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

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

749 
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

750 
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

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

752 
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

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

754 
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

755 
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

756 
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

757 
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

758 
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

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

760 
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

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

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

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

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

765 

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

766 
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

767 
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

768 
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

769 
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

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

771 

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

772 
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

773 
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

774 
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

775 
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

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

777 

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

778 
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

779 
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

780 
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

781 
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

782 

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

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

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

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

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

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

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

789 
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

790 
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

791 
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

792 
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

793 
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

794 
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

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

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

797 
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

798 
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

799 
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

800 
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

801 
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

802 
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

803 
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

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

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

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

807 
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

808 
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

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

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

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

812 
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

813 
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

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

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

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

817 
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

818 
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

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

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

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

822 
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

823 
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

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

825 
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

826 
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

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

828 
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

829 
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

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

831 
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

832 
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

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

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

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

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

837 
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

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

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

840 

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

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

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

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

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

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

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

847 

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

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

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

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

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

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

853 
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

854 
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

855 
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

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

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

858 
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

859 
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

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

861 
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

862 
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

863 
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

864 
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

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

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

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

868 
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

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

870 
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

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

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

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

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

875 
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

876 
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

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

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

879 

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

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

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

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

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

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

885 
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

886 
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

887 
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

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

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

890 
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

891 
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

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

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

894 
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

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

896 
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

897 
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

898 
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

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

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

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

902 
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

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

904 
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

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

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

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

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

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

910 
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

911 
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

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

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

914 

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

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

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

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

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

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

920 

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

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

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

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

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

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

926 

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

927 

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

928 
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

929 

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

930 
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

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

932 

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

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

934 
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

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

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

937 
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

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

939 
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

940 
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

941 
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

942 
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

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

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

945 

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

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

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

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

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

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

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

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

953 
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

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

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

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

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

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

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

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

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

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

963 
have "0 \<le> x \<Longrightarrow> x + a < 1 \<Longrightarrow> x \<notin> (\<lambda>x. x  a) ` s \<Longrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

964 
vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a))" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

966 
apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist(1a) x" _ "(\<lambda>x. g(a+x))"]]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

972 
using a apply (auto simp: has_vector_derivative_def vector_derivative_works image_def add.commute) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

976 
have "1 < x + a \<Longrightarrow> x \<le> 1 \<Longrightarrow> x \<notin> (\<lambda>x. x  a + 1) ` s \<Longrightarrow> 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

977 
vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a  1))" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

979 
apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist (1a) x" _ "(\<lambda>x. g(a+x1))"]]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

985 
using a apply (auto simp: has_vector_derivative_def vector_derivative_works image_def add.commute) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

996 
[where s = "{1a} \<union> (\<lambda>x. xa) ` s" and f = "\<lambda>x. f(g(a+x)) * vector_derivative g (at(a+x))"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

1000 
using has_integral_affinity [where m=1 and c=a, simplified, OF integrable_integral [OF va1]] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1001 
apply (simp add: image_affinity_atLeastAtMost_diff [where m=1 and c=a, simplified] add.commute) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

1007 
[where s = "{1a} \<union> (\<lambda>x. xa+1) ` s" and f = "\<lambda>x. f(g(a+x1)) * vector_derivative g (at(a+x1))"]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

1011 
using has_integral_affinity [where m=1 and c="a1", simplified, OF integrable_integral [OF v0a]] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1012 
apply (simp add: image_affinity_atLeastAtMost [where m=1 and c="1a", simplified]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1013 
apply (simp add: algebra_simps) 
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 
ultimately show ?thesis 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

1019 

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

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

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

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

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

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

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

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

1027 
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

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

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

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

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

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

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

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

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

1036 
[of "{0<..<1}s" _ "(shiftpath (1  a) (shiftpath a g))"]]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

1040 
apply (rule Derivative.differentiable_transform_at [of "min x (1x)", OF _ _ gx]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

1052 
qed 
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 has_path_integral_shiftpath_eq: 
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 "(f has_path_integral i) (shiftpath a g) \<longleftrightarrow> (f has_path_integral i) g" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1058 

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

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

1060 
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

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

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

1063 

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

1064 

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

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

1066 

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

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

1068 
"(linepath a b has_vector_derivative (b  a)) (at x within s)" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

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

1072 

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

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

1074 
"x \<in> {0..1} \<Longrightarrow> vector_derivative (linepath a b) (at x within {0..1}) = b  a" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1075 
apply (rule vector_derivative_within_closed_interval [of 0 "1::real", simplified]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

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

1078 

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

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

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

1081 

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

1082 
lemma valid_path_linepath [iff]: "valid_path (linepath a b)" 
2bd401e364f9
Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents:
61104
diff
changeset

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

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

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

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

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

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

1089 

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

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

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

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

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

1094 

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

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

1096 
shows "x \<in> {0..1} \<Longrightarrow> linepath a b x \<in> closed_segment a b" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1098 

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

1099 
lemma linepath_image_01: "linepath a b ` {0..1} = closed_segment a b" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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

1101 

457abb82fb9e
the Cauchy integral theorem and related material
