src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
author paulson <lp15@cam.ac.uk>
Tue, 28 Jul 2015 16:16:13 +0100
changeset 60809 457abb82fb9e
child 61104 3c2d4636cebc
permissions -rw-r--r--
the Cauchy integral theorem and related material
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
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     4
imports Complex_Transcendental Path_Connected
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
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     7
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     8
definition piecewise_differentiable_on
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     9
           (infixr "piecewise'_differentiable'_on" 50)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    10
  where "f piecewise_differentiable_on i  \<equiv>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    11
           continuous_on i f \<and>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    12
           (\<exists>s. finite s \<and> (\<forall>x \<in> i - s. f differentiable (at x)))"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    13
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    14
lemma piecewise_differentiable_on_imp_continuous_on:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    15
    "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
    16
by (simp add: piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    17
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    18
lemma piecewise_differentiable_on_subset:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    19
    "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
    20
  using continuous_on_subset
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    21
  by (fastforce simp: piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    22
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    23
lemma differentiable_on_imp_piecewise_differentiable:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    24
  fixes a:: "'a::{linorder_topology,real_normed_vector}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    25
  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
    26
  apply (simp add: piecewise_differentiable_on_def differentiable_imp_continuous_on)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    27
  apply (rule_tac x="{a,b}" in exI, simp)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    28
  by (metis DiffE atLeastAtMost_diff_ends differentiable_on_subset subsetI
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    29
        differentiable_on_eq_differentiable_at open_greaterThanLessThan)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    30
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    31
lemma differentiable_imp_piecewise_differentiable:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    32
    "(\<And>x. x \<in> s \<Longrightarrow> f differentiable (at x))
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    33
         \<Longrightarrow> f piecewise_differentiable_on s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    34
by (auto simp: piecewise_differentiable_on_def differentiable_on_eq_differentiable_at
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    35
               differentiable_imp_continuous_within continuous_at_imp_continuous_on)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    36
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    37
lemma piecewise_differentiable_compose:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    38
    "\<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
    39
      \<And>x. finite (s \<inter> f-`{x})\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    40
      \<Longrightarrow> (g o f) piecewise_differentiable_on s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    41
  apply (simp add: piecewise_differentiable_on_def, safe)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    42
  apply (blast intro: continuous_on_compose2)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    43
  apply (rename_tac A B)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    44
  apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f-`{x})" in exI)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    45
  using differentiable_chain_at by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    46
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    47
lemma piecewise_differentiable_affine:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    48
  fixes m::real
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    49
  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
    50
  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
    51
proof (cases "m = 0")
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    52
  case True
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    53
  then show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    54
    unfolding o_def
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    55
    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
    56
next
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    57
  case False
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    58
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    59
    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
    60
    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
    61
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    62
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    63
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    64
lemma piecewise_differentiable_cases:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    65
  fixes c::real
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    66
  assumes "f piecewise_differentiable_on {a..c}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    67
          "g piecewise_differentiable_on {c..b}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    68
           "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
    69
  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
    70
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    71
  obtain s t where st: "finite s" "finite t"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    72
                       "\<forall>x\<in>{a..c} - s. f differentiable at x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    73
                       "\<forall>x\<in>{c..b} - t. g differentiable at x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    74
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    75
    by (auto simp: piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    76
  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
    77
    using assms piecewise_differentiable_on_def by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    78
  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
    79
    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
    80
                               OF closed_real_atLeastAtMost [of c b],
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    81
                               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
    82
    by (force simp: ivl_disj_un_two_touch)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    83
  moreover
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    84
  { fix x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    85
    assume x: "x \<in> {a..b} - insert c (s \<union> t)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    86
    have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x" (is "?diff_fg")
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    87
    proof (cases x c rule: le_cases)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    88
      case le show ?diff_fg
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    89
        apply (rule differentiable_transform_at [of "dist x c" _ f])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    90
        using dist_nz x dist_real_def le st x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    91
        apply auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    92
        done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    93
    next
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    94
      case ge show ?diff_fg
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    95
        apply (rule differentiable_transform_at [of "dist x c" _ g])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    96
        using dist_nz x dist_real_def ge st x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    97
        apply auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    98
        done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    99
    qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   100
  }
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   101
  then have "\<exists>s. finite s \<and> (\<forall>x\<in>{a..b} - s. (\<lambda>x. if x \<le> c then f x else g x) differentiable at x)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   102
    using st
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   103
    by (metis (full_types) finite_Un finite_insert)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   104
  ultimately show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   105
    by (simp add: piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   106
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   107
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   108
lemma piecewise_differentiable_neg:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   109
    "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
   110
  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
   111
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   112
lemma piecewise_differentiable_add:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   113
  assumes "f piecewise_differentiable_on i"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   114
          "g piecewise_differentiable_on i"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   115
    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
   116
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   117
  obtain s t where st: "finite s" "finite t"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   118
                       "\<forall>x\<in>i - s. f differentiable at x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   119
                       "\<forall>x\<in>i - t. g differentiable at x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   120
    using assms by (auto simp: piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   121
  then have "finite (s \<union> t) \<and> (\<forall>x\<in>i - (s \<union> t). (\<lambda>x. f x + g x) differentiable at x)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   122
    by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   123
  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
   124
    using assms piecewise_differentiable_on_def by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   125
  ultimately show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   126
    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
   127
qed
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_diff:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   130
    "\<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
   131
     \<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
   132
  unfolding diff_conv_add_uminus
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   133
  by (metis piecewise_differentiable_add piecewise_differentiable_neg)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   134
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   135
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   136
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
   137
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   138
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
   139
  by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   140
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   141
definition valid_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
   142
  where "valid_path f \<equiv> f piecewise_differentiable_on {0..1::real}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   143
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   144
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
   145
  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
   146
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   147
lemma valid_path_compose:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   148
  assumes "valid_path g" "f differentiable_on (path_image g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   149
  shows "valid_path (f o g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   150
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   151
  { fix s :: "real set"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   152
    assume df: "f differentiable_on g ` {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   153
       and cg: "continuous_on {0..1} g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   154
       and s: "finite s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   155
       and dg: "\<And>x. x\<in>{0..1} - s \<Longrightarrow> g differentiable at x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   156
    have dfo: "f differentiable_on g ` {0<..<1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   157
      by (auto intro: differentiable_on_subset [OF df])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   158
    have *: "\<And>x. x \<in> {0<..<1} \<Longrightarrow> x \<notin> s \<Longrightarrow> (f o g) differentiable (at x within ({0<..<1} - s))"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   159
      apply (rule differentiable_chain_within)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   160
      apply (simp_all add: dg differentiable_at_withinI differentiable_chain_within)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   161
      using df
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   162
      apply (force simp: differentiable_on_def elim: Deriv.differentiable_subset)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   163
      done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   164
    have oo: "open ({0<..<1} - s)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   165
      by (simp add: finite_imp_closed open_Diff s)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   166
    have "\<exists>s. finite s \<and> (\<forall>x\<in>{0..1} - s. f \<circ> g differentiable at x)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   167
      apply (rule_tac x="{0,1} Un s" in exI)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   168
      apply (simp add: Diff_Un_eq atLeastAtMost_diff_ends s del: Set.Un_insert_left, clarify)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   169
      apply (rule differentiable_within_open [OF _ oo, THEN iffD1])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   170
      apply (auto simp: *)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   171
      done }
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   172
  with assms show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   173
    by (clarsimp simp: valid_path_def piecewise_differentiable_on_def continuous_on_compose
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   174
                       differentiable_imp_continuous_on path_image_def   simp del: o_apply)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   175
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   176
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   177
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   178
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
   179
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   180
lemma valid_path_imp_path: "valid_path g \<Longrightarrow> path g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   181
by (simp add: path_def piecewise_differentiable_on_def valid_path_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   182
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   183
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
   184
  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
   185
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   186
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
   187
  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
   188
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   189
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
   190
  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
   191
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   192
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
   193
  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
   194
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   195
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   196
subsection\<open>Contour Integrals along a path\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   197
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   198
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
   199
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   200
text\<open>= piecewise differentiable function on [0,1]\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   201
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   202
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
   203
           (infixr "has'_path'_integral" 50)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   204
  where "(f has_path_integral i) g \<equiv>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   205
           ((\<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
   206
            has_integral i) {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   207
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   208
definition path_integrable_on
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   209
           (infixr "path'_integrable'_on" 50)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   210
  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
   211
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   212
definition path_integral
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   213
  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
   214
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   215
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
   216
  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
   217
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   218
lemma has_path_integral_integral:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   219
    "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
   220
  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
   221
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   222
lemma has_path_integral_unique:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   223
    "(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
   224
  using has_integral_unique
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   225
  by (auto simp: has_path_integral_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   226
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   227
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
   228
  using path_integrable_on_def by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   229
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   230
(* 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
   231
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   232
lemma vector_derivative_within_interior:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   233
     "\<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
   234
      \<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
   235
  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
   236
  apply (subst lim_within_interior, auto)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   237
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   238
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   239
lemma has_integral_localized_vector_derivative:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   240
    "((\<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
   241
     ((\<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
   242
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   243
  have "{a..b} - {a,b} = interior {a..b}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   244
    by (simp add: atLeastAtMost_diff_ends)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   245
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   246
    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
   247
    apply (auto simp: vector_derivative_within_interior)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   248
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   249
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   250
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   251
lemma integrable_on_localized_vector_derivative:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   252
    "(\<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
   253
     (\<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
   254
  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
   255
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   256
lemma has_path_integral:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   257
     "(f has_path_integral i) g \<longleftrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   258
      ((\<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
   259
  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
   260
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   261
lemma path_integrable_on:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   262
     "f path_integrable_on g \<longleftrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   263
      (\<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
   264
  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
   265
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   266
subsection\<open>Reversing a path\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   267
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   268
lemma valid_path_imp_reverse:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   269
  assumes "valid_path g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   270
    shows "valid_path(reversepath g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   271
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   272
  obtain s where "finite s" "\<forall>x\<in>{0..1} - s. g differentiable at x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   273
    using assms by (auto simp: valid_path_def piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   274
  then have "finite (op - 1 ` s)" "(\<forall>x\<in>{0..1} - op - 1 ` s. reversepath g differentiable at x)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   275
    apply (auto simp: reversepath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   276
    apply (rule differentiable_chain_at [of "\<lambda>x::real. 1-x" _ g, unfolded o_def])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   277
    using image_iff
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   278
    apply fastforce+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   279
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   280
  then show ?thesis using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   281
    by (auto simp: valid_path_def piecewise_differentiable_on_def path_def [symmetric])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   282
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   283
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   284
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
   285
  using valid_path_imp_reverse by force
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   286
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   287
lemma has_path_integral_reversepath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   288
  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
   289
    shows "(f has_path_integral (-i)) (reversepath g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   290
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   291
  { fix s x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   292
    assume xs: "\<forall>x\<in>{0..1} - s. g differentiable at x" "x \<notin> op - 1 ` s" "0 \<le> x" "x \<le> 1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   293
      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
   294
            - 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
   295
      proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   296
        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
   297
          using xs
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   298
          apply (drule_tac x="1-x" in bspec)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   299
          apply (simp_all add: has_vector_derivative_def differentiable_def, force)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   300
          apply (blast elim!: linear_imp_scaleR dest: has_derivative_linear)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   301
          done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   302
        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
   303
          apply (rule vector_diff_chain_within)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   304
          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
   305
          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
   306
          done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   307
        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
   308
          by (simp add: o_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   309
        show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   310
          using xs
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   311
          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
   312
      qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   313
  } note * = this
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   314
  have 01: "{0..1::real} = cbox 0 1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   315
    by simp
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   316
  show ?thesis using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   317
    apply (auto simp: has_path_integral_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   318
    apply (drule has_integral_affinity01 [where m= "-1" and c=1])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   319
    apply (auto simp: reversepath_def valid_path_def piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   320
    apply (drule has_integral_neg)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   321
    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
   322
    apply (auto simp: *)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   323
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   324
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   325
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   326
lemma path_integrable_reversepath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   327
    "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
   328
  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
   329
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   330
lemma path_integrable_reversepath_eq:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   331
    "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
   332
  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
   333
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   334
lemma path_integral_reversepath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   335
    "\<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
   336
  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
   337
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   338
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   339
subsection\<open>Joining two paths together\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   340
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   341
lemma valid_path_join:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   342
  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
   343
    shows "valid_path(g1 +++ g2)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   344
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   345
  have "g1 1 = g2 0"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   346
    using assms by (auto simp: pathfinish_def pathstart_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   347
  moreover have "(g1 o (\<lambda>x. 2*x)) piecewise_differentiable_on {0..1/2}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   348
    apply (rule piecewise_differentiable_compose)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   349
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   350
    apply (auto simp: valid_path_def piecewise_differentiable_on_def continuous_on_joinpaths)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   351
    apply (rule continuous_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   352
    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
   353
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   354
  moreover have "(g2 o (\<lambda>x. 2*x-1)) piecewise_differentiable_on {1/2..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   355
    apply (rule piecewise_differentiable_compose)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   356
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   357
    apply (auto simp: valid_path_def piecewise_differentiable_on_def continuous_on_joinpaths)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   358
    apply (rule continuous_intros | simp add: image_affinity_atLeastAtMost_diff)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   359
    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
   360
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   361
  ultimately show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   362
    apply (simp only: valid_path_def continuous_on_joinpaths joinpaths_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   363
    apply (rule piecewise_differentiable_cases)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   364
    apply (auto simp: o_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   365
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   366
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   367
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   368
lemma continuous_on_joinpaths_D1:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   369
    "continuous_on {0..1} (g1 +++ g2) \<Longrightarrow> continuous_on {0..1} g1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   370
  apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (op*(inverse 2))"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   371
  apply (simp add: joinpaths_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   372
  apply (rule continuous_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   373
  apply (auto elim!: continuous_on_subset)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   374
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   375
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   376
lemma continuous_on_joinpaths_D2:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   377
    "\<lbrakk>continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> continuous_on {0..1} g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   378
  apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (\<lambda>x. inverse 2*x + 1/2)"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   379
  apply (simp add: joinpaths_def pathfinish_def pathstart_def Ball_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   380
  apply (rule continuous_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   381
  apply (auto elim!: continuous_on_subset)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   382
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   383
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   384
lemma piecewise_differentiable_D1:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   385
    "(g1 +++ g2) piecewise_differentiable_on {0..1} \<Longrightarrow> g1 piecewise_differentiable_on {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   386
  apply (clarsimp simp add: piecewise_differentiable_on_def continuous_on_joinpaths_D1)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   387
  apply (rule_tac x="insert 1 ((op*2)`s)" in exI)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   388
  apply simp
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   389
  apply (intro ballI)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   390
  apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_at)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   391
  apply (auto simp: dist_real_def joinpaths_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   392
  apply (rule differentiable_chain_at derivative_intros | force)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   393
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   394
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   395
lemma piecewise_differentiable_D2:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   396
    "\<lbrakk>(g1 +++ g2) piecewise_differentiable_on {0..1}; pathfinish g1 = pathstart g2\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   397
    \<Longrightarrow> g2 piecewise_differentiable_on {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   398
  apply (clarsimp simp add: piecewise_differentiable_on_def continuous_on_joinpaths_D2)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   399
  apply (rule_tac x="insert 0 ((\<lambda>x. 2*x-1)`s)" in exI)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   400
  apply simp
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   401
  apply (intro ballI)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   402
  apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_at)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   403
  apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: split_if_asm)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   404
  apply (rule differentiable_chain_at derivative_intros | force simp: divide_simps)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   405
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   406
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   407
lemma valid_path_join_D1: "valid_path (g1 +++ g2) \<Longrightarrow> valid_path g1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   408
  by (simp add: valid_path_def piecewise_differentiable_D1)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   409
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   410
lemma valid_path_join_D2: "\<lbrakk>valid_path (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> valid_path g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   411
  by (simp add: valid_path_def piecewise_differentiable_D2)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   412
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   413
lemma valid_path_join_eq [simp]:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   414
    "pathfinish g1 = pathstart g2 \<Longrightarrow> (valid_path(g1 +++ g2) \<longleftrightarrow> valid_path g1 \<and> valid_path g2)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   415
  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
   416
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   417
lemma has_path_integral_join:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   418
  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
   419
          "valid_path g1" "valid_path g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   420
    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
   421
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   422
  obtain s1 s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   423
    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
   424
      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
   425
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   426
    by (auto simp: valid_path_def piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   427
  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
   428
   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
   429
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   430
    by (auto simp: has_path_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   431
  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
   432
   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
   433
    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
   434
          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
   435
    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
   436
  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
   437
            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
   438
            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
   439
    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
   440
    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
   441
    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
   442
    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
   443
    using s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   444
    apply (auto simp: algebra_simps vector_derivative_works)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   445
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   446
  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
   447
            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
   448
            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
   449
    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
   450
    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
   451
    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
   452
    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
   453
    using s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   454
    apply (auto simp: algebra_simps vector_derivative_works)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   455
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   456
  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
   457
    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
   458
    using s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   459
    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
   460
    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
   461
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   462
  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
   463
    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
   464
    using s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   465
    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
   466
    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
   467
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   468
  ultimately
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   469
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   470
    apply (simp add: has_path_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   471
    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
   472
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   473
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   474
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   475
lemma path_integrable_joinI:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   476
  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
   477
          "valid_path g1" "valid_path g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   478
    shows "f path_integrable_on (g1 +++ g2)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   479
  using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   480
  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
   481
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   482
lemma path_integrable_joinD1:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   483
  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
   484
    shows "f path_integrable_on g1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   485
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   486
  obtain s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   487
    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
   488
    using assms by (auto simp: valid_path_def piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   489
  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
   490
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   491
    apply (auto simp: path_integrable_on)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   492
    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
   493
    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
   494
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   495
  then have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2))/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
   496
    by (force 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
   497
  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
   498
            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
   499
            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
   500
    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
   501
    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
   502
    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
   503
    using s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   504
    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
   505
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   506
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   507
    using s1
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   508
    apply (auto simp: path_integrable_on)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   509
    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
   510
    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
   511
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   512
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   513
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   514
lemma path_integrable_joinD2: (*FIXME: could combine these proofs*)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   515
  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
   516
    shows "f path_integrable_on g2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   517
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   518
  obtain s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   519
    where 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
   520
    using assms by (auto simp: valid_path_def piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   521
  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
   522
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   523
    apply (auto simp: path_integrable_on)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   524
    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
   525
    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
   526
    apply (simp add: image_affinity_atLeastAtMost_diff)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   527
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   528
  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
   529
                integrable_on {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   530
    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
   531
  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
   532
            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
   533
            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
   534
    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
   535
    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
   536
    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
   537
    using s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   538
    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
   539
                      vector_derivative_works add_divide_distrib)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   540
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   541
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   542
    using s2
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   543
    apply (auto simp: path_integrable_on)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   544
    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
   545
    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
   546
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   547
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   548
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   549
lemma path_integrable_join [simp]:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   550
  shows
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   551
    "\<lbrakk>valid_path g1; valid_path g2\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   552
     \<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
   553
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
   554
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   555
lemma path_integral_join [simp]:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   556
  shows
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   557
    "\<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
   558
        \<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
   559
  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
   560
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   561
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   562
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
   563
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   564
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
   565
  by (auto simp: shiftpath_def)
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 valid_path_shiftpath [intro]:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   568
  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
   569
    shows "valid_path(shiftpath a g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   570
  using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   571
  apply (auto simp: valid_path_def shiftpath_alt_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   572
  apply (rule piecewise_differentiable_cases)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   573
  apply (auto simp: algebra_simps)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   574
  apply (rule piecewise_differentiable_affine [of g 1 a, simplified o_def scaleR_one])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   575
  apply (auto simp: pathfinish_def pathstart_def elim: piecewise_differentiable_on_subset)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   576
  apply (rule piecewise_differentiable_affine [of g 1 "a-1", simplified o_def scaleR_one algebra_simps])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   577
  apply (auto simp: pathfinish_def pathstart_def elim: piecewise_differentiable_on_subset)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   578
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   579
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   580
lemma has_path_integral_shiftpath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   581
  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
   582
      and a: "a \<in> {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   583
    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
   584
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   585
  obtain s
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   586
    where s: "finite s" and g: "\<forall>x\<in>{0..1} - s. g differentiable at x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   587
    using assms by (auto simp: valid_path_def piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   588
  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
   589
    using assms by (auto simp: has_path_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   590
  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
   591
                    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
   592
    apply (rule has_integral_unique)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   593
    apply (subst add.commute)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   594
    apply (subst Integration.integral_combine)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   595
    using assms * integral_unique by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   596
  { fix x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   597
    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
   598
         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
   599
      unfolding shiftpath_def
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   600
      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
   601
        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
   602
      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
   603
       apply (intro derivative_eq_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   604
      using g
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   605
       apply (drule_tac x="x+a" in bspec)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   606
      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
   607
      done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   608
  } note vd1 = this
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   609
  { fix x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   610
    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
   611
          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
   612
      unfolding shiftpath_def
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   613
      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
   614
        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
   615
      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
   616
       apply (intro derivative_eq_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   617
      using g
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   618
      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
   619
      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
   620
      done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   621
  } note vd2 = this
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   622
  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
   623
    using * a   by (fastforce intro: integrable_subinterval_real)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   624
  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
   625
    apply (rule integrable_subinterval_real)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   626
    using * a by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   627
  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
   628
        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
   629
    apply (rule has_integral_spike_finite
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   630
             [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
   631
      using s apply blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   632
     using a apply (auto simp: algebra_simps vd1)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   633
     apply (force simp: shiftpath_def add.commute)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   634
    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
   635
    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
   636
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   637
  moreover
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   638
  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
   639
        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
   640
    apply (rule has_integral_spike_finite
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   641
             [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
   642
      using s apply blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   643
     using a apply (auto simp: algebra_simps vd2)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   644
     apply (force simp: shiftpath_def add.commute)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   645
    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
   646
    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
   647
    apply (simp add: algebra_simps)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   648
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   649
  ultimately show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   650
    using a
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   651
    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
   652
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   653
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   654
lemma has_path_integral_shiftpath_D:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   655
  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
   656
          "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
   657
    shows "(f has_path_integral i) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   658
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   659
  obtain s
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   660
    where s: "finite s" and g: "\<forall>x\<in>{0..1} - s. g differentiable at x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   661
    using assms by (auto simp: valid_path_def piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   662
  { fix x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   663
    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
   664
    then have gx: "g differentiable at x"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   665
      using g by auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   666
    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
   667
          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
   668
      apply (rule vector_derivative_at_within_ivl
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   669
                  [OF has_vector_derivative_transform_within_open
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   670
                      [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
   671
      using s g assms x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   672
      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
   673
                        vector_derivative_within_interior vector_derivative_works [symmetric])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   674
      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
   675
      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
   676
      done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   677
  } note vd = this
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   678
  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
   679
    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
   680
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   681
    apply (simp add: has_path_integral_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   682
    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
   683
    using s assms vd
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   684
    apply (auto simp: Path_Connected.shiftpath_shiftpath)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   685
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   686
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   687
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   688
lemma has_path_integral_shiftpath_eq:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   689
  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
   690
    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
   691
  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
   692
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   693
lemma path_integral_shiftpath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   694
  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
   695
    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
   696
   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
   697
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   698
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   699
subsection\<open>More about straight-line paths\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   700
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   701
lemma has_vector_derivative_linepath_within:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   702
    "(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
   703
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
   704
apply (rule derivative_eq_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   705
done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   706
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   707
lemma valid_path_linepath [iff]: "valid_path (linepath a b)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   708
  apply (simp add: valid_path_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   709
  apply (rule differentiable_on_imp_piecewise_differentiable)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   710
  apply (simp add: differentiable_on_def differentiable_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   711
  using has_vector_derivative_def has_vector_derivative_linepath_within by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   712
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   713
lemma vector_derivative_linepath_within:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   714
    "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
   715
  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
   716
  apply (auto simp: has_vector_derivative_linepath_within)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   717
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   718
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   719
lemma vector_derivative_linepath_at: "vector_derivative (linepath a b) (at x) = b - a"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   720
  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
   721
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   722
lemma has_path_integral_linepath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   723
  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
   724
         ((\<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
   725
  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
   726
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   727
lemma linepath_in_path:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   728
  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
   729
  by (auto simp: segment linepath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   730
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   731
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
   732
  by (auto simp: segment linepath_def)
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 linepath_in_convex_hull:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   735
    fixes x::real
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   736
    assumes a: "a \<in> convex hull s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   737
        and b: "b \<in> convex hull s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   738
        and x: "0\<le>x" "x\<le>1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   739
       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
   740
  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
   741
  using x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   742
  apply (auto simp: linepath_image_01 [symmetric])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   743
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   744
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   745
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
   746
  by (simp add: linepath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   747
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   748
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
   749
  by (simp add: linepath_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   750
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   751
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
   752
  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
   753
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   754
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
   755
  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
   756
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   757
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
   758
  by (simp add: has_path_integral_linepath)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   759
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   760
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
   761
  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
   762
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   763
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   764
subsection\<open>Relation to subpath construction\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   765
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   766
lemma valid_path_subpath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   767
  fixes g :: "real \<Rightarrow> 'a :: real_normed_vector"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   768
  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
   769
    shows "valid_path(subpath u v g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   770
proof (cases "v=u")
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   771
  case True
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   772
  then show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   773
    by (simp add: valid_path_def subpath_def differentiable_on_def differentiable_on_imp_piecewise_differentiable)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   774
next
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   775
  case False
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   776
  have "(g o (\<lambda>x. ((v-u) * x + u))) piecewise_differentiable_on {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   777
    apply (rule piecewise_differentiable_compose)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   778
      apply (simp add: differentiable_on_def differentiable_on_imp_piecewise_differentiable)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   779
     apply (simp add: image_affinity_atLeastAtMost)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   780
    using assms False
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   781
    apply (auto simp: algebra_simps valid_path_def piecewise_differentiable_on_subset)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   782
    apply (subst Int_commute)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   783
    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
   784
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   785
  then show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   786
    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
   787
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   788
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   789
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
   790
  by (simp add: has_path_integral subpath_def)
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_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
   793
  using has_path_integral_subpath_refl path_integrable_on_def by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   794
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   795
lemma path_integral_subpath_refl [simp]: "path_integral (subpath u u g) f = 0"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   796
  by (simp add: has_path_integral_subpath_refl path_integral_unique)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   797
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   798
lemma has_path_integral_subpath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   799
  assumes f: "f path_integrable_on g" and g: "valid_path g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   800
      and uv: "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   801
    shows "(f has_path_integral  integral {u..v} (\<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
   802
           (subpath u v g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   803
proof (cases "v=u")
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   804
  case True
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   805
  then show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   806
    using f   by (simp add: path_integrable_on_def subpath_def has_path_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   807
next
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   808
  case False
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   809
  obtain s where s: "\<And>x. x \<in> {0..1} - s \<Longrightarrow> g differentiable at x" and fs: "finite s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   810
    using g   by (auto simp: valid_path_def piecewise_differentiable_on_def) (blast intro: that)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   811
  have *: "((\<lambda>x. f (g ((v - u) * x + u)) * vector_derivative g (at ((v - u) * x + u)))
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   812
            has_integral (1 / (v - u)) * integral {u..v} (\<lambda>t. f (g t) * vector_derivative g (at t)))
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   813
           {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   814
    using f uv
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   815
    apply (simp add: path_integrable_on subpath_def has_path_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   816
    apply (drule integrable_on_subcbox [where a=u and b=v, simplified])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   817
    apply (simp_all add: has_integral_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   818
    apply (drule has_integral_affinity [where m="v-u" and c=u, simplified])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   819
    apply (simp_all add: False image_affinity_atLeastAtMost_div_diff scaleR_conv_of_real)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   820
    apply (simp add: divide_simps False)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   821
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   822
  { fix x
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   823
    have "x \<in> {0..1} \<Longrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   824
           x \<notin> (\<lambda>t. (v-u) *\<^sub>R t + u) -` s \<Longrightarrow>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   825
           vector_derivative (\<lambda>x. g ((v-u) * x + u)) (at x) = (v-u) *\<^sub>R vector_derivative g (at ((v-u) * x + u))"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   826
      apply (rule vector_derivative_at [OF vector_diff_chain_at [simplified o_def]])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   827
      apply (intro derivative_eq_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   828
      apply (cut_tac s [of "(v - u) * x + u"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   829
      using uv mult_left_le [of x "v-u"]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   830
      apply (auto simp:  vector_derivative_works)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   831
      done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   832
  } note vd = this
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   833
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   834
    apply (cut_tac has_integral_cmul [OF *, where c = "v-u"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   835
    using fs assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   836
    apply (simp add: False subpath_def has_path_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   837
    apply (rule_tac s = "(\<lambda>t. ((v-u) *\<^sub>R t + u)) -` s" in has_integral_spike_finite)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   838
    apply (auto simp: inj_on_def False finite_vimageI vd scaleR_conv_of_real)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   839
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   840
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   841
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   842
lemma path_integrable_subpath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   843
  assumes "f path_integrable_on g" "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
   844
    shows "f path_integrable_on (subpath u v g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   845
  apply (cases u v rule: linorder_class.le_cases)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   846
   apply (metis path_integrable_on_def has_path_integral_subpath [OF assms])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   847
  apply (subst reversepath_subpath [symmetric])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   848
  apply (rule path_integrable_reversepath)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   849
   using assms apply (blast intro: valid_path_subpath)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   850
  apply (simp add: path_integrable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   851
  using assms apply (blast intro: has_path_integral_subpath)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   852
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   853
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   854
lemma has_integral_integrable_integral: "(f has_integral i) s \<longleftrightarrow> f integrable_on s \<and> integral s f = i"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   855
  by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   856
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   857
lemma has_integral_path_integral_subpath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   858
  assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   859
    shows "(((\<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
   860
            has_integral  path_integral (subpath u v g) f) {u..v}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   861
  using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   862
  apply (auto simp: has_integral_integrable_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   863
  apply (rule integrable_on_subcbox [where a=u and b=v and s = "{0..1}", simplified])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   864
  apply (auto simp: path_integral_unique [OF has_path_integral_subpath] path_integrable_on)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   865
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   866
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   867
lemma path_integral_subpath_integral:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   868
  assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   869
    shows "path_integral (subpath u v g) f =
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   870
           integral {u..v} (\<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
   871
  using assms has_path_integral_subpath path_integral_unique by blast
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   872
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   873
lemma path_integral_subpath_combine_less:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   874
  assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "w \<in> {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   875
          "u<v" "v<w"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   876
    shows "path_integral (subpath u v g) f + path_integral (subpath v w g) f =
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   877
           path_integral (subpath u w g) f"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   878
  using assms apply (auto simp: path_integral_subpath_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   879
  apply (rule integral_combine, auto)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   880
  apply (rule integrable_on_subcbox [where a=u and b=w and s = "{0..1}", simplified])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   881
  apply (auto simp: path_integrable_on)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   882
  done
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 path_integral_subpath_combine:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   885
  assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "w \<in> {0..1}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   886
    shows "path_integral (subpath u v g) f + path_integral (subpath v w g) f =
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   887
           path_integral (subpath u w g) f"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   888
proof (cases "u\<noteq>v \<and> v\<noteq>w \<and> u\<noteq>w")
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   889
  case True
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   890
    have *: "subpath v u g = reversepath(subpath u v g) \<and>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   891
             subpath w u g = reversepath(subpath u w g) \<and>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   892
             subpath w v g = reversepath(subpath v w g)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   893
      by (auto simp: reversepath_subpath)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   894
    have "u < v \<and> v < w \<or>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   895
          u < w \<and> w < v \<or>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   896
          v < u \<and> u < w \<or>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   897
          v < w \<and> w < u \<or>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   898
          w < u \<and> u < v \<or>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   899
          w < v \<and> v < u"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   900
      using True assms by linarith
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   901
    with assms show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   902
      using path_integral_subpath_combine_less [of f g u v w]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   903
            path_integral_subpath_combine_less [of f g u w v]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   904
            path_integral_subpath_combine_less [of f g v u w]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   905
            path_integral_subpath_combine_less [of f g v w u]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   906
            path_integral_subpath_combine_less [of f g w u v]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   907
            path_integral_subpath_combine_less [of f g w v u]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   908
      apply simp
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   909
      apply (elim disjE)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   910
      apply (auto simp: * path_integral_reversepath path_integrable_subpath
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   911
                   valid_path_reversepath valid_path_subpath algebra_simps)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   912
      done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   913
next
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   914
  case False
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   915
  then show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   916
    apply (auto simp: path_integral_subpath_refl)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   917
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   918
    by (metis eq_neg_iff_add_eq_0 path_integrable_subpath path_integral_reversepath reversepath_subpath valid_path_subpath)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   919
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   920
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   921
lemma path_integral_integral:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   922
  shows "path_integral g f = integral {0..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
   923
  by (simp add: path_integral_def integral_def has_path_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   924
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   925
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   926
subsection\<open>Segments via convex hulls\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   927
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   928
lemma segments_subset_convex_hull:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   929
    "closed_segment a b \<subseteq> (convex hull {a,b,c})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   930
    "closed_segment a c \<subseteq> (convex hull {a,b,c})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   931
    "closed_segment b c \<subseteq> (convex hull {a,b,c})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   932
    "closed_segment b a \<subseteq> (convex hull {a,b,c})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   933
    "closed_segment c a \<subseteq> (convex hull {a,b,c})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   934
    "closed_segment c b \<subseteq> (convex hull {a,b,c})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   935
by (auto simp: segment_convex_hull linepath_of_real  elim!: rev_subsetD [OF _ hull_mono])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   936
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   937
lemma midpoints_in_convex_hull:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   938
  assumes "x \<in> convex hull s" "y \<in> convex hull s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   939
    shows "midpoint x y \<in> convex hull s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   940
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   941
  have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \<in> convex hull s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   942
    apply (rule mem_convex)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   943
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   944
    apply (auto simp: convex_convex_hull)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   945
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   946
  then show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   947
    by (simp add: midpoint_def algebra_simps)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   948
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   949
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   950
lemma convex_hull_subset:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   951
    "s \<subseteq> convex hull t \<Longrightarrow> convex hull s \<subseteq> convex hull t"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   952
  by (simp add: convex_convex_hull subset_hull)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   953
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   954
lemma not_in_interior_convex_hull_3:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   955
  fixes a :: "complex"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   956
  shows "a \<notin> interior(convex hull {a,b,c})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   957
        "b \<notin> interior(convex hull {a,b,c})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   958
        "c \<notin> interior(convex hull {a,b,c})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   959
  by (auto simp: card_insert_le_m1 not_in_interior_convex_hull)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   960
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   961
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   962
text\<open>Cauchy's theorem where there's a primitive\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   963
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   964
lemma path_integral_primitive_lemma:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   965
  fixes f :: "complex \<Rightarrow> complex" and g :: "real \<Rightarrow> complex"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   966
  assumes "a \<le> b"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   967
      and "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   968
      and "g piecewise_differentiable_on {a..b}"  "\<And>x. x \<in> {a..b} \<Longrightarrow> g x \<in> s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   969
    shows "((\<lambda>x. f'(g x) * vector_derivative g (at x within {a..b}))
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   970
             has_integral (f(g b) - f(g a))) {a..b}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   971
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   972
  obtain k where k: "finite k" "\<forall>x\<in>{a..b} - k. g differentiable at x" and cg: "continuous_on {a..b} g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   973
    using assms by (auto simp: piecewise_differentiable_on_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   974
  have cfg: "continuous_on {a..b} (\<lambda>x. f (g x))"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   975
    apply (rule continuous_on_compose [OF cg, unfolded o_def])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   976
    using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   977
    apply (metis complex_differentiable_def complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   978
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   979
  { fix x::real
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   980
    assume a: "a < x" and b: "x < b" and xk: "x \<notin> k"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   981
    then have "g differentiable at x within {a..b}"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   982
      using k by (simp add: differentiable_at_withinI)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   983
    then have "(g has_vector_derivative vector_derivative g (at x within {a..b})) (at x within {a..b})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   984
      by (simp add: vector_derivative_works has_field_derivative_def scaleR_conv_of_real)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   985
    then have gdiff: "(g has_derivative (\<lambda>u. u * vector_derivative g (at x within {a..b}))) (at x within {a..b})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   986
      by (simp add: has_vector_derivative_def scaleR_conv_of_real)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   987
    have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {a..b})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   988
      using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   989
    then have fdiff: "(f has_derivative op * (f' (g x))) (at (g x) within g ` {a..b})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   990
      by (simp add: has_field_derivative_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   991
    have "((\<lambda>x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {a..b})) (at x within {a..b})"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   992
      using diff_chain_within [OF gdiff fdiff]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   993
      by (simp add: has_vector_derivative_def scaleR_conv_of_real o_def mult_ac)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   994
  } note * = this
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   995
  show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   996
    apply (rule fundamental_theorem_of_calculus_interior_strong)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   997
    using k assms cfg *
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   998
    apply (auto simp: at_within_closed_interval)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   999
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1000
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1001
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1002
lemma path_integral_primitive:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1003
  assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1004
      and "valid_path g" "path_image g \<subseteq> s"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1005
    shows "(f' has_path_integral (f(pathfinish g) - f(pathstart g))) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1006
  using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1007
  apply (simp add: valid_path_def path_image_def pathfinish_def pathstart_def has_path_integral_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1008
  apply (auto intro!: path_integral_primitive_lemma [of 0 1 s])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1009
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1010
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1011
corollary Cauchy_theorem_primitive:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1012
  assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1013
      and "valid_path g"  "path_image g \<subseteq> s" "pathfinish g = pathstart g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1014
    shows "(f' has_path_integral 0) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1015
  using assms
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1016
  by (metis diff_self path_integral_primitive)
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
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1019
text\<open>Existence of path integral for continuous function\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1020
lemma path_integrable_continuous_linepath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1021
  assumes "continuous_on (closed_segment a b) f"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1022
  shows "f path_integrable_on (linepath a b)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1023
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1024
  have "continuous_on {0..1} ((\<lambda>x. f x * (b - a)) o linepath a b)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1025
    apply (rule continuous_on_compose [OF continuous_on_linepath], simp add: linepath_image_01)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1026
    apply (rule continuous_intros | simp add: assms)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1027
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1028
  then show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1029
    apply (simp add: path_integrable_on_def has_path_integral_def integrable_on_def [symmetric])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1030
    apply (rule integrable_continuous [of 0 "1::real", simplified])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1031
    apply (rule continuous_on_eq [where f = "\<lambda>x. f(linepath a b x)*(b - a)"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1032
    apply (auto simp: vector_derivative_linepath_within)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1033
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1034
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1035
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1036
lemma has_field_der_id: "((\<lambda>x. x\<^sup>2 / 2) has_field_derivative x) (at x)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1037
  by (rule has_derivative_imp_has_field_derivative)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1038
     (rule derivative_intros | simp)+
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1039
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1040
lemma path_integral_id [simp]: "path_integral (linepath a b) (\<lambda>y. y) = (b^2 - a^2)/2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1041
  apply (rule path_integral_unique)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1042
  using path_integral_primitive [of UNIV "\<lambda>x. x^2/2" "\<lambda>x. x" "linepath a b"]
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1043
  apply (auto simp: field_simps has_field_der_id)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1044
  done
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 path_integrable_on_const [iff]: "(\<lambda>x. c) path_integrable_on (linepath a b)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1047
  by (simp add: continuous_on_const path_integrable_continuous_linepath)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1048
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1049
lemma path_integrable_on_id [iff]: "(\<lambda>x. x) path_integrable_on (linepath a b)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1050
  by (simp add: continuous_on_id path_integrable_continuous_linepath)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1051
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
subsection\<open>Arithmetical combining theorems\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1054
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1055
lemma has_path_integral_neg:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1056
    "(f has_path_integral i) g \<Longrightarrow> ((\<lambda>x. -(f x)) has_path_integral (-i)) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1057
  by (simp add: has_integral_neg has_path_integral_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1058
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1059
lemma has_path_integral_add:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1060
    "\<lbrakk>(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1061
     \<Longrightarrow> ((\<lambda>x. f1 x + f2 x) has_path_integral (i1 + i2)) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1062
  by (simp add: has_integral_add has_path_integral_def algebra_simps)
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 has_path_integral_diff:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1065
  shows "\<lbrakk>(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1066
         \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) has_path_integral (i1 - i2)) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1067
  by (simp add: has_integral_sub has_path_integral_def algebra_simps)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1068
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1069
lemma has_path_integral_lmul:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1070
  shows "(f has_path_integral i) g
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1071
         \<Longrightarrow> ((\<lambda>x. c * (f x)) has_path_integral (c*i)) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1072
apply (simp add: has_path_integral_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1073
apply (drule has_integral_mult_right)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1074
apply (simp add: algebra_simps)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1075
done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1076
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1077
lemma has_path_integral_rmul:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1078
  shows "(f has_path_integral i) g \<Longrightarrow> ((\<lambda>x. (f x) * c) has_path_integral (i*c)) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1079
apply (drule has_path_integral_lmul)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1080
apply (simp add: mult.commute)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1081
done
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
lemma has_path_integral_div:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1084
  shows "(f has_path_integral i) g \<Longrightarrow> ((\<lambda>x. f x/c) has_path_integral (i/c)) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1085
  by (simp add: field_class.field_divide_inverse) (metis has_path_integral_rmul)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1086
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1087
lemma has_path_integral_eq:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1088
  shows
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1089
    "\<lbrakk>(f has_path_integral y) p; \<And>x. x \<in> path_image p \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> (g has_path_integral y) p"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1090
apply (simp add: path_image_def has_path_integral_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1091
by (metis (no_types, lifting) image_eqI has_integral_eq)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1092
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1093
lemma has_path_integral_bound_linepath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1094
  assumes "(f has_path_integral i) (linepath a b)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1095
          "0 \<le> B" "\<And>x. x \<in> closed_segment a b \<Longrightarrow> norm(f x) \<le> B"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1096
    shows "norm i \<le> B * norm(b - a)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1097
proof -
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1098
  { fix x::real
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1099
    assume x: "0 \<le> x" "x \<le> 1"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1100
  have "norm (f (linepath a b x)) *
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1101
        norm (vector_derivative (linepath a b) (at x within {0..1})) \<le> B * norm (b - a)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1102
    by (auto intro: mult_mono simp: assms linepath_in_path of_real_linepath vector_derivative_linepath_within x)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1103
  } note * = this
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1104
  have "norm i \<le> (B * norm (b - a)) * content (cbox 0 (1::real))"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1105
    apply (rule has_integral_bound
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1106
       [of _ "\<lambda>x. f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})"])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1107
    using assms * unfolding has_path_integral_def
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1108
    apply (auto simp: norm_mult)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1109
    done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1110
  then show ?thesis
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1111
    by (auto simp: content_real)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1112
qed
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1113
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1114
(*UNUSED
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1115
lemma has_path_integral_bound_linepath_strong:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1116
  fixes a :: real and f :: "complex \<Rightarrow> real"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1117
  assumes "(f has_path_integral i) (linepath a b)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1118
          "finite k"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1119
          "0 \<le> B" "\<And>x::real. x \<in> closed_segment a b - k \<Longrightarrow> norm(f x) \<le> B"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1120
    shows "norm i \<le> B*norm(b - a)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1121
*)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1122
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1123
lemma has_path_integral_const_linepath: "((\<lambda>x. c) has_path_integral c*(b - a))(linepath a b)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1124
  unfolding has_path_integral_linepath
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1125
  by (metis content_real diff_0_right has_integral_const_real lambda_one of_real_1 scaleR_conv_of_real zero_le_one)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1126
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1127
lemma has_path_integral_0: "((\<lambda>x. 0) has_path_integral 0) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1128
  by (simp add: has_path_integral_def)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1129
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1130
lemma has_path_integral_is_0:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1131
    "(\<And>z. z \<in> path_image g \<Longrightarrow> f z = 0) \<Longrightarrow> (f has_path_integral 0) g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1132
  by (rule has_path_integral_eq [OF has_path_integral_0]) auto
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1133
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1134
lemma has_path_integral_setsum:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1135
    "\<lbrakk>finite s; \<And>a. a \<in> s \<Longrightarrow> (f a has_path_integral i a) p\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1136
     \<Longrightarrow> ((\<lambda>x. setsum (\<lambda>a. f a x) s) has_path_integral setsum i s) p"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1137
  by (induction s rule: finite_induct) (auto simp: has_path_integral_0 has_path_integral_add)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1138
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1139
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1140
subsection \<open>Operations on path integrals\<close>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1141
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1142
lemma path_integral_const_linepath [simp]: "path_integral (linepath a b) (\<lambda>x. c) = c*(b - a)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1143
  by (rule path_integral_unique [OF has_path_integral_const_linepath])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1144
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1145
lemma path_integral_neg:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1146
    "f path_integrable_on g \<Longrightarrow> path_integral g (\<lambda>x. -(f x)) = -(path_integral g f)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1147
  by (simp add: path_integral_unique has_path_integral_integral has_path_integral_neg)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1148
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1149
lemma path_integral_add:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1150
    "f1 path_integrable_on g \<Longrightarrow> f2 path_integrable_on g \<Longrightarrow> path_integral g (\<lambda>x. f1 x + f2 x) =
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1151
                path_integral g f1 + path_integral g f2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1152
  by (simp add: path_integral_unique has_path_integral_integral has_path_integral_add)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1153
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1154
lemma path_integral_diff:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1155
    "f1 path_integrable_on g \<Longrightarrow> f2 path_integrable_on g \<Longrightarrow> path_integral g (\<lambda>x. f1 x - f2 x) =
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1156
                path_integral g f1 - path_integral g f2"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1157
  by (simp add: path_integral_unique has_path_integral_integral has_path_integral_diff)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1158
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1159
lemma path_integral_lmul:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1160
  shows "f path_integrable_on g
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1161
           \<Longrightarrow> path_integral g (\<lambda>x. c * f x) = c*path_integral g f"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1162
  by (simp add: path_integral_unique has_path_integral_integral has_path_integral_lmul)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1163
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1164
lemma path_integral_rmul:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1165
  shows "f path_integrable_on g
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1166
        \<Longrightarrow> path_integral g (\<lambda>x. f x * c) = path_integral g f * c"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1167
  by (simp add: path_integral_unique has_path_integral_integral has_path_integral_rmul)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1168
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1169
lemma path_integral_div:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1170
  shows "f path_integrable_on g
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1171
        \<Longrightarrow> path_integral g (\<lambda>x. f x / c) = path_integral g f / c"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1172
  by (simp add: path_integral_unique has_path_integral_integral has_path_integral_div)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1173
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1174
lemma path_integral_eq:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1175
    "(\<And>x. x \<in> path_image p \<Longrightarrow> f x = g x) \<Longrightarrow> path_integral p f = path_integral p g"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1176
  by (simp add: path_integral_def) (metis has_path_integral_eq)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1177
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1178
lemma path_integral_eq_0:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1179
    "(\<And>z. z \<in> path_image g \<Longrightarrow> f z = 0) \<Longrightarrow> path_integral g f = 0"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1180
  by (simp add: has_path_integral_is_0 path_integral_unique)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1181
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1182
lemma path_integral_bound_linepath:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1183
  shows
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1184
    "\<lbrakk>f path_integrable_on (linepath a b);
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1185
      0 \<le> B; \<And>x. x \<in> closed_segment a b \<Longrightarrow> norm(f x) \<le> B\<rbrakk>
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1186
     \<Longrightarrow> norm(path_integral (linepath a b) f) \<le> B*norm(b - a)"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1187
  apply (rule has_path_integral_bound_linepath [of f])
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1188
  apply (auto simp: has_path_integral_integral)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1189
  done
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1190
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1191
lemma path_integral_0: "path_integral g (\<lambda>x. 0) = 0"
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1192
  by (simp add: path_integral_unique has_path_integral_0)
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1193
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1194
lemma path_integral_setsum:
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1195
    "\<lbrakk>finite s; \<And>a. a \<in> s \<Longrightarrow> (f a) path_integrable_on p\<rbrakk>