src/HOL/Analysis/Cauchy_Integral_Theorem.thy
author paulson <lp15@cam.ac.uk>
Tue, 21 Feb 2017 17:12:10 +0000
changeset 65037 2cf841ff23be
parent 65036 ab7e11730ad8
child 65578 e4997c181cce
permissions -rw-r--r--
some new material, also recasting some theorems using “obtains”
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     1
section \<open>Complex path integrals and Cauchy's integral theorem\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     2
61711
21d7910d6816 Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents: 61694
diff changeset
     3
text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)\<close>
21d7910d6816 Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents: 61694
diff changeset
     4
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63589
diff changeset
     5
theory Cauchy_Integral_Theorem
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63589
diff changeset
     6
imports Complex_Transcendental Weierstrass_Theorems Ordered_Euclidean_Space
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     7
begin
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     8
62620
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
     9
subsection\<open>Homeomorphisms of arc images\<close>
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    10
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    11
lemma homeomorphism_arc:
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    12
  fixes g :: "real \<Rightarrow> 'a::t2_space"
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    13
  assumes "arc g"
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    14
  obtains h where "homeomorphism {0..1} (path_image g) g h"
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    15
using assms by (force simp add: arc_def homeomorphism_compact path_def path_image_def)
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    16
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    17
lemma homeomorphic_arc_image_interval:
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    18
  fixes g :: "real \<Rightarrow> 'a::t2_space" and a::real
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    19
  assumes "arc g" "a < b"
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    20
  shows "(path_image g) homeomorphic {a..b}"
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    21
proof -
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    22
  have "(path_image g) homeomorphic {0..1::real}"
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    23
    by (meson assms(1) homeomorphic_def homeomorphic_sym homeomorphism_arc)
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    24
  also have "... homeomorphic {a..b}"
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    25
    using assms by (force intro: homeomorphic_closed_intervals_real)
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    26
  finally show ?thesis .
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    27
qed
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    28
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    29
lemma homeomorphic_arc_images:
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    30
  fixes g :: "real \<Rightarrow> 'a::t2_space" and h :: "real \<Rightarrow> 'b::t2_space"
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    31
  assumes "arc g" "arc h"
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    32
  shows "(path_image g) homeomorphic (path_image h)"
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    33
proof -
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    34
  have "(path_image g) homeomorphic {0..1::real}"
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    35
    by (meson assms homeomorphic_def homeomorphic_sym homeomorphism_arc)
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    36
  also have "... homeomorphic (path_image h)"
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    37
    by (meson assms homeomorphic_def homeomorphism_arc)
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    38
  finally show ?thesis .
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    39
qed
d21dab28b3f9 New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents: 62618
diff changeset
    40
65037
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    41
lemma path_connected_arc_complement:
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    42
  fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    43
  assumes "arc \<gamma>" "2 \<le> DIM('a)"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    44
  shows "path_connected(- path_image \<gamma>)"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    45
proof -
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    46
  have "path_image \<gamma> homeomorphic {0..1::real}"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    47
    by (simp add: assms homeomorphic_arc_image_interval)
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    48
  then
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    49
  show ?thesis
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    50
    apply (rule path_connected_complement_homeomorphic_convex_compact)
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    51
      apply (auto simp: assms)
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    52
    done
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    53
qed
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    54
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    55
lemma connected_arc_complement:
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    56
  fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    57
  assumes "arc \<gamma>" "2 \<le> DIM('a)"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    58
  shows "connected(- path_image \<gamma>)"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    59
  by (simp add: assms path_connected_arc_complement path_connected_imp_connected)
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    60
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    61
lemma inside_arc_empty:
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    62
  fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    63
  assumes "arc \<gamma>"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    64
    shows "inside(path_image \<gamma>) = {}"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    65
proof (cases "DIM('a) = 1")
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    66
  case True
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    67
  then show ?thesis
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    68
    using assms connected_arc_image connected_convex_1_gen inside_convex by blast
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    69
next
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    70
  case False
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    71
  show ?thesis
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    72
  proof (rule inside_bounded_complement_connected_empty)
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    73
    show "connected (- path_image \<gamma>)"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    74
      apply (rule connected_arc_complement [OF assms])
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    75
      using False
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    76
      by (metis DIM_ge_Suc0 One_nat_def Suc_1 not_less_eq_eq order_class.order.antisym)
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    77
    show "bounded (path_image \<gamma>)"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    78
      by (simp add: assms bounded_arc_image)
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    79
  qed
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    80
qed
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    81
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    82
lemma inside_simple_curve_imp_closed:
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    83
  fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    84
    shows "\<lbrakk>simple_path \<gamma>; x \<in> inside(path_image \<gamma>)\<rbrakk> \<Longrightarrow> pathfinish \<gamma> = pathstart \<gamma>"
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    85
  using arc_simple_path  inside_arc_empty by blast
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    86
2cf841ff23be some new material, also recasting some theorems using “obtains”
paulson <lp15@cam.ac.uk>
parents: 65036
diff changeset
    87
    
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
    88
subsection \<open>Piecewise differentiable functions\<close>
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    89
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    90
definition piecewise_differentiable_on
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    91
           (infixr "piecewise'_differentiable'_on" 50)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    92
  where "f piecewise_differentiable_on i  \<equiv>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    93
           continuous_on i f \<and>
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
    94
           (\<exists>s. finite s \<and> (\<forall>x \<in> i - s. f differentiable (at x within i)))"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    95
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    96
lemma piecewise_differentiable_on_imp_continuous_on:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    97
    "f piecewise_differentiable_on s \<Longrightarrow> continuous_on s f"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    98
by (simp add: piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    99
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   100
lemma piecewise_differentiable_on_subset:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   101
    "f piecewise_differentiable_on s \<Longrightarrow> t \<le> s \<Longrightarrow> f piecewise_differentiable_on t"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   102
  using continuous_on_subset
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   103
  unfolding piecewise_differentiable_on_def
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   104
  apply safe
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   105
  apply (blast intro: elim: continuous_on_subset)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   106
  by (meson Diff_iff differentiable_within_subset subsetCE)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   107
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   108
lemma differentiable_on_imp_piecewise_differentiable:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   109
  fixes a:: "'a::{linorder_topology,real_normed_vector}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   110
  shows "f differentiable_on {a..b} \<Longrightarrow> f piecewise_differentiable_on {a..b}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   111
  apply (simp add: piecewise_differentiable_on_def differentiable_imp_continuous_on)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   112
  apply (rule_tac x="{a,b}" in exI, simp add: differentiable_on_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   113
  done
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   114
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   115
lemma differentiable_imp_piecewise_differentiable:
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   116
    "(\<And>x. x \<in> s \<Longrightarrow> f differentiable (at x within s))
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   117
         \<Longrightarrow> f piecewise_differentiable_on s"
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   118
by (auto simp: piecewise_differentiable_on_def differentiable_imp_continuous_on differentiable_on_def
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   119
         intro: differentiable_within_subset)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   120
61204
3e491e34a62e new lemmas and movement of lemmas into place
paulson
parents: 61200
diff changeset
   121
lemma piecewise_differentiable_const [iff]: "(\<lambda>x. z) piecewise_differentiable_on s"
3e491e34a62e new lemmas and movement of lemmas into place
paulson
parents: 61200
diff changeset
   122
  by (simp add: differentiable_imp_piecewise_differentiable)
3e491e34a62e new lemmas and movement of lemmas into place
paulson
parents: 61200
diff changeset
   123
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   124
lemma piecewise_differentiable_compose:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   125
    "\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on (f ` s);
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   126
      \<And>x. finite (s \<inter> f-`{x})\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   127
      \<Longrightarrow> (g o f) piecewise_differentiable_on s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   128
  apply (simp add: piecewise_differentiable_on_def, safe)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   129
  apply (blast intro: continuous_on_compose2)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   130
  apply (rename_tac A B)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   131
  apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f-`{x})" in exI)
65036
ab7e11730ad8 Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
paulson <lp15@cam.ac.uk>
parents: 64788
diff changeset
   132
  apply (blast intro!: differentiable_chain_within)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   133
  done
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   134
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   135
lemma piecewise_differentiable_affine:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   136
  fixes m::real
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   137
  assumes "f piecewise_differentiable_on ((\<lambda>x. m *\<^sub>R x + c) ` s)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   138
  shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_differentiable_on s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   139
proof (cases "m = 0")
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   140
  case True
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   141
  then show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   142
    unfolding o_def
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   143
    by (force intro: differentiable_imp_piecewise_differentiable differentiable_const)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   144
next
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   145
  case False
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   146
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   147
    apply (rule piecewise_differentiable_compose [OF differentiable_imp_piecewise_differentiable])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   148
    apply (rule assms derivative_intros | simp add: False vimage_def real_vector_affinity_eq)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   149
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   150
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   151
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   152
lemma piecewise_differentiable_cases:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   153
  fixes c::real
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   154
  assumes "f piecewise_differentiable_on {a..c}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   155
          "g piecewise_differentiable_on {c..b}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   156
           "a \<le> c" "c \<le> b" "f c = g c"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   157
  shows "(\<lambda>x. if x \<le> c then f x else g x) piecewise_differentiable_on {a..b}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   158
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   159
  obtain s t where st: "finite s" "finite t"
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   160
                       "\<forall>x\<in>{a..c} - s. f differentiable at x within {a..c}"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   161
                       "\<forall>x\<in>{c..b} - t. g differentiable at x within {c..b}"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   162
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   163
    by (auto simp: piecewise_differentiable_on_def)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   164
  have finabc: "finite ({a,b,c} \<union> (s \<union> t))"
61222
05d28dc76e5c isabelle update_cartouches;
wenzelm
parents: 61204
diff changeset
   165
    by (metis \<open>finite s\<close> \<open>finite t\<close> finite_Un finite_insert finite.emptyI)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   166
  have "continuous_on {a..c} f" "continuous_on {c..b} g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   167
    using assms piecewise_differentiable_on_def by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   168
  then have "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   169
    using continuous_on_cases [OF closed_real_atLeastAtMost [of a c],
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   170
                               OF closed_real_atLeastAtMost [of c b],
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   171
                               of f g "\<lambda>x. x\<le>c"]  assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   172
    by (force simp: ivl_disj_un_two_touch)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   173
  moreover
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   174
  { fix x
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   175
    assume x: "x \<in> {a..b} - ({a,b,c} \<union> (s \<union> t))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   176
    have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b}" (is "?diff_fg")
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   177
    proof (cases x c rule: le_cases)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   178
      case le show ?diff_fg
63955
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   179
      proof (rule differentiable_transform_within [where d = "dist x c" and f = f])
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   180
        have "f differentiable at x within ({a<..<c} - s)"
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   181
          apply (rule differentiable_at_withinI)
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   182
          using x le st
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   183
          by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost le st(3) x)
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   184
        moreover have "open ({a<..<c} - s)"
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   185
          by (blast intro: open_greaterThanLessThan \<open>finite s\<close> finite_imp_closed)
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   186
        ultimately show "f differentiable at x within {a..b}"
63969
f4b4fba60b1d HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
hoelzl
parents: 63955
diff changeset
   187
          using x le by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI)
63955
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   188
      qed (use x le st dist_real_def in auto)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   189
    next
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   190
      case ge show ?diff_fg
63955
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   191
      proof (rule differentiable_transform_within [where d = "dist x c" and f = g])
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   192
        have "g differentiable at x within ({c<..<b} - t)"
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   193
          apply (rule differentiable_at_withinI)
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   194
          using x ge st
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   195
          by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost)
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   196
        moreover have "open ({c<..<b} - t)"
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   197
          by (blast intro: open_greaterThanLessThan \<open>finite t\<close> finite_imp_closed)
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   198
        ultimately show "g differentiable at x within {a..b}"
63969
f4b4fba60b1d HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
hoelzl
parents: 63955
diff changeset
   199
          using x ge by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI)
63955
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   200
      qed (use x ge st dist_real_def in auto)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   201
    qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   202
  }
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   203
  then have "\<exists>s. finite s \<and>
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   204
                 (\<forall>x\<in>{a..b} - s. (\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b})"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   205
    by (meson finabc)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   206
  ultimately show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   207
    by (simp add: piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   208
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   209
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   210
lemma piecewise_differentiable_neg:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   211
    "f piecewise_differentiable_on s \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_differentiable_on s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   212
  by (auto simp: piecewise_differentiable_on_def continuous_on_minus)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   213
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   214
lemma piecewise_differentiable_add:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   215
  assumes "f piecewise_differentiable_on i"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   216
          "g piecewise_differentiable_on i"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   217
    shows "(\<lambda>x. f x + g x) piecewise_differentiable_on i"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   218
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   219
  obtain s t where st: "finite s" "finite t"
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   220
                       "\<forall>x\<in>i - s. f differentiable at x within i"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   221
                       "\<forall>x\<in>i - t. g differentiable at x within i"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   222
    using assms by (auto simp: piecewise_differentiable_on_def)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   223
  then have "finite (s \<union> t) \<and> (\<forall>x\<in>i - (s \<union> t). (\<lambda>x. f x + g x) differentiable at x within i)"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   224
    by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   225
  moreover have "continuous_on i f" "continuous_on i g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   226
    using assms piecewise_differentiable_on_def by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   227
  ultimately show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   228
    by (auto simp: piecewise_differentiable_on_def continuous_on_add)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   229
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   230
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   231
lemma piecewise_differentiable_diff:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   232
    "\<lbrakk>f piecewise_differentiable_on s;  g piecewise_differentiable_on s\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   233
     \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_differentiable_on s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   234
  unfolding diff_conv_add_uminus
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   235
  by (metis piecewise_differentiable_add piecewise_differentiable_neg)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   236
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   237
lemma continuous_on_joinpaths_D1:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   238
    "continuous_on {0..1} (g1 +++ g2) \<Longrightarrow> continuous_on {0..1} g1"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   239
  apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (op*(inverse 2))"])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   240
  apply (rule continuous_intros | simp)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   241
  apply (auto elim!: continuous_on_subset simp: joinpaths_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   242
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   243
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   244
lemma continuous_on_joinpaths_D2:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   245
    "\<lbrakk>continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> continuous_on {0..1} g2"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   246
  apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (\<lambda>x. inverse 2*x + 1/2)"])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   247
  apply (rule continuous_intros | simp)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   248
  apply (auto elim!: continuous_on_subset simp add: joinpaths_def pathfinish_def pathstart_def Ball_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   249
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   250
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   251
lemma piecewise_differentiable_D1:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   252
    "(g1 +++ g2) piecewise_differentiable_on {0..1} \<Longrightarrow> g1 piecewise_differentiable_on {0..1}"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   253
  apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D1)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   254
  apply (rule_tac x="insert 1 ((op*2)`s)" in exI)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   255
  apply simp
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   256
  apply (intro ballI)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   257
  apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   258
       in differentiable_transform_within)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   259
  apply (auto simp: dist_real_def joinpaths_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   260
  apply (rule differentiable_chain_within derivative_intros | simp)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   261
  apply (rule differentiable_subset)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   262
  apply (force simp:)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   263
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   264
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   265
lemma piecewise_differentiable_D2:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   266
    "\<lbrakk>(g1 +++ g2) piecewise_differentiable_on {0..1}; pathfinish g1 = pathstart g2\<rbrakk>
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   267
    \<Longrightarrow> g2 piecewise_differentiable_on {0..1}"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   268
  apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D2)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   269
  apply (rule_tac x="insert 0 ((\<lambda>x. 2*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
   270
  apply simp
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   271
  apply (intro ballI)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   272
  apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   273
          in differentiable_transform_within)
62390
842917225d56 more canonical names
nipkow
parents: 62379
diff changeset
   274
  apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: if_split_asm)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   275
  apply (rule differentiable_chain_within derivative_intros | simp)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   276
  apply (rule differentiable_subset)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   277
  apply (force simp: divide_simps)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   278
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   279
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   280
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   281
subsubsection\<open>The concept of continuously differentiable\<close>
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   282
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   283
text \<open>
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   284
John Harrison writes as follows:
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   285
62456
11e06f5283bc proper document source;
wenzelm
parents: 62408
diff changeset
   286
``The usual assumption in complex analysis texts is that a path \<open>\<gamma>\<close> should be piecewise
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   287
continuously differentiable, which ensures that the path integral exists at least for any continuous
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   288
f, since all piecewise continuous functions are integrable. However, our notion of validity is
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   289
weaker, just piecewise differentiability... [namely] continuity plus differentiability except on a
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   290
finite set ... [Our] underlying theory of integration is the Kurzweil-Henstock theory. In contrast to
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   291
the Riemann or Lebesgue theory (but in common with a simple notion based on antiderivatives), this
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   292
can integrate all derivatives.''
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   293
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   294
"Formalizing basic complex analysis." From Insight to Proof: Festschrift in Honour of Andrzej Trybulec.
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   295
Studies in Logic, Grammar and Rhetoric 10.23 (2007): 151-165.
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   296
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   297
And indeed he does not assume that his derivatives are continuous, but the penalty is unreasonably
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   298
difficult proofs concerning winding numbers. We need a self-contained and straightforward theorem
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   299
asserting that all derivatives can be integrated before we can adopt Harrison's choice.\<close>
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   300
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   301
definition C1_differentiable_on :: "(real \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> real set \<Rightarrow> bool"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   302
           (infix "C1'_differentiable'_on" 50)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   303
  where
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   304
  "f C1_differentiable_on s \<longleftrightarrow>
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   305
   (\<exists>D. (\<forall>x \<in> s. (f has_vector_derivative (D x)) (at x)) \<and> continuous_on s D)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   306
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   307
lemma C1_differentiable_on_eq:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   308
    "f C1_differentiable_on s \<longleftrightarrow>
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   309
     (\<forall>x \<in> s. f differentiable at x) \<and> continuous_on s (\<lambda>x. vector_derivative f (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   310
  unfolding C1_differentiable_on_def
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   311
  apply safe
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   312
  using differentiable_def has_vector_derivative_def apply blast
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   313
  apply (erule continuous_on_eq)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   314
  using vector_derivative_at apply fastforce
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   315
  using vector_derivative_works apply fastforce
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   316
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   317
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   318
lemma C1_differentiable_on_subset:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   319
  "f C1_differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   320
  unfolding C1_differentiable_on_def  continuous_on_eq_continuous_within
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   321
  by (blast intro:  continuous_within_subset)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   322
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   323
lemma C1_differentiable_compose:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   324
    "\<lbrakk>f C1_differentiable_on s; g C1_differentiable_on (f ` s);
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   325
      \<And>x. finite (s \<inter> f-`{x})\<rbrakk>
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   326
      \<Longrightarrow> (g o f) C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   327
  apply (simp add: C1_differentiable_on_eq, safe)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   328
   using differentiable_chain_at apply blast
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   329
  apply (rule continuous_on_eq [of _ "\<lambda>x. vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   330
   apply (rule Limits.continuous_on_scaleR, assumption)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   331
   apply (metis (mono_tags, lifting) continuous_on_eq continuous_at_imp_continuous_on continuous_on_compose differentiable_imp_continuous_within o_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   332
  by (simp add: vector_derivative_chain_at)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   333
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   334
lemma C1_diff_imp_diff: "f C1_differentiable_on s \<Longrightarrow> f differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   335
  by (simp add: C1_differentiable_on_eq differentiable_at_imp_differentiable_on)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   336
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   337
lemma C1_differentiable_on_ident [simp, derivative_intros]: "(\<lambda>x. x) C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   338
  by (auto simp: C1_differentiable_on_eq continuous_on_const)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   339
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   340
lemma C1_differentiable_on_const [simp, derivative_intros]: "(\<lambda>z. a) C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   341
  by (auto simp: C1_differentiable_on_eq continuous_on_const)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   342
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   343
lemma C1_differentiable_on_add [simp, derivative_intros]:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   344
  "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x + g x) C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   345
  unfolding C1_differentiable_on_eq  by (auto intro: continuous_intros)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   346
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   347
lemma C1_differentiable_on_minus [simp, derivative_intros]:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   348
  "f C1_differentiable_on s \<Longrightarrow> (\<lambda>x. - f x) C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   349
  unfolding C1_differentiable_on_eq  by (auto intro: continuous_intros)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   350
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   351
lemma C1_differentiable_on_diff [simp, derivative_intros]:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   352
  "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x - g x) C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   353
  unfolding C1_differentiable_on_eq  by (auto intro: continuous_intros)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   354
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   355
lemma C1_differentiable_on_mult [simp, derivative_intros]:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   356
  fixes f g :: "real \<Rightarrow> 'a :: real_normed_algebra"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   357
  shows "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x * g x) C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   358
  unfolding C1_differentiable_on_eq
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   359
  by (auto simp: continuous_on_add continuous_on_mult continuous_at_imp_continuous_on differentiable_imp_continuous_within)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   360
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   361
lemma C1_differentiable_on_scaleR [simp, derivative_intros]:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   362
  "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   363
  unfolding C1_differentiable_on_eq
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   364
  by (rule continuous_intros | simp add: continuous_at_imp_continuous_on differentiable_imp_continuous_within)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   365
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   366
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   367
definition piecewise_C1_differentiable_on
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   368
           (infixr "piecewise'_C1'_differentiable'_on" 50)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   369
  where "f piecewise_C1_differentiable_on i  \<equiv>
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   370
           continuous_on i f \<and>
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   371
           (\<exists>s. finite s \<and> (f C1_differentiable_on (i - s)))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   372
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   373
lemma C1_differentiable_imp_piecewise:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   374
    "f C1_differentiable_on s \<Longrightarrow> f piecewise_C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   375
  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_at_imp_continuous_on differentiable_imp_continuous_within)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   376
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   377
lemma piecewise_C1_imp_differentiable:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   378
    "f piecewise_C1_differentiable_on i \<Longrightarrow> f piecewise_differentiable_on i"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   379
  by (auto simp: piecewise_C1_differentiable_on_def piecewise_differentiable_on_def
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   380
           C1_differentiable_on_def differentiable_def has_vector_derivative_def
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   381
           intro: has_derivative_at_within)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   382
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   383
lemma piecewise_C1_differentiable_compose:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   384
    "\<lbrakk>f piecewise_C1_differentiable_on s; g piecewise_C1_differentiable_on (f ` s);
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   385
      \<And>x. finite (s \<inter> f-`{x})\<rbrakk>
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   386
      \<Longrightarrow> (g o f) piecewise_C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   387
  apply (simp add: piecewise_C1_differentiable_on_def, safe)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   388
  apply (blast intro: continuous_on_compose2)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   389
  apply (rename_tac A B)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   390
  apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f-`{x})" in exI)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   391
  apply (rule conjI, blast)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   392
  apply (rule C1_differentiable_compose)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   393
  apply (blast intro: C1_differentiable_on_subset)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   394
  apply (blast intro: C1_differentiable_on_subset)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   395
  by (simp add: Diff_Int_distrib2)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   396
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   397
lemma piecewise_C1_differentiable_on_subset:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   398
    "f piecewise_C1_differentiable_on s \<Longrightarrow> t \<le> s \<Longrightarrow> f piecewise_C1_differentiable_on t"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   399
  by (auto simp: piecewise_C1_differentiable_on_def elim!: continuous_on_subset C1_differentiable_on_subset)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   400
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   401
lemma C1_differentiable_imp_continuous_on:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   402
  "f C1_differentiable_on s \<Longrightarrow> continuous_on s f"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   403
  unfolding C1_differentiable_on_eq continuous_on_eq_continuous_within
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   404
  using differentiable_at_withinI differentiable_imp_continuous_within by blast
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   405
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   406
lemma C1_differentiable_on_empty [iff]: "f C1_differentiable_on {}"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   407
  unfolding C1_differentiable_on_def
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   408
  by auto
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   409
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   410
lemma piecewise_C1_differentiable_affine:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   411
  fixes m::real
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   412
  assumes "f piecewise_C1_differentiable_on ((\<lambda>x. m * x + c) ` s)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   413
  shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   414
proof (cases "m = 0")
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   415
  case True
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   416
  then show ?thesis
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   417
    unfolding o_def by (auto simp: piecewise_C1_differentiable_on_def continuous_on_const)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   418
next
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   419
  case False
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   420
  show ?thesis
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   421
    apply (rule piecewise_C1_differentiable_compose [OF C1_differentiable_imp_piecewise])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   422
    apply (rule assms derivative_intros | simp add: False vimage_def)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   423
    using real_vector_affinity_eq [OF False, where c=c, unfolded scaleR_conv_of_real]
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   424
    apply simp
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   425
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   426
qed
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   427
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   428
lemma piecewise_C1_differentiable_cases:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   429
  fixes c::real
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   430
  assumes "f piecewise_C1_differentiable_on {a..c}"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   431
          "g piecewise_C1_differentiable_on {c..b}"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   432
           "a \<le> c" "c \<le> b" "f c = g c"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   433
  shows "(\<lambda>x. if x \<le> c then f x else g x) piecewise_C1_differentiable_on {a..b}"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   434
proof -
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   435
  obtain s t where st: "f C1_differentiable_on ({a..c} - s)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   436
                       "g C1_differentiable_on ({c..b} - t)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   437
                       "finite s" "finite t"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   438
    using assms
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   439
    by (force simp: piecewise_C1_differentiable_on_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   440
  then have f_diff: "f differentiable_on {a..<c} - s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   441
        and g_diff: "g differentiable_on {c<..b} - t"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   442
    by (simp_all add: C1_differentiable_on_eq differentiable_at_withinI differentiable_on_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   443
  have "continuous_on {a..c} f" "continuous_on {c..b} g"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   444
    using assms piecewise_C1_differentiable_on_def by auto
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   445
  then have cab: "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   446
    using continuous_on_cases [OF closed_real_atLeastAtMost [of a c],
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   447
                               OF closed_real_atLeastAtMost [of c b],
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   448
                               of f g "\<lambda>x. x\<le>c"]  assms
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   449
    by (force simp: ivl_disj_un_two_touch)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   450
  { fix x
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   451
    assume x: "x \<in> {a..b} - insert c (s \<union> t)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   452
    have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x" (is "?diff_fg")
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   453
    proof (cases x c rule: le_cases)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   454
      case le show ?diff_fg
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   455
        apply (rule differentiable_transform_within [where f=f and d = "dist x c"])
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   456
        using x dist_real_def le st by (auto simp: C1_differentiable_on_eq)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   457
    next
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   458
      case ge show ?diff_fg
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   459
        apply (rule differentiable_transform_within [where f=g and d = "dist x c"])
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   460
        using dist_nz x dist_real_def ge st x by (auto simp: C1_differentiable_on_eq)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   461
    qed
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   462
  }
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   463
  then have "(\<forall>x \<in> {a..b} - insert c (s \<union> t). (\<lambda>x. if x \<le> c then f x else g x) differentiable at x)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   464
    by auto
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   465
  moreover
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   466
  { assume fcon: "continuous_on ({a<..<c} - s) (\<lambda>x. vector_derivative f (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   467
       and gcon: "continuous_on ({c<..<b} - t) (\<lambda>x. vector_derivative g (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   468
    have "open ({a<..<c} - s)"  "open ({c<..<b} - t)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   469
      using st by (simp_all add: open_Diff finite_imp_closed)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   470
    moreover have "continuous_on ({a<..<c} - s) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   471
      apply (rule continuous_on_eq [OF fcon])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   472
      apply (simp add:)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   473
      apply (rule vector_derivative_at [symmetric])
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   474
      apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_within)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   475
      apply (simp_all add: dist_norm vector_derivative_works [symmetric])
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   476
      apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff linorder_not_le order_less_irrefl st(1))
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   477
      apply auto
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   478
      done
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   479
    moreover have "continuous_on ({c<..<b} - t) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   480
      apply (rule continuous_on_eq [OF gcon])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   481
      apply (simp add:)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   482
      apply (rule vector_derivative_at [symmetric])
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   483
      apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_within)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   484
      apply (simp_all add: dist_norm vector_derivative_works [symmetric])
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   485
      apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff less_irrefl not_le st(2))
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   486
      apply auto
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   487
      done
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   488
    ultimately have "continuous_on ({a<..<b} - insert c (s \<union> t))
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   489
        (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   490
      apply (rule continuous_on_subset [OF continuous_on_open_Un], auto)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   491
      done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   492
  } note * = this
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   493
  have "continuous_on ({a<..<b} - insert c (s \<union> t)) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   494
    using st
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   495
    by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset intro: *)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   496
  ultimately have "\<exists>s. finite s \<and> ((\<lambda>x. if x \<le> c then f x else g x) C1_differentiable_on {a..b} - s)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   497
    apply (rule_tac x="{a,b,c} \<union> s \<union> t" in exI)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   498
    using st  by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   499
  with cab show ?thesis
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   500
    by (simp add: piecewise_C1_differentiable_on_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   501
qed
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   502
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   503
lemma piecewise_C1_differentiable_neg:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   504
    "f piecewise_C1_differentiable_on s \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   505
  unfolding piecewise_C1_differentiable_on_def
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   506
  by (auto intro!: continuous_on_minus C1_differentiable_on_minus)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   507
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   508
lemma piecewise_C1_differentiable_add:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   509
  assumes "f piecewise_C1_differentiable_on i"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   510
          "g piecewise_C1_differentiable_on i"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   511
    shows "(\<lambda>x. f x + g x) piecewise_C1_differentiable_on i"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   512
proof -
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   513
  obtain s t where st: "finite s" "finite t"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   514
                       "f C1_differentiable_on (i-s)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   515
                       "g C1_differentiable_on (i-t)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   516
    using assms by (auto simp: piecewise_C1_differentiable_on_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   517
  then have "finite (s \<union> t) \<and> (\<lambda>x. f x + g x) C1_differentiable_on i - (s \<union> t)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   518
    by (auto intro: C1_differentiable_on_add elim!: C1_differentiable_on_subset)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   519
  moreover have "continuous_on i f" "continuous_on i g"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   520
    using assms piecewise_C1_differentiable_on_def by auto
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   521
  ultimately show ?thesis
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   522
    by (auto simp: piecewise_C1_differentiable_on_def continuous_on_add)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   523
qed
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   524
61204
3e491e34a62e new lemmas and movement of lemmas into place
paulson
parents: 61200
diff changeset
   525
lemma piecewise_C1_differentiable_diff:
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   526
    "\<lbrakk>f piecewise_C1_differentiable_on s;  g piecewise_C1_differentiable_on s\<rbrakk>
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   527
     \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_C1_differentiable_on s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   528
  unfolding diff_conv_add_uminus
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   529
  by (metis piecewise_C1_differentiable_add piecewise_C1_differentiable_neg)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   530
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   531
lemma piecewise_C1_differentiable_D1:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   532
  fixes g1 :: "real \<Rightarrow> 'a::real_normed_field"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   533
  assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   534
    shows "g1 piecewise_C1_differentiable_on {0..1}"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   535
proof -
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   536
  obtain s where "finite s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   537
             and co12: "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   538
             and g12D: "\<forall>x\<in>{0..1} - s. g1 +++ g2 differentiable at x"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   539
    using assms  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   540
  then have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (op * 2 ` s)" for x
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   541
    apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_within)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   542
    using that
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   543
    apply (simp_all add: dist_real_def joinpaths_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   544
    apply (rule differentiable_chain_at derivative_intros | force)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   545
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   546
  have [simp]: "vector_derivative (g1 \<circ> op * 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   547
               if "x \<in> {0..1} - insert 1 (op * 2 ` s)" for x
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   548
    apply (subst vector_derivative_chain_at)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   549
    using that
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   550
    apply (rule derivative_eq_intros g1D | simp)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   551
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   552
  have "continuous_on ({0..1/2} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   553
    using co12 by (rule continuous_on_subset) force
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   554
  then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 o op*2) (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   555
    apply (rule continuous_on_eq [OF _ vector_derivative_at])
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   556
    apply (rule_tac f="g1 o op*2" and d="dist x (1/2)" in has_vector_derivative_transform_within)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   557
    apply (simp_all add: dist_norm joinpaths_def vector_derivative_works [symmetric])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   558
    apply (force intro: g1D differentiable_chain_at)
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   559
    apply auto
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   560
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   561
  have "continuous_on ({0..1} - insert 1 (op * 2 ` s))
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   562
                      ((\<lambda>x. 1/2 * vector_derivative (g1 o op*2) (at x)) o op*(1/2))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   563
    apply (rule continuous_intros)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   564
    using coDhalf
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   565
    apply (simp add: scaleR_conv_of_real image_set_diff image_image)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   566
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   567
  then have con_g1: "continuous_on ({0..1} - insert 1 (op * 2 ` s)) (\<lambda>x. vector_derivative g1 (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   568
    by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   569
  have "continuous_on {0..1} g1"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   570
    using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast
61222
05d28dc76e5c isabelle update_cartouches;
wenzelm
parents: 61204
diff changeset
   571
  with \<open>finite s\<close> show ?thesis
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   572
    apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   573
    apply (rule_tac x="insert 1 ((op*2)`s)" in exI)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   574
    apply (simp add: g1D con_g1)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   575
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   576
qed
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   577
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   578
lemma piecewise_C1_differentiable_D2:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   579
  fixes g2 :: "real \<Rightarrow> 'a::real_normed_field"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   580
  assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" "pathfinish g1 = pathstart g2"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   581
    shows "g2 piecewise_C1_differentiable_on {0..1}"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   582
proof -
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   583
  obtain s where "finite s"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   584
             and co12: "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   585
             and g12D: "\<forall>x\<in>{0..1} - s. g1 +++ g2 differentiable at x"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   586
    using assms  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   587
  then have g2D: "g2 differentiable at x" if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)" for x
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   588
    apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_within)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   589
    using that
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   590
    apply (simp_all add: dist_real_def joinpaths_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   591
    apply (auto simp: dist_real_def joinpaths_def field_simps)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   592
    apply (rule differentiable_chain_at derivative_intros | force)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   593
    apply (drule_tac x= "(x + 1) / 2" in bspec, force simp: divide_simps)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   594
    apply assumption
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   595
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   596
  have [simp]: "vector_derivative (g2 \<circ> (\<lambda>x. 2*x-1)) (at ((x+1)/2)) = 2 *\<^sub>R vector_derivative g2 (at x)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   597
               if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)" for x
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   598
    using that  by (auto simp: vector_derivative_chain_at divide_simps g2D)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   599
  have "continuous_on ({1/2..1} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   600
    using co12 by (rule continuous_on_subset) force
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   601
  then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) s) (\<lambda>x. vector_derivative (g2 o (\<lambda>x. 2*x-1)) (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   602
    apply (rule continuous_on_eq [OF _ vector_derivative_at])
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   603
    apply (rule_tac f="g2 o (\<lambda>x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_within)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   604
    apply (auto simp: dist_real_def field_simps joinpaths_def vector_derivative_works [symmetric]
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   605
                intro!: g2D differentiable_chain_at)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   606
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   607
  have [simp]: "((\<lambda>x. (x + 1) / 2) ` ({0..1} - insert 0 ((\<lambda>x. 2 * x - 1) ` s))) = ({1/2..1} - insert (1/2) s)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   608
    apply (simp add: image_set_diff inj_on_def image_image)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   609
    apply (auto simp: image_affinity_atLeastAtMost_div add_divide_distrib)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   610
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   611
  have "continuous_on ({0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s))
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   612
                      ((\<lambda>x. 1/2 * vector_derivative (g2 \<circ> (\<lambda>x. 2*x-1)) (at x)) o (\<lambda>x. (x+1)/2))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   613
    by (rule continuous_intros | simp add:  coDhalf)+
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   614
  then have con_g2: "continuous_on ({0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)) (\<lambda>x. vector_derivative g2 (at x))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   615
    by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   616
  have "continuous_on {0..1} g2"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   617
    using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast
61222
05d28dc76e5c isabelle update_cartouches;
wenzelm
parents: 61204
diff changeset
   618
  with \<open>finite s\<close> show ?thesis
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   619
    apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   620
    apply (rule_tac x="insert 0 ((\<lambda>x. 2 * x - 1) ` s)" in exI)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   621
    apply (simp add: g2D con_g2)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   622
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   623
qed
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   624
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   625
subsection \<open>Valid paths, and their start and finish\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   626
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   627
definition valid_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool"
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   628
  where "valid_path f \<equiv> f piecewise_C1_differentiable_on {0..1::real}"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   629
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   630
definition closed_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   631
  where "closed_path g \<equiv> g 0 = g 1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   632
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   633
subsubsection\<open>In particular, all results for paths apply\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   634
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   635
lemma valid_path_imp_path: "valid_path g \<Longrightarrow> path g"
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   636
by (simp add: path_def piecewise_C1_differentiable_on_def valid_path_def)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   637
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   638
lemma connected_valid_path_image: "valid_path g \<Longrightarrow> connected(path_image g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   639
  by (metis connected_path_image valid_path_imp_path)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   640
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   641
lemma compact_valid_path_image: "valid_path g \<Longrightarrow> compact(path_image g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   642
  by (metis compact_path_image valid_path_imp_path)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   643
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   644
lemma bounded_valid_path_image: "valid_path g \<Longrightarrow> bounded(path_image g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   645
  by (metis bounded_path_image valid_path_imp_path)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   646
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   647
lemma closed_valid_path_image: "valid_path g \<Longrightarrow> closed(path_image g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   648
  by (metis closed_path_image valid_path_imp_path)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   649
62540
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   650
proposition valid_path_compose:
62623
dbc62f86a1a9 rationalisation of theorem names esp about "real Archimedian" etc.
paulson <lp15@cam.ac.uk>
parents: 62620
diff changeset
   651
  assumes "valid_path g"
64394
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   652
      and der: "\<And>x. x \<in> path_image g \<Longrightarrow> f field_differentiable (at x)"
62540
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   653
      and con: "continuous_on (path_image g) (deriv f)"
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   654
    shows "valid_path (f o g)"
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   655
proof -
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   656
  obtain s where "finite s" and g_diff: "g C1_differentiable_on {0..1} - s"
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62626
diff changeset
   657
    using \<open>valid_path g\<close> unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
62540
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   658
  have "f \<circ> g differentiable at t" when "t\<in>{0..1} - s" for t
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   659
    proof (rule differentiable_chain_at)
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62626
diff changeset
   660
      show "g differentiable at t" using \<open>valid_path g\<close>
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   661
        by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - s\<close> that)
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   662
    next
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   663
      have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
64394
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   664
      then show "f differentiable at (g t)" 
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   665
        using der[THEN field_differentiable_imp_differentiable] by auto
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   666
    qed
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   667
  moreover have "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (f \<circ> g) (at x))"
62540
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   668
    proof (rule continuous_on_eq [where f = "\<lambda>x. vector_derivative g (at x) * deriv f (g x)"],
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   669
        rule continuous_intros)
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   670
      show "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative g (at x))"
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   671
        using g_diff C1_differentiable_on_eq by auto
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   672
    next
62623
dbc62f86a1a9 rationalisation of theorem names esp about "real Archimedian" etc.
paulson <lp15@cam.ac.uk>
parents: 62620
diff changeset
   673
      have "continuous_on {0..1} (\<lambda>x. deriv f (g x))"
dbc62f86a1a9 rationalisation of theorem names esp about "real Archimedian" etc.
paulson <lp15@cam.ac.uk>
parents: 62620
diff changeset
   674
        using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def]
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62626
diff changeset
   675
          \<open>valid_path g\<close> piecewise_C1_differentiable_on_def valid_path_def
62540
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   676
        by blast
62623
dbc62f86a1a9 rationalisation of theorem names esp about "real Archimedian" etc.
paulson <lp15@cam.ac.uk>
parents: 62620
diff changeset
   677
      then show "continuous_on ({0..1} - s) (\<lambda>x. deriv f (g x))"
62540
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   678
        using continuous_on_subset by blast
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   679
    next
62540
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   680
      show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f \<circ> g) (at t)"
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   681
          when "t \<in> {0..1} - s" for t
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   682
        proof (rule vector_derivative_chain_at_general[symmetric])
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   683
          show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that)
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   684
        next
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   685
          have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
64394
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   686
          then show "f field_differentiable at (g t)" using der by auto
62540
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   687
        qed
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   688
    qed
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   689
  ultimately have "f o g C1_differentiable_on {0..1} - s"
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   690
    using C1_differentiable_on_eq by blast
64394
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   691
  moreover have "path (f \<circ> g)" 
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   692
    apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]])
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   693
    using der
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   694
    by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   695
  ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62626
diff changeset
   696
    using \<open>finite s\<close> by auto
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   697
qed
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62398
diff changeset
   698
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   699
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   700
subsection\<open>Contour Integrals along a path\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   701
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   702
text\<open>This definition is for complex numbers only, and does not generalise to line integrals in a vector field\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   703
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   704
text\<open>piecewise differentiable function on [0,1]\<close>
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   705
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   706
definition has_contour_integral :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool"
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   707
           (infixr "has'_contour'_integral" 50)
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   708
  where "(f has_contour_integral i) g \<equiv>
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   709
           ((\<lambda>x. f(g x) * vector_derivative g (at x within {0..1}))
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   710
            has_integral i) {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   711
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   712
definition contour_integrable_on
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   713
           (infixr "contour'_integrable'_on" 50)
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   714
  where "f contour_integrable_on g \<equiv> \<exists>i. (f has_contour_integral i) g"
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   715
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   716
definition contour_integral
62463
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   717
  where "contour_integral g f \<equiv> @i. (f has_contour_integral i) g \<or> ~ f contour_integrable_on g \<and> i=0"
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   718
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   719
lemma not_integrable_contour_integral: "~ f contour_integrable_on g \<Longrightarrow> contour_integral g f = 0"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   720
  unfolding contour_integrable_on_def contour_integral_def by blast
62463
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   721
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   722
lemma contour_integral_unique: "(f has_contour_integral i) g \<Longrightarrow> contour_integral g f = i"
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   723
  apply (simp add: contour_integral_def has_contour_integral_def contour_integrable_on_def)
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   724
  using has_integral_unique by blast
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   725
62131
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62101
diff changeset
   726
corollary has_contour_integral_eqpath:
62397
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62379
diff changeset
   727
     "\<lbrakk>(f has_contour_integral y) p; f contour_integrable_on \<gamma>;
62131
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62101
diff changeset
   728
       contour_integral p f = contour_integral \<gamma> f\<rbrakk>
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62101
diff changeset
   729
      \<Longrightarrow> (f has_contour_integral y) \<gamma>"
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62101
diff changeset
   730
using contour_integrable_on_def contour_integral_unique by auto
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62101
diff changeset
   731
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   732
lemma has_contour_integral_integral:
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   733
    "f contour_integrable_on i \<Longrightarrow> (f has_contour_integral (contour_integral i f)) i"
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   734
  by (metis contour_integral_unique contour_integrable_on_def)
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   735
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   736
lemma has_contour_integral_unique:
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   737
    "(f has_contour_integral i) g \<Longrightarrow> (f has_contour_integral j) g \<Longrightarrow> i = j"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   738
  using has_integral_unique
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   739
  by (auto simp: has_contour_integral_def)
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   740
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   741
lemma has_contour_integral_integrable: "(f has_contour_integral i) g \<Longrightarrow> f contour_integrable_on g"
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   742
  using contour_integrable_on_def by blast
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   743
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   744
(* Show that we can forget about the localized derivative.*)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   745
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   746
lemma vector_derivative_within_interior:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   747
     "\<lbrakk>x \<in> interior s; NO_MATCH UNIV s\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   748
      \<Longrightarrow> vector_derivative f (at x within s) = vector_derivative f (at x)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   749
  apply (simp add: vector_derivative_def has_vector_derivative_def has_derivative_def netlimit_within_interior)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   750
  apply (subst lim_within_interior, auto)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   751
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   752
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   753
lemma has_integral_localized_vector_derivative:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   754
    "((\<lambda>x. f (g x) * vector_derivative g (at x within {a..b})) has_integral i) {a..b} \<longleftrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   755
     ((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {a..b}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   756
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   757
  have "{a..b} - {a,b} = interior {a..b}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   758
    by (simp add: atLeastAtMost_diff_ends)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   759
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   760
    apply (rule has_integral_spike_eq [of "{a,b}"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   761
    apply (auto simp: vector_derivative_within_interior)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   762
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   763
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   764
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   765
lemma integrable_on_localized_vector_derivative:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   766
    "(\<lambda>x. f (g x) * vector_derivative g (at x within {a..b})) integrable_on {a..b} \<longleftrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   767
     (\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on {a..b}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   768
  by (simp add: integrable_on_def has_integral_localized_vector_derivative)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   769
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   770
lemma has_contour_integral:
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   771
     "(f has_contour_integral i) g \<longleftrightarrow>
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   772
      ((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}"
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   773
  by (simp add: has_integral_localized_vector_derivative has_contour_integral_def)
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   774
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   775
lemma contour_integrable_on:
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   776
     "f contour_integrable_on g \<longleftrightarrow>
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   777
      (\<lambda>t. f(g t) * vector_derivative g (at t)) integrable_on {0..1}"
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   778
  by (simp add: has_contour_integral integrable_on_def contour_integrable_on_def)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   779
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   780
subsection\<open>Reversing a path\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   781
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   782
lemma valid_path_imp_reverse:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   783
  assumes "valid_path g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   784
    shows "valid_path(reversepath g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   785
proof -
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   786
  obtain s where "finite s" "g C1_differentiable_on ({0..1} - s)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   787
    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   788
  then have "finite (op - 1 ` s)" "(reversepath g C1_differentiable_on ({0..1} - op - 1 ` s))"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   789
    apply (auto simp: reversepath_def)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   790
    apply (rule C1_differentiable_compose [of "\<lambda>x::real. 1-x" _ g, unfolded o_def])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   791
    apply (auto simp: C1_differentiable_on_eq)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   792
    apply (rule continuous_intros, force)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   793
    apply (force elim!: continuous_on_subset)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   794
    apply (simp add: finite_vimageI inj_on_def)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   795
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   796
  then show ?thesis using assms
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   797
    by (auto simp: valid_path_def piecewise_C1_differentiable_on_def path_def [symmetric])
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   798
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   799
62540
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   800
lemma valid_path_reversepath [simp]: "valid_path(reversepath g) \<longleftrightarrow> valid_path g"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   801
  using valid_path_imp_reverse by force
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   802
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   803
lemma has_contour_integral_reversepath:
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   804
  assumes "valid_path g" "(f has_contour_integral i) g"
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   805
    shows "(f has_contour_integral (-i)) (reversepath g)"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   806
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   807
  { fix s x
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   808
    assume xs: "g C1_differentiable_on ({0..1} - s)" "x \<notin> op - 1 ` s" "0 \<le> x" "x \<le> 1"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   809
      have "vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) =
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   810
            - vector_derivative g (at (1 - x) within {0..1})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   811
      proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   812
        obtain f' where f': "(g has_vector_derivative f') (at (1 - x))"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   813
          using xs
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   814
          by (force simp: has_vector_derivative_def C1_differentiable_on_def)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   815
        have "(g o (\<lambda>x. 1 - x) has_vector_derivative -1 *\<^sub>R f') (at x)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   816
          apply (rule vector_diff_chain_within)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   817
          apply (intro vector_diff_chain_within derivative_eq_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   818
          apply (rule has_vector_derivative_at_within [OF f'])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   819
          done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   820
        then have mf': "((\<lambda>x. g (1 - x)) has_vector_derivative -f') (at x)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   821
          by (simp add: o_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   822
        show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   823
          using xs
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   824
          by (auto simp: vector_derivative_at_within_ivl [OF mf'] vector_derivative_at_within_ivl [OF f'])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   825
      qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   826
  } note * = this
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   827
  have 01: "{0..1::real} = cbox 0 1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   828
    by simp
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   829
  show ?thesis using assms
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   830
    apply (auto simp: has_contour_integral_def)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   831
    apply (drule has_integral_affinity01 [where m= "-1" and c=1])
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   832
    apply (auto simp: reversepath_def valid_path_def piecewise_C1_differentiable_on_def)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   833
    apply (drule has_integral_neg)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   834
    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
   835
    apply (auto simp: *)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   836
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   837
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   838
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   839
lemma contour_integrable_reversepath:
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   840
    "valid_path g \<Longrightarrow> f contour_integrable_on g \<Longrightarrow> f contour_integrable_on (reversepath g)"
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   841
  using has_contour_integral_reversepath contour_integrable_on_def by blast
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   842
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   843
lemma contour_integrable_reversepath_eq:
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   844
    "valid_path g \<Longrightarrow> (f contour_integrable_on (reversepath g) \<longleftrightarrow> f contour_integrable_on g)"
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   845
  using contour_integrable_reversepath valid_path_reversepath by fastforce
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   846
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   847
lemma contour_integral_reversepath:
62463
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   848
  assumes "valid_path g"
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   849
    shows "contour_integral (reversepath g) f = - (contour_integral g f)"
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   850
proof (cases "f contour_integrable_on g")
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   851
  case True then show ?thesis
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   852
    by (simp add: assms contour_integral_unique has_contour_integral_integral has_contour_integral_reversepath)
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   853
next
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   854
  case False then have "~ f contour_integrable_on (reversepath g)"
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   855
    by (simp add: assms contour_integrable_reversepath_eq)
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   856
  with False show ?thesis by (simp add: not_integrable_contour_integral)
547c5c6e66d4 the integral is 0 when otherwise it would be undefined (also for contour integrals)
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   857
qed
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   858
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   859
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   860
subsection\<open>Joining two paths together\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   861
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   862
lemma valid_path_join:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   863
  assumes "valid_path g1" "valid_path g2" "pathfinish g1 = pathstart g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   864
    shows "valid_path(g1 +++ g2)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   865
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   866
  have "g1 1 = g2 0"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   867
    using assms by (auto simp: pathfinish_def pathstart_def)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   868
  moreover have "(g1 o (\<lambda>x. 2*x)) piecewise_C1_differentiable_on {0..1/2}"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   869
    apply (rule piecewise_C1_differentiable_compose)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   870
    using assms
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   871
    apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   872
    apply (rule continuous_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   873
    apply (force intro: finite_vimageI [where h = "op*2"] inj_onI)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   874
    done
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   875
  moreover have "(g2 o (\<lambda>x. 2*x-1)) piecewise_C1_differentiable_on {1/2..1}"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   876
    apply (rule piecewise_C1_differentiable_compose)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   877
    using assms unfolding valid_path_def piecewise_C1_differentiable_on_def
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   878
    by (auto intro!: continuous_intros finite_vimageI [where h = "(\<lambda>x. 2*x - 1)"] inj_onI
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   879
             simp: image_affinity_atLeastAtMost_diff continuous_on_joinpaths)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   880
  ultimately show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   881
    apply (simp only: valid_path_def continuous_on_joinpaths joinpaths_def)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   882
    apply (rule piecewise_C1_differentiable_cases)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   883
    apply (auto simp: o_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   884
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   885
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   886
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   887
lemma valid_path_join_D1:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   888
  fixes g1 :: "real \<Rightarrow> 'a::real_normed_field"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   889
  shows "valid_path (g1 +++ g2) \<Longrightarrow> valid_path g1"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   890
  unfolding valid_path_def
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   891
  by (rule piecewise_C1_differentiable_D1)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   892
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   893
lemma valid_path_join_D2:
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   894
  fixes g2 :: "real \<Rightarrow> 'a::real_normed_field"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   895
  shows "\<lbrakk>valid_path (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> valid_path g2"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   896
  unfolding valid_path_def
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   897
  by (rule piecewise_C1_differentiable_D2)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   898
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   899
lemma valid_path_join_eq [simp]:
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   900
  fixes g2 :: "real \<Rightarrow> 'a::real_normed_field"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   901
  shows "pathfinish g1 = pathstart g2 \<Longrightarrow> (valid_path(g1 +++ g2) \<longleftrightarrow> valid_path g1 \<and> valid_path g2)"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   902
  using valid_path_join_D1 valid_path_join_D2 valid_path_join by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   903
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   904
lemma has_contour_integral_join:
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   905
  assumes "(f has_contour_integral i1) g1" "(f has_contour_integral i2) g2"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   906
          "valid_path g1" "valid_path g2"
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   907
    shows "(f has_contour_integral (i1 + i2)) (g1 +++ g2)"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   908
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   909
  obtain s1 s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   910
    where s1: "finite s1" "\<forall>x\<in>{0..1} - s1. g1 differentiable at x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   911
      and s2: "finite s2" "\<forall>x\<in>{0..1} - s2. g2 differentiable at x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   912
    using assms
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   913
    by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   914
  have 1: "((\<lambda>x. f (g1 x) * vector_derivative g1 (at x)) has_integral i1) {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   915
   and 2: "((\<lambda>x. f (g2 x) * vector_derivative g2 (at x)) has_integral i2) {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   916
    using assms
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   917
    by (auto simp: has_contour_integral)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   918
  have i1: "((\<lambda>x. (2*f (g1 (2*x))) * vector_derivative g1 (at (2*x))) has_integral i1) {0..1/2}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   919
   and i2: "((\<lambda>x. (2*f (g2 (2*x - 1))) * vector_derivative g2 (at (2*x - 1))) has_integral i2) {1/2..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   920
    using has_integral_affinity01 [OF 1, where m= 2 and c=0, THEN has_integral_cmul [where c=2]]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   921
          has_integral_affinity01 [OF 2, where m= 2 and c="-1", THEN has_integral_cmul [where c=2]]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   922
    by (simp_all only: image_affinity_atLeastAtMost_div_diff, simp_all add: scaleR_conv_of_real mult_ac)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   923
  have g1: "\<lbrakk>0 \<le> z; z*2 < 1; z*2 \<notin> s1\<rbrakk> \<Longrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   924
            vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   925
            2 *\<^sub>R vector_derivative g1 (at (z*2))" for z
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   926
    apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g1(2*x))" and d = "\<bar>z - 1/2\<bar>"]])
62390
842917225d56 more canonical names
nipkow
parents: 62379
diff changeset
   927
    apply (simp_all add: dist_real_def abs_if split: if_split_asm)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   928
    apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x" 2 _ g1, simplified o_def])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   929
    apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   930
    using s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   931
    apply (auto simp: algebra_simps vector_derivative_works)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   932
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   933
  have g2: "\<lbrakk>1 < z*2; z \<le> 1; z*2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   934
            vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   935
            2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))" for z
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   936
    apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g2 (2*x - 1))" and d = "\<bar>z - 1/2\<bar>"]])
62390
842917225d56 more canonical names
nipkow
parents: 62379
diff changeset
   937
    apply (simp_all add: dist_real_def abs_if split: if_split_asm)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   938
    apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x - 1" 2 _ g2, simplified o_def])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   939
    apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   940
    using s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   941
    apply (auto simp: algebra_simps vector_derivative_works)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   942
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   943
  have "((\<lambda>x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i1) {0..1/2}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   944
    apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) (op*2 -` s1)"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   945
    using s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   946
    apply (force intro: finite_vimageI [where h = "op*2"] inj_onI)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   947
    apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g1)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   948
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   949
  moreover have "((\<lambda>x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i2) {1/2..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   950
    apply (rule has_integral_spike_finite [OF _ _ i2, of "insert (1/2) ((\<lambda>x. 2*x-1) -` s2)"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   951
    using s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   952
    apply (force intro: finite_vimageI [where h = "\<lambda>x. 2*x-1"] inj_onI)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   953
    apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g2)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   954
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   955
  ultimately
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   956
  show ?thesis
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   957
    apply (simp add: has_contour_integral)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   958
    apply (rule has_integral_combine [where c = "1/2"], auto)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   959
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   960
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   961
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   962
lemma contour_integrable_joinI:
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   963
  assumes "f contour_integrable_on g1" "f contour_integrable_on g2"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   964
          "valid_path g1" "valid_path g2"
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   965
    shows "f contour_integrable_on (g1 +++ g2)"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   966
  using assms
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   967
  by (meson has_contour_integral_join contour_integrable_on_def)
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   968
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   969
lemma contour_integrable_joinD1:
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   970
  assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g1"
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   971
    shows "f contour_integrable_on g1"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   972
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   973
  obtain s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   974
    where s1: "finite s1" "\<forall>x\<in>{0..1} - s1. g1 differentiable at x"
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   975
    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   976
  have "(\<lambda>x. f ((g1 +++ g2) (x/2)) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   977
    using assms
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   978
    apply (auto simp: contour_integrable_on)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   979
    apply (drule integrable_on_subcbox [where a=0 and b="1/2"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   980
    apply (auto intro: integrable_affinity [of _ 0 "1/2::real" "1/2" 0, simplified])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   981
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   982
  then have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2))/2) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}"
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   983
    by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   984
  have g1: "\<lbrakk>0 < z; z < 1; z \<notin> s1\<rbrakk> \<Longrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   985
            vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) =
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   986
            2 *\<^sub>R vector_derivative g1 (at z)"  for z
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
   987
    apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g1(2*x))" and d = "\<bar>(z-1)/2\<bar>"]])
62390
842917225d56 more canonical names
nipkow
parents: 62379
diff changeset
   988
    apply (simp_all add: field_simps dist_real_def abs_if split: if_split_asm)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   989
    apply (rule vector_diff_chain_at [of "\<lambda>x. x*2" 2 _ g1, simplified o_def])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   990
    using s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   991
    apply (auto simp: vector_derivative_works has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   992
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   993
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   994
    using s1
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
   995
    apply (auto simp: contour_integrable_on)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   996
    apply (rule integrable_spike_finite [of "{0,1} \<union> s1", OF _ _ *])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   997
    apply (auto simp: joinpaths_def scaleR_conv_of_real g1)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   998
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   999
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1000
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1001
lemma contour_integrable_joinD2:
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1002
  assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g2"
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1003
    shows "f contour_integrable_on g2"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1004
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1005
  obtain s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1006
    where s2: "finite s2" "\<forall>x\<in>{0..1} - s2. g2 differentiable at x"
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1007
    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1008
  have "(\<lambda>x. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1009
    using assms
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1010
    apply (auto simp: contour_integrable_on)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1011
    apply (drule integrable_on_subcbox [where a="1/2" and b=1], auto)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1012
    apply (drule integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2", simplified])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1013
    apply (simp add: image_affinity_atLeastAtMost_diff)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1014
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1015
  then have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2 + 1/2))/2) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2)))
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1016
                integrable_on {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1017
    by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1018
  have g2: "\<lbrakk>0 < z; z < 1; z \<notin> s2\<rbrakk> \<Longrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1019
            vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2+1/2)) =
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1020
            2 *\<^sub>R vector_derivative g2 (at z)" for z
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61976
diff changeset
  1021
    apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g2(2*x-1))" and d = "\<bar>z/2\<bar>"]])
62390
842917225d56 more canonical names
nipkow
parents: 62379
diff changeset
  1022
    apply (simp_all add: field_simps dist_real_def abs_if split: if_split_asm)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1023
    apply (rule vector_diff_chain_at [of "\<lambda>x. x*2-1" 2 _ g2, simplified o_def])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1024
    using s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1025
    apply (auto simp: has_vector_derivative_def has_derivative_def bounded_linear_mult_left
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1026
                      vector_derivative_works add_divide_distrib)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1027
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1028
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1029
    using s2
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1030
    apply (auto simp: contour_integrable_on)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1031
    apply (rule integrable_spike_finite [of "{0,1} \<union> s2", OF _ _ *])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1032
    apply (auto simp: joinpaths_def scaleR_conv_of_real g2)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1033
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1034
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1035
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1036
lemma contour_integrable_join [simp]:
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1037
  shows
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1038
    "\<lbrakk>valid_path g1; valid_path g2\<rbrakk>
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1039
     \<Longrightarrow> f contour_integrable_on (g1 +++ g2) \<longleftrightarrow> f contour_integrable_on g1 \<and> f contour_integrable_on g2"
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1040
using contour_integrable_joinD1 contour_integrable_joinD2 contour_integrable_joinI by blast
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1041
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1042
lemma contour_integral_join [simp]:
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1043
  shows
61738
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1044
    "\<lbrakk>f contour_integrable_on g1; f contour_integrable_on g2; valid_path g1; valid_path g2\<rbrakk>
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1045
        \<Longrightarrow> contour_integral (g1 +++ g2) f = contour_integral g1 f + contour_integral g2 f"
c4f6031f1310 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents: 61711
diff changeset
  1046
  by (simp add: has_contour_integral_integral has_contour_integral_join contour_integral_unique)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1047
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1048
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1049
subsection\<open>Shifting the starting point of a (closed) path\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1050
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1051
lemma shiftpath_alt_def: "shiftpath a f = (\<lambda>x. if x \<le> 1-a then f (a + x) else f (a + x - 1))"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1052
  by (auto simp: shiftpath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1053
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1054
lemma valid_path_shiftpath [intro]:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1055
  assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1056
    shows "valid_path(shiftpath a g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1057
  using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1058
  apply (auto simp: valid_path_def shiftpath_alt_def)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1059
  apply (rule piecewise_C1_differentiable_cases)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1060
  apply (auto simp: algebra_simps)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1061
  apply (rule piecewise_C1_differentiable_affine [of g 1 a, simplified o_def scaleR_one])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1062
  apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1063
  apply (rule piecewise_C1_differentiable_affine [of g 1 "a-1", simplified o_def scaleR_one algebra_simps])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1064
  apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1065
  done