--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Thu Feb 25 00:36:44 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Thu Feb 25 13:58:48 2016 +0000
@@ -197,6 +197,24 @@
subsubsection\<open>The concept of continuously differentiable\<close>
+text \<open>
+John Harrison writes as follows:
+
+``The usual assumption in complex analysis texts is that a path \<gamma> should be piecewise
+continuously differentiable, which ensures that the path integral exists at least for any continuous
+f, since all piecewise continuous functions are integrable. However, our notion of validity is
+weaker, just piecewise differentiability... [namely] continuity plus differentiability except on a
+finite set ... [Our] underlying theory of integration is the Kurzweil-Henstock theory. In contrast to
+the Riemann or Lebesgue theory (but in common with a simple notion based on antiderivatives), this
+can integrate all derivatives.''
+
+"Formalizing basic complex analysis." From Insight to Proof: Festschrift in Honour of Andrzej Trybulec.
+Studies in Logic, Grammar and Rhetoric 10.23 (2007): 151-165.
+
+And indeed he does not assume that his derivatives are continuous, but the penalty is unreasonably
+difficult proofs concerning winding numbers. We need a self-contained and straightforward theorem
+asserting that all derivatives can be integrated before we can adopt Harrison's choice.\<close>
+
definition C1_differentiable_on :: "(real \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> real set \<Rightarrow> bool"
(infix "C1'_differentiable'_on" 50)
where
@@ -549,6 +567,63 @@
lemma closed_valid_path_image: "valid_path g \<Longrightarrow> closed(path_image g)"
by (metis closed_path_image valid_path_imp_path)
+lemma valid_path_compose:
+ assumes "valid_path g"
+ and der:"\<And>x. x \<in> path_image g \<Longrightarrow> \<exists>f'. (f has_field_derivative f') (at x)"
+ and con: "continuous_on {0..1} (\<lambda>x. deriv f (g x))"
+ shows "valid_path (f o g)"
+proof -
+ obtain s where "finite s" and g_diff: "g C1_differentiable_on {0..1} - s"
+ using `valid_path g` unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
+ have "f \<circ> g differentiable at t" if "t \<in> {0..1} - s" for t
+ proof (rule differentiable_chain_at)
+ show "g differentiable at t" using `valid_path g`
+ by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - s\<close> that)
+ next
+ have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
+ then obtain f' where "(f has_field_derivative f') (at (g t))"
+ using der by auto
+ then have " (f has_derivative op * f') (at (g t))"
+ using has_field_derivative_imp_has_derivative[of f f' "at (g t)"] by auto
+ then show "f differentiable at (g t)" using differentiableI by auto
+ qed
+ moreover have "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (f \<circ> g) (at x))"
+ proof (rule continuous_on_eq [where f = "\<lambda>x. vector_derivative g (at x) * deriv f (g x)"],
+ rule continuous_intros)
+ show "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative g (at x))"
+ using g_diff C1_differentiable_on_eq by auto
+ next
+ show "continuous_on ({0..1} - s) (\<lambda>x. deriv f (g x))"
+ using con continuous_on_subset by blast
+ next
+ show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f \<circ> g) (at t)"
+ if "t \<in> {0..1} - s" for t
+ proof (rule vector_derivative_chain_at_general[symmetric])
+ show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that)
+ next
+ have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
+ then obtain f' where "(f has_field_derivative f') (at (g t))"
+ using der by auto
+ then show "\<exists>g'. (f has_field_derivative g') (at (g t))" by auto
+ qed
+ qed
+ ultimately have "f o g C1_differentiable_on {0..1} - s"
+ using C1_differentiable_on_eq by blast
+ moreover have "path (f o g)"
+ proof -
+ have "isCont f x" if "x \<in> path_image g" for x
+ proof -
+ obtain f' where "(f has_field_derivative f') (at x)"
+ using der `x\<in>path_image g` by auto
+ thus ?thesis using DERIV_isCont by auto
+ qed
+ then have "continuous_on (path_image g) f" using continuous_at_imp_continuous_on by auto
+ then show ?thesis using path_continuous_image `valid_path g` valid_path_imp_path by auto
+ qed
+ ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
+ using `finite s` by auto
+qed
+
subsection\<open>Contour Integrals along a path\<close>