src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
author paulson
Mon, 21 Sep 2015 19:52:13 +0100
changeset 61204 3e491e34a62e
parent 61200 a5674da43c2b
child 61222 05d28dc76e5c
permissions -rw-r--r--
new lemmas and movement of lemmas into place
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
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     3
theory Cauchy_Integral_Thm
61104
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 60809
diff changeset
     4
imports Complex_Transcendental Weierstrass
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     5
begin
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     6
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
     7
subsection \<open>Piecewise differentiable functions\<close>
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     8
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     9
definition piecewise_differentiable_on
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    10
           (infixr "piecewise'_differentiable'_on" 50)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    11
  where "f piecewise_differentiable_on i  \<equiv>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    12
           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
    13
           (\<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
    14
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    15
lemma piecewise_differentiable_on_imp_continuous_on:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    16
    "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
    17
by (simp add: piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    18
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    19
lemma piecewise_differentiable_on_subset:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    20
    "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
    21
  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
    22
  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
    23
  apply safe
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
    24
  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
    25
  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
    26
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    27
lemma differentiable_on_imp_piecewise_differentiable:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    28
  fixes a:: "'a::{linorder_topology,real_normed_vector}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    29
  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
    30
  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
    31
  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
    32
  done
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    33
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    34
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
    35
    "(\<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
    36
         \<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
    37
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
    38
         intro: differentiable_within_subset)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    39
61204
3e491e34a62e new lemmas and movement of lemmas into place
paulson
parents: 61200
diff changeset
    40
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
    41
  by (simp add: differentiable_imp_piecewise_differentiable)
3e491e34a62e new lemmas and movement of lemmas into place
paulson
parents: 61200
diff changeset
    42
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    43
lemma piecewise_differentiable_compose:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    44
    "\<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
    45
      \<And>x. finite (s \<inter> f-`{x})\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    46
      \<Longrightarrow> (g o f) piecewise_differentiable_on s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    47
  apply (simp add: piecewise_differentiable_on_def, safe)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    48
  apply (blast intro: continuous_on_compose2)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    49
  apply (rename_tac A B)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    50
  apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f-`{x})" in exI)
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
    51
  apply (blast intro: differentiable_chain_within)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
    52
  done
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    53
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    54
lemma piecewise_differentiable_affine:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    55
  fixes m::real
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    56
  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
    57
  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
    58
proof (cases "m = 0")
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    59
  case True
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    60
  then show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    61
    unfolding o_def
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    62
    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
    63
next
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    64
  case False
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    65
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    66
    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
    67
    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
    68
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    69
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    70
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    71
lemma piecewise_differentiable_cases:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    72
  fixes c::real
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    73
  assumes "f piecewise_differentiable_on {a..c}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    74
          "g piecewise_differentiable_on {c..b}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    75
           "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
    76
  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
    77
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    78
  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
    79
                       "\<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
    80
                       "\<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
    81
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    82
    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
    83
  have finabc: "finite ({a,b,c} \<union> (s \<union> t))"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
    84
    by (metis `finite s` `finite t` finite_Un finite_insert finite.emptyI)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    85
  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
    86
    using assms piecewise_differentiable_on_def by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    87
  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
    88
    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
    89
                               OF closed_real_atLeastAtMost [of c b],
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    90
                               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
    91
    by (force simp: ivl_disj_un_two_touch)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    92
  moreover
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    93
  { 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
    94
    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
    95
    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
    96
    proof (cases x c rule: le_cases)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    97
      case le show ?diff_fg
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
    98
        apply (rule differentiable_transform_within [where d = "dist x c" and f = f])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
    99
        using x le st
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   100
        apply (simp_all add: dist_real_def dist_nz [symmetric])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   101
        apply (rule differentiable_at_withinI)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   102
        apply (rule differentiable_within_open [where s = "{a<..<c} - s", THEN iffD1], simp_all)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   103
        apply (blast intro: open_greaterThanLessThan finite_imp_closed)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   104
        apply (force elim!: differentiable_subset)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   105
        done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   106
    next
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   107
      case ge show ?diff_fg
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   108
        apply (rule differentiable_transform_within [where d = "dist x c" and f = g])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   109
        using x ge st
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   110
        apply (simp_all add: dist_real_def dist_nz [symmetric])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   111
        apply (rule differentiable_at_withinI)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   112
        apply (rule differentiable_within_open [where s = "{c<..<b} - t", THEN iffD1], simp_all)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   113
        apply (blast intro: open_greaterThanLessThan finite_imp_closed)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   114
        apply (force elim!: differentiable_subset)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   115
        done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   116
    qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   117
  }
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   118
  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
   119
                 (\<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
   120
    by (meson finabc)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   121
  ultimately show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   122
    by (simp add: piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   123
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   124
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   125
lemma piecewise_differentiable_neg:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   126
    "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
   127
  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
   128
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   129
lemma piecewise_differentiable_add:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   130
  assumes "f piecewise_differentiable_on i"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   131
          "g piecewise_differentiable_on i"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   132
    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
   133
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   134
  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
   135
                       "\<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
   136
                       "\<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
   137
    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
   138
  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
   139
    by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   140
  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
   141
    using assms piecewise_differentiable_on_def by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   142
  ultimately show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   143
    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
   144
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   145
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   146
lemma piecewise_differentiable_diff:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   147
    "\<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
   148
     \<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
   149
  unfolding diff_conv_add_uminus
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   150
  by (metis piecewise_differentiable_add piecewise_differentiable_neg)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   151
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   152
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
   153
    "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
   154
  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
   155
  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
   156
  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
   157
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   158
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   159
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
   160
    "\<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
   161
  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
   162
  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
   163
  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
   164
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   165
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   166
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
   167
    "(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
   168
  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
   169
  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
   170
  apply simp
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   171
  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
   172
  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
   173
       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
   174
  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
   175
  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
   176
  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
   177
  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
   178
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   179
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   180
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
   181
    "\<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
   182
    \<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
   183
  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
   184
  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
   185
  apply simp
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   186
  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
   187
  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
   188
          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
   189
  apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: split_if_asm)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   190
  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
   191
  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
   192
  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
   193
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   194
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   195
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   196
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
   197
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   198
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
   199
           (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
   200
  where
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   201
  "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
   202
   (\<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
   203
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   204
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
   205
    "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
   206
     (\<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
   207
  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
   208
  apply safe
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   209
  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
   210
  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
   211
  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
   212
  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
   213
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   214
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   215
lemma 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
   216
  "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
   217
  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
   218
  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
   219
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   220
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
   221
    "\<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
   222
      \<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
   223
      \<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
   224
  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
   225
   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
   226
  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
   227
   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
   228
   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
   229
  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
   230
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   231
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
   232
  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
   233
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   234
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
   235
  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
   236
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   237
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
   238
  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
   239
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   240
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
   241
  "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
   242
  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
   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 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
   245
  "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
   246
  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
   247
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   248
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
   249
  "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
   250
  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
   251
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   252
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
   253
  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
   254
  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
   255
  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
   256
  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
   257
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   258
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
   259
  "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
   260
  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
   261
  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
   262
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   263
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   264
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
   265
           (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
   266
  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
   267
           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
   268
           (\<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
   269
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   270
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
   271
    "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
   272
  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
   273
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   274
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
   275
    "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
   276
  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
   277
           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
   278
           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
   279
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   280
lemma 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
   281
    "\<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
   282
      \<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
   283
      \<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
   284
  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
   285
  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
   286
  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
   287
  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
   288
  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
   289
  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
   290
  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
   291
  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
   292
  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
   293
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   294
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
   295
    "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
   296
  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
   297
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   298
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
   299
  "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
   300
  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
   301
  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
   302
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   303
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
   304
  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
   305
  by auto
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 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
   308
  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
   309
  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
   310
  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
   311
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
   312
  case True
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   313
  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
   314
    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
   315
next
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   316
  case False
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   317
  show ?thesis
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   318
    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
   319
    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
   320
    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
   321
    apply simp
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   322
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   323
qed
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   324
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   325
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
   326
  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
   327
  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
   328
          "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
   329
           "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
   330
  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
   331
proof -
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   332
  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
   333
                       "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
   334
                       "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
   335
    using assms
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   336
    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
   337
  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
   338
        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
   339
    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
   340
  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
   341
    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
   342
  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
   343
    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
   344
                               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
   345
                               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
   346
    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
   347
  { fix x
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   348
    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
   349
    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
   350
    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
   351
      case le show ?diff_fg
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   352
        apply (rule differentiable_transform_at [of "dist x c" _ f])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   353
        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
   354
    next
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   355
      case ge show ?diff_fg
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   356
        apply (rule differentiable_transform_at [of "dist x c" _ g])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   357
        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
   358
    qed
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   359
  }
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   360
  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
   361
    by auto
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   362
  moreover
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   363
  { 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
   364
       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
   365
    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
   366
      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
   367
    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
   368
      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
   369
      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
   370
      apply (rule vector_derivative_at [symmetric])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   371
      apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_at)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   372
      apply (simp_all add: dist_norm vector_derivative_works [symmetric])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   373
      using f_diff
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   374
      by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_imp_le st(1))
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   375
    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
   376
      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
   377
      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
   378
      apply (rule vector_derivative_at [symmetric])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   379
      apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_at)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   380
      apply (simp_all add: dist_norm vector_derivative_works [symmetric])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   381
      using g_diff
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   382
      by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_imp_le st(2))
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   383
    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
   384
        (\<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
   385
      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
   386
      done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   387
  } note * = this
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   388
  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
   389
    using st
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   390
    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
   391
  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
   392
    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
   393
    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
   394
  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
   395
    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
   396
qed
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   397
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   398
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
   399
    "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
   400
  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
   401
  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
   402
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   403
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
   404
  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
   405
          "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
   406
    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
   407
proof -
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   408
  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
   409
                       "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
   410
                       "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
   411
    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
   412
  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
   413
    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
   414
  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
   415
    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
   416
  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
   417
    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
   418
qed
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   419
61204
3e491e34a62e new lemmas and movement of lemmas into place
paulson
parents: 61200
diff changeset
   420
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
   421
    "\<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
   422
     \<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
   423
  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
   424
  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
   425
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   426
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
   427
  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
   428
  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
   429
    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
   430
proof -
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   431
  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
   432
             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
   433
             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
   434
    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
   435
  then have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (op * 2 ` s)" for x
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   436
    apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_at)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   437
    using that
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   438
    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
   439
    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
   440
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   441
  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
   442
               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
   443
    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
   444
    using that
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   445
    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
   446
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   447
  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
   448
    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
   449
  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
   450
    apply (rule continuous_on_eq [OF _ vector_derivative_at])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   451
    apply (rule_tac f="g1 o op*2" and d="dist x (1/2)" in has_vector_derivative_transform_at)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   452
    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
   453
    apply (force intro: g1D differentiable_chain_at)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   454
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   455
  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
   456
                      ((\<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
   457
    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
   458
    using coDhalf
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   459
    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
   460
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   461
  then have 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
   462
    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
   463
  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
   464
    using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   465
  with `finite s` show ?thesis
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   466
    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
   467
    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
   468
    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
   469
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   470
qed
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   471
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   472
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
   473
  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
   474
  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
   475
    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
   476
proof -
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   477
  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
   478
             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
   479
             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
   480
    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
   481
  then have g2D: "g2 differentiable at x" 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
   482
    apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_at)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   483
    using that
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_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
   485
    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
   486
    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
   487
    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
   488
    apply assumption
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   489
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   490
  have [simp]: "vector_derivative (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
   491
               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
   492
    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
   493
  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
   494
    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
   495
  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
   496
    apply (rule continuous_on_eq [OF _ vector_derivative_at])
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   497
    apply (rule_tac f="g2 o (\<lambda>x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_at)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   498
    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
   499
                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
   500
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   501
  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
   502
    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
   503
    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
   504
    done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   505
  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
   506
                      ((\<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
   507
    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
   508
  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
   509
    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
   510
  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
   511
    using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   512
  with `finite s` show ?thesis
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   513
    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
   514
    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
   515
    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
   516
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   517
qed
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   518
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   519
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
   520
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   521
lemma Diff_Un_eq: "A - (B \<union> C) = A - B - C"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   522
  by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   523
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   524
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
   525
  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
   526
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   527
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
   528
  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
   529
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   530
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
   531
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   532
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
   533
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
   534
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   535
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
   536
  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
   537
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   538
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
   539
  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
   540
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   541
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
   542
  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
   543
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   544
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
   545
  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
   546
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   547
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   548
subsection\<open>Contour Integrals along a path\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   549
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   550
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
   551
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   552
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
   553
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   554
definition has_path_integral :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   555
           (infixr "has'_path'_integral" 50)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   556
  where "(f has_path_integral i) g \<equiv>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   557
           ((\<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
   558
            has_integral i) {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   559
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   560
definition path_integrable_on
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   561
           (infixr "path'_integrable'_on" 50)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   562
  where "f path_integrable_on g \<equiv> \<exists>i. (f has_path_integral i) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   563
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   564
definition path_integral
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   565
  where "path_integral g f \<equiv> @i. (f has_path_integral i) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   566
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   567
lemma path_integral_unique: "(f has_path_integral i)  g \<Longrightarrow> path_integral g f = i"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   568
  by (auto simp: path_integral_def has_path_integral_def integral_def [symmetric])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   569
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   570
lemma has_path_integral_integral:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   571
    "f path_integrable_on i \<Longrightarrow> (f has_path_integral (path_integral i f)) i"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   572
  by (metis path_integral_unique path_integrable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   573
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   574
lemma has_path_integral_unique:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   575
    "(f has_path_integral i) g \<Longrightarrow> (f has_path_integral j) g \<Longrightarrow> i = j"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   576
  using has_integral_unique
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   577
  by (auto simp: has_path_integral_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   578
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   579
lemma has_path_integral_integrable: "(f has_path_integral i) g \<Longrightarrow> f path_integrable_on g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   580
  using path_integrable_on_def by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   581
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   582
(* 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
   583
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   584
lemma vector_derivative_within_interior:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   585
     "\<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
   586
      \<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
   587
  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
   588
  apply (subst lim_within_interior, auto)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   589
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   590
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   591
lemma has_integral_localized_vector_derivative:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   592
    "((\<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
   593
     ((\<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
   594
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   595
  have "{a..b} - {a,b} = interior {a..b}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   596
    by (simp add: atLeastAtMost_diff_ends)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   597
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   598
    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
   599
    apply (auto simp: vector_derivative_within_interior)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   600
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   601
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   602
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   603
lemma integrable_on_localized_vector_derivative:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   604
    "(\<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
   605
     (\<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
   606
  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
   607
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   608
lemma has_path_integral:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   609
     "(f has_path_integral i) g \<longleftrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   610
      ((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   611
  by (simp add: has_integral_localized_vector_derivative has_path_integral_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   612
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   613
lemma path_integrable_on:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   614
     "f path_integrable_on g \<longleftrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   615
      (\<lambda>t. f(g t) * vector_derivative g (at t)) integrable_on {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   616
  by (simp add: has_path_integral integrable_on_def path_integrable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   617
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   618
subsection\<open>Reversing a path\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   619
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   620
lemma valid_path_imp_reverse:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   621
  assumes "valid_path g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   622
    shows "valid_path(reversepath g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   623
proof -
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   624
  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
   625
    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
   626
  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
   627
    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
   628
    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
   629
    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
   630
    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
   631
    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
   632
    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
   633
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   634
  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
   635
    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
   636
qed
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 valid_path_reversepath: "valid_path(reversepath g) \<longleftrightarrow> valid_path g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   639
  using valid_path_imp_reverse by force
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 has_path_integral_reversepath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   642
  assumes "valid_path g" "(f has_path_integral i) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   643
    shows "(f has_path_integral (-i)) (reversepath g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   644
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   645
  { 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
   646
    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
   647
      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
   648
            - 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
   649
      proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   650
        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
   651
          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
   652
          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
   653
        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
   654
          apply (rule vector_diff_chain_within)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   655
          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
   656
          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
   657
          done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   658
        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
   659
          by (simp add: o_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   660
        show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   661
          using xs
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   662
          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
   663
      qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   664
  } note * = this
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   665
  have 01: "{0..1::real} = cbox 0 1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   666
    by simp
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   667
  show ?thesis using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   668
    apply (auto simp: has_path_integral_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   669
    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
   670
    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
   671
    apply (drule has_integral_neg)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   672
    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
   673
    apply (auto simp: *)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   674
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   675
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   676
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   677
lemma path_integrable_reversepath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   678
    "valid_path g \<Longrightarrow> f path_integrable_on g \<Longrightarrow> f path_integrable_on (reversepath g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   679
  using has_path_integral_reversepath path_integrable_on_def by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   680
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   681
lemma path_integrable_reversepath_eq:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   682
    "valid_path g \<Longrightarrow> (f path_integrable_on (reversepath g) \<longleftrightarrow> f path_integrable_on g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   683
  using path_integrable_reversepath valid_path_reversepath by fastforce
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   684
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   685
lemma path_integral_reversepath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   686
    "\<lbrakk>valid_path g; f path_integrable_on g\<rbrakk> \<Longrightarrow> path_integral (reversepath g) f = -(path_integral g f)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   687
  using has_path_integral_reversepath path_integrable_on_def path_integral_unique by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   688
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   689
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   690
subsection\<open>Joining two paths together\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   691
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   692
lemma valid_path_join:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   693
  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
   694
    shows "valid_path(g1 +++ g2)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   695
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   696
  have "g1 1 = g2 0"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   697
    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
   698
  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
   699
    apply (rule piecewise_C1_differentiable_compose)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   700
    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
   701
    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
   702
    apply (rule continuous_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   703
    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
   704
    done
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   705
  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
   706
    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
   707
    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
   708
    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
   709
             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
   710
  ultimately show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   711
    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
   712
    apply (rule piecewise_C1_differentiable_cases)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   713
    apply (auto simp: o_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   714
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   715
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   716
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   717
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
   718
  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
   719
  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
   720
  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
   721
  by (rule piecewise_C1_differentiable_D1)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   722
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   723
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
   724
  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
   725
  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
   726
  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
   727
  by (rule piecewise_C1_differentiable_D2)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   728
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   729
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
   730
  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
   731
  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
   732
  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
   733
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   734
lemma has_path_integral_join:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   735
  assumes "(f has_path_integral i1) g1" "(f has_path_integral i2) g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   736
          "valid_path g1" "valid_path g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   737
    shows "(f has_path_integral (i1 + i2)) (g1 +++ g2)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   738
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   739
  obtain s1 s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   740
    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
   741
      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
   742
    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
   743
    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
   744
  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
   745
   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
   746
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   747
    by (auto simp: has_path_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   748
  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
   749
   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
   750
    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
   751
          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
   752
    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
   753
  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
   754
            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
   755
            2 *\<^sub>R vector_derivative g1 (at (z*2))" for z
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   756
    apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>z - 1/2\<bar>" _ "(\<lambda>x. g1(2*x))"]])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   757
    apply (simp_all add: dist_real_def abs_if split: split_if_asm)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   758
    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
   759
    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
   760
    using s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   761
    apply (auto simp: algebra_simps vector_derivative_works)
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
  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
   764
            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
   765
            2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))" for z
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   766
    apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>z - 1/2\<bar>" _ "(\<lambda>x. g2 (2*x - 1))"]])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   767
    apply (simp_all add: dist_real_def abs_if split: split_if_asm)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   768
    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
   769
    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
   770
    using s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   771
    apply (auto simp: algebra_simps vector_derivative_works)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   772
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   773
  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
   774
    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
   775
    using s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   776
    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
   777
    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
   778
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   779
  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
   780
    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
   781
    using s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   782
    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
   783
    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
   784
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   785
  ultimately
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   786
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   787
    apply (simp add: has_path_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   788
    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
   789
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   790
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   791
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   792
lemma path_integrable_joinI:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   793
  assumes "f path_integrable_on g1" "f path_integrable_on g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   794
          "valid_path g1" "valid_path g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   795
    shows "f path_integrable_on (g1 +++ g2)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   796
  using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   797
  by (meson has_path_integral_join path_integrable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   798
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   799
lemma path_integrable_joinD1:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   800
  assumes "f path_integrable_on (g1 +++ g2)" "valid_path g1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   801
    shows "f path_integrable_on g1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   802
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   803
  obtain s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   804
    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
   805
    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
   806
  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
   807
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   808
    apply (auto simp: path_integrable_on)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   809
    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
   810
    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
   811
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   812
  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
   813
    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
   814
  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
   815
            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
   816
            2 *\<^sub>R vector_derivative g1 (at z)"  for z
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   817
    apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>(z-1)/2\<bar>" _ "(\<lambda>x. g1(2*x))"]])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   818
    apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   819
    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
   820
    using s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   821
    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
   822
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   823
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   824
    using s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   825
    apply (auto simp: path_integrable_on)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   826
    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
   827
    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
   828
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   829
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   830
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   831
lemma path_integrable_joinD2:
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   832
  assumes "f path_integrable_on (g1 +++ g2)" "valid_path g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   833
    shows "f path_integrable_on g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   834
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   835
  obtain s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   836
    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
   837
    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
   838
  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
   839
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   840
    apply (auto simp: path_integrable_on)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   841
    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
   842
    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
   843
    apply (simp add: image_affinity_atLeastAtMost_diff)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   844
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   845
  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
   846
                integrable_on {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   847
    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
   848
  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
   849
            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
   850
            2 *\<^sub>R vector_derivative g2 (at z)" for z
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   851
    apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>z/2\<bar>" _ "(\<lambda>x. g2(2*x-1))"]])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   852
    apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   853
    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
   854
    using s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   855
    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
   856
                      vector_derivative_works add_divide_distrib)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   857
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   858
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   859
    using s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   860
    apply (auto simp: path_integrable_on)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   861
    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
   862
    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
   863
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   864
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   865
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   866
lemma path_integrable_join [simp]:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   867
  shows
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   868
    "\<lbrakk>valid_path g1; valid_path g2\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   869
     \<Longrightarrow> f path_integrable_on (g1 +++ g2) \<longleftrightarrow> f path_integrable_on g1 \<and> f path_integrable_on g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   870
using path_integrable_joinD1 path_integrable_joinD2 path_integrable_joinI by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   871
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   872
lemma path_integral_join [simp]:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   873
  shows
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   874
    "\<lbrakk>f path_integrable_on g1; f path_integrable_on g2; valid_path g1; valid_path g2\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   875
        \<Longrightarrow> path_integral (g1 +++ g2) f = path_integral g1 f + path_integral g2 f"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   876
  by (simp add: has_path_integral_integral has_path_integral_join path_integral_unique)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   877
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   878
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   879
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
   880
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   881
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
   882
  by (auto simp: shiftpath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   883
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   884
lemma valid_path_shiftpath [intro]:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   885
  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
   886
    shows "valid_path(shiftpath a g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   887
  using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   888
  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
   889
  apply (rule piecewise_C1_differentiable_cases)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   890
  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
   891
  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
   892
  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
   893
  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
   894
  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
   895
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   896
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   897
lemma has_path_integral_shiftpath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   898
  assumes f: "(f has_path_integral i) g" "valid_path g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   899
      and a: "a \<in> {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   900
    shows "(f has_path_integral i) (shiftpath a g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   901
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   902
  obtain s
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   903
    where s: "finite s" and g: "\<forall>x\<in>{0..1} - s. g differentiable at x"
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   904
    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
   905
  have *: "((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   906
    using assms by (auto simp: has_path_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   907
  then have i: "i = integral {a..1} (\<lambda>x. f (g x) * vector_derivative g (at x)) +
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   908
                    integral {0..a} (\<lambda>x. f (g x) * vector_derivative g (at x))"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   909
    apply (rule has_integral_unique)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   910
    apply (subst add.commute)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   911
    apply (subst Integration.integral_combine)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   912
    using assms * integral_unique by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   913
  { fix x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   914
    have "0 \<le> x \<Longrightarrow> x + a < 1 \<Longrightarrow> x \<notin> (\<lambda>x. x - a) ` s \<Longrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   915
         vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a))"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   916
      unfolding shiftpath_def
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   917
      apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist(1-a) x" _ "(\<lambda>x. g(a+x))"]])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   918
        apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   919
      apply (rule vector_diff_chain_at [of "\<lambda>x. x+a" 1 _ g, simplified o_def scaleR_one])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   920
       apply (intro derivative_eq_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   921
      using g
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   922
       apply (drule_tac x="x+a" in bspec)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   923
      using a apply (auto simp: has_vector_derivative_def vector_derivative_works image_def add.commute)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   924
      done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   925
  } note vd1 = this
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   926
  { fix x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   927
    have "1 < x + a \<Longrightarrow> x \<le> 1 \<Longrightarrow> x \<notin> (\<lambda>x. x - a + 1) ` s \<Longrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   928
          vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a - 1))"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   929
      unfolding shiftpath_def
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   930
      apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist (1-a) x" _ "(\<lambda>x. g(a+x-1))"]])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   931
        apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   932
      apply (rule vector_diff_chain_at [of "\<lambda>x. x+a-1" 1 _ g, simplified o_def scaleR_one])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   933
       apply (intro derivative_eq_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   934
      using g
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   935
      apply (drule_tac x="x+a-1" in bspec)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   936
      using a apply (auto simp: has_vector_derivative_def vector_derivative_works image_def add.commute)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   937
      done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   938
  } note vd2 = this
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   939
  have va1: "(\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on ({a..1})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   940
    using * a   by (fastforce intro: integrable_subinterval_real)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   941
  have v0a: "(\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on ({0..a})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   942
    apply (rule integrable_subinterval_real)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   943
    using * a by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   944
  have "((\<lambda>x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x))
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   945
        has_integral  integral {a..1} (\<lambda>x. f (g x) * vector_derivative g (at x)))  {0..1 - a}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   946
    apply (rule has_integral_spike_finite
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   947
             [where s = "{1-a} \<union> (\<lambda>x. x-a) ` s" and f = "\<lambda>x. f(g(a+x)) * vector_derivative g (at(a+x))"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   948
      using s apply blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   949
     using a apply (auto simp: algebra_simps vd1)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   950
     apply (force simp: shiftpath_def add.commute)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   951
    using has_integral_affinity [where m=1 and c=a, simplified, OF integrable_integral [OF va1]]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   952
    apply (simp add: image_affinity_atLeastAtMost_diff [where m=1 and c=a, simplified] add.commute)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   953
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   954
  moreover
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   955
  have "((\<lambda>x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x))
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   956
        has_integral  integral {0..a} (\<lambda>x. f (g x) * vector_derivative g (at x)))  {1 - a..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   957
    apply (rule has_integral_spike_finite
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   958
             [where s = "{1-a} \<union> (\<lambda>x. x-a+1) ` s" and f = "\<lambda>x. f(g(a+x-1)) * vector_derivative g (at(a+x-1))"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   959
      using s apply blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   960
     using a apply (auto simp: algebra_simps vd2)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   961
     apply (force simp: shiftpath_def add.commute)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   962
    using has_integral_affinity [where m=1 and c="a-1", simplified, OF integrable_integral [OF v0a]]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   963
    apply (simp add: image_affinity_atLeastAtMost [where m=1 and c="1-a", simplified])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   964
    apply (simp add: algebra_simps)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   965
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   966
  ultimately show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   967
    using a
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   968
    by (auto simp: i has_path_integral intro: has_integral_combine [where c = "1-a"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   969
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   970
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   971
lemma has_path_integral_shiftpath_D:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   972
  assumes "(f has_path_integral i) (shiftpath a g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   973
          "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
   974
    shows "(f has_path_integral i) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   975
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   976
  obtain s
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   977
    where s: "finite s" and g: "\<forall>x\<in>{0..1} - s. g differentiable at x"
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
   978
    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
   979
  { fix x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   980
    assume x: "0 < x" "x < 1" "x \<notin> s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   981
    then have gx: "g differentiable at x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   982
      using g by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   983
    have "vector_derivative g (at x within {0..1}) =
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   984
          vector_derivative (shiftpath (1 - a) (shiftpath a g)) (at x within {0..1})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   985
      apply (rule vector_derivative_at_within_ivl
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   986
                  [OF has_vector_derivative_transform_within_open
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   987
                      [of "{0<..<1}-s" _ "(shiftpath (1 - a) (shiftpath a g))"]])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   988
      using s g assms x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   989
      apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   990
                        vector_derivative_within_interior vector_derivative_works [symmetric])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   991
      apply (rule Derivative.differentiable_transform_at [of "min x (1-x)", OF _ _ gx])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   992
      apply (auto simp: dist_real_def shiftpath_shiftpath abs_if)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   993
      done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   994
  } note vd = this
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   995
  have fi: "(f has_path_integral i) (shiftpath (1 - a) (shiftpath a g))"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   996
    using assms  by (auto intro!: has_path_integral_shiftpath)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   997
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   998
    apply (simp add: has_path_integral_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   999
    apply (rule has_integral_spike_finite [of "{0,1} \<union> s", OF _ _  fi [unfolded has_path_integral_def]])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1000
    using s assms vd
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1001
    apply (auto simp: Path_Connected.shiftpath_shiftpath)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1002
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1003
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1004
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1005
lemma has_path_integral_shiftpath_eq:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1006
  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
  1007
    shows "(f has_path_integral i) (shiftpath a g) \<longleftrightarrow> (f has_path_integral i) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1008
  using assms has_path_integral_shiftpath has_path_integral_shiftpath_D by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1009
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1010
lemma path_integral_shiftpath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1011
  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
  1012
    shows "path_integral (shiftpath a g) f = path_integral g f"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1013
   using assms by (simp add: path_integral_def has_path_integral_shiftpath_eq)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1014
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1015
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1016
subsection\<open>More about straight-line paths\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1017
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1018
lemma has_vector_derivative_linepath_within:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1019
    "(linepath a b has_vector_derivative (b - a)) (at x within s)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1020
apply (simp add: linepath_def has_vector_derivative_def algebra_simps)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1021
apply (rule derivative_eq_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1022
done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1023
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1024
lemma vector_derivative_linepath_within:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1025
    "x \<in> {0..1} \<Longrightarrow> vector_derivative (linepath a b) (at x within {0..1}) = b - a"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1026
  apply (rule vector_derivative_within_closed_interval [of 0 "1::real", simplified])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1027
  apply (auto simp: has_vector_derivative_linepath_within)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1028
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1029
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1030
lemma vector_derivative_linepath_at [simp]: "vector_derivative (linepath a b) (at x) = b - a"
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1031
  by (simp add: has_vector_derivative_linepath_within vector_derivative_at)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1032
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1033
lemma valid_path_linepath [iff]: "valid_path (linepath a b)"
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1034
  apply (simp add: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_on_linepath)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1035
  apply (rule_tac x="{}" in exI)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1036
  apply (simp add: differentiable_on_def differentiable_def)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1037
  using has_vector_derivative_def has_vector_derivative_linepath_within
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1038
  apply (fastforce simp add: continuous_on_eq_continuous_within)
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1039
  done
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1040
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1041
lemma has_path_integral_linepath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1042
  shows "(f has_path_integral i) (linepath a b) \<longleftrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1043
         ((\<lambda>x. f(linepath a b x) * (b - a)) has_integral i) {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1044
  by (simp add: has_path_integral vector_derivative_linepath_at)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1045
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1046
lemma linepath_in_path:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1047
  shows "x \<in> {0..1} \<Longrightarrow> linepath a b x \<in> closed_segment a b"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1048
  by (auto simp: segment linepath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1049
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1050
lemma linepath_image_01: "linepath a b ` {0..1} = closed_segment a b"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1051
  by (auto simp: segment linepath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1052
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1053
lemma linepath_in_convex_hull:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1054
    fixes x::real
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1055
    assumes a: "a \<in> convex hull s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1056
        and b: "b \<in> convex hull s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1057
        and x: "0\<le>x" "x\<le>1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1058
       shows "linepath a b x \<in> convex hull s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1059
  apply (rule closed_segment_subset_convex_hull [OF a b, THEN subsetD])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1060
  using x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1061
  apply (auto simp: linepath_image_01 [symmetric])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1062
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1063
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1064
lemma Re_linepath: "Re(linepath (of_real a) (of_real b) x) = (1 - x)*a + x*b"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1065
  by (simp add: linepath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1066
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1067
lemma Im_linepath: "Im(linepath (of_real a) (of_real b) x) = 0"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1068
  by (simp add: linepath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1069
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1070
lemma linepath_of_real: "(linepath (of_real a) (of_real b) x) = of_real ((1 - x)*a + x*b)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1071
  by (simp add: scaleR_conv_of_real linepath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1072
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1073
lemma of_real_linepath: "of_real (linepath a b x) = linepath (of_real a) (of_real b) x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1074
  by (metis linepath_of_real mult.right_neutral of_real_def real_scaleR_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1075
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1076
lemma has_path_integral_trivial [iff]: "(f has_path_integral 0) (linepath a a)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1077
  by (simp add: has_path_integral_linepath)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1078
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1079
lemma path_integral_trivial [simp]: "path_integral (linepath a a) f = 0"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1080
  using has_path_integral_trivial path_integral_unique by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1081
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1082
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1083
subsection\<open>Relation to subpath construction\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1084
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1085
lemma valid_path_subpath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1086
  fixes g :: "real \<Rightarrow> 'a :: real_normed_vector"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1087
  assumes "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1088
    shows "valid_path(subpath u v g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1089
proof (cases "v=u")
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1090
  case True
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1091
  then 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
  1092
    unfolding valid_path_def subpath_def
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1093
    by (force intro: C1_differentiable_on_const C1_differentiable_imp_piecewise)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1094
next
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1095
  case False
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1096
  have "(g o (\<lambda>x. ((v-u) * x + u))) 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
  1097
    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
  1098
    apply (simp add: C1_differentiable_imp_piecewise)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1099
     apply (simp add: image_affinity_atLeastAtMost)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1100
    using assms False
61190
2bd401e364f9 Massive revisions, as a valid path must now be continously differentiable (C!)
paulson <lp15@cam.ac.uk>
parents: 61104
diff changeset
  1101
    apply (auto simp: algebra_simps valid_path_def piecewise_C1_differentiable_on_subset)
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1102
    apply (subst Int_commute)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1103
    apply (auto simp: inj_on_def algebra_simps crossproduct_eq finite_vimage_IntI)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1104
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1105
  then show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1106
    by (auto simp: o_def valid_path_def subpath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1107
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1108
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1109
lemma has_path_integral_subpath_refl [iff]: "(f has_path_integral 0) (subpath u u g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1110
  by (simp add: has_path_integral subpath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1111
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1112
lemma path_integrable_subpath_refl [iff]: "f path_integrable_on (subpath u u g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1113
  using has_path_integral_subpath_refl path_integrable_on_def by blast