Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Bille.loaded2.jpg Sprache: Isabelle

Original von: Isabelle^©

section \<open>Contour integration\<close>
theory Contour_Integration
  imports "HOL-Analysis.Analysis"
begin

lemma lhopital_complex_simple:
  assumes "(f has_field_derivative f') (at z)"
  assumes "(g has_field_derivative g') (at z)"
  assumes "f z = 0" "g z = 0" "g' \ 0" "f' / g' = c"
  shows   "((\w. f w / g w) \ c) (at z)"
proof -
  have "eventually (\w. w \ z) (at z)"
    by (auto simp: eventually_at_filter)
  hence "eventually (\w. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z)) = f w / g w) (at z)"
    by eventually_elim (simp add: assms field_split_simps)
  moreover have "((\w. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z))) \ f' / g') (at z)"
    by (intro tendsto_divide has_field_derivativeD assms)
  ultimately have "((\w. f w / g w) \ f' / g') (at z)"
    by (blast intro: Lim_transform_eventually)
  with assms show ?thesis by simp
qed

subsection\<open>Definition\<close>

text\<open>
  This definition is for complex numbers only, and does not generalise to
  line integrals in a vector field
\<close>

definition\<^marker>\<open>tag important\<close> has_contour_integral :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool"
           (infixr "has'_contour'_integral" 50)
  where "(f has_contour_integral i) g \
           ((\<lambda>x. f(g x) * vector_derivative g (at x within {0..1}))
            has_integral i) {0..1}"

definition\<^marker>\<open>tag important\<close> contour_integrable_on
           (infixr "contour'_integrable'_on" 50)
  where "f contour_integrable_on g \ \i. (f has_contour_integral i) g"

definition\<^marker>\<open>tag important\<close> contour_integral
  where "contour_integral g f \ SOME i. (f has_contour_integral i) g \ \ f contour_integrable_on g \ i=0"

lemma not_integrable_contour_integral: "\ f contour_integrable_on g \ contour_integral g f = 0"
  unfolding contour_integrable_on_def contour_integral_def by blast

lemma contour_integral_unique: "(f has_contour_integral i) g \ contour_integral g f = i"
  apply (simp add: contour_integral_def has_contour_integral_def contour_integrable_on_def)
  using has_integral_unique by blast

lemma has_contour_integral_eqpath:
     "\(f has_contour_integral y) p; f contour_integrable_on \;
       contour_integral p f = contour_integral \<gamma> f\<rbrakk>
      \<Longrightarrow> (f has_contour_integral y) \<gamma>"
using contour_integrable_on_def contour_integral_unique by auto

lemma has_contour_integral_integral:
    "f contour_integrable_on i \ (f has_contour_integral (contour_integral i f)) i"
  by (metis contour_integral_unique contour_integrable_on_def)

lemma has_contour_integral_unique:
    "(f has_contour_integral i) g \ (f has_contour_integral j) g \ i = j"
  using has_integral_unique
  by (auto simp: has_contour_integral_def)

lemma has_contour_integral_integrable: "(f has_contour_integral i) g \ f contour_integrable_on g"
  using contour_integrable_on_def by blast

text\<open>Show that we can forget about the localized derivative.\<close>

lemma has_integral_localized_vector_derivative:
    "((\x. f (g x) * vector_derivative g (at x within {a..b})) has_integral i) {a..b} \
     ((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {a..b}"
proof -
  have *: "{a..b} - {a,b} = interior {a..b}"
    by (simp add: atLeastAtMost_diff_ends)
  show ?thesis
    by (rule has_integral_spike_eq [of "{a,b}"]) (auto simp: at_within_interior [of _ "{a..b}"])
qed

lemma integrable_on_localized_vector_derivative:
    "(\x. f (g x) * vector_derivative g (at x within {a..b})) integrable_on {a..b} \
     (\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on {a..b}"
  by (simp add: integrable_on_def has_integral_localized_vector_derivative)

lemma has_contour_integral:
     "(f has_contour_integral i) g \
      ((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}"
  by (simp add: has_integral_localized_vector_derivative has_contour_integral_def)

lemma contour_integrable_on:
     "f contour_integrable_on g \
      (\<lambda>t. f(g t) * vector_derivative g (at t)) integrable_on {0..1}"
  by (simp add: has_contour_integral integrable_on_def contour_integrable_on_def)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Reversing a path\<close>

lemma has_contour_integral_reversepath:
  assumes "valid_path g" and f: "(f has_contour_integral i) g"
    shows "(f has_contour_integral (-i)) (reversepath g)"
proof -
  { fix S x
    assume xs: "g C1_differentiable_on ({0..1} - S)" "x \ (-) 1 ` S" "0 \ x" "x \ 1"
    have "vector_derivative (\x. g (1 - x)) (at x within {0..1}) =
            - vector_derivative g (at (1 - x) within {0..1})"
    proof -
      obtain f' where f': "(g has_vector_derivative f') (at (1 - x))"
        using xs
        by (force simp: has_vector_derivative_def C1_differentiable_on_def)
      have "(g \ (\x. 1 - x) has_vector_derivative -1 *\<^sub>R f') (at x)"
        by (intro vector_diff_chain_within has_vector_derivative_at_within [OF f'] derivative_eq_intros | simp)+
      then have mf': "((\x. g (1 - x)) has_vector_derivative -f') (at x)"
        by (simp add: o_def)
      show ?thesis
        using xs
        by (auto simp: vector_derivative_at_within_ivl [OF mf'] vector_derivative_at_within_ivl [OF f'])
    qed
  } note * = this
  obtain S where S: "continuous_on {0..1} g" "finite S" "g C1_differentiable_on {0..1} - S"
    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
  have "((\x. - (f (g (1 - x)) * vector_derivative g (at (1 - x) within {0..1}))) has_integral -i)
       {0..1}"
    using has_integral_affinity01 [where m= "-1" and c=1, OF f [unfolded has_contour_integral_def]]
    by (simp add: has_integral_neg)
  then show ?thesis
    using S
    unfolding reversepath_def has_contour_integral_def
    by (rule_tac S = "(\x. 1 - x) ` S" in has_integral_spike_finite) (auto simp: *)
qed

lemma contour_integrable_reversepath:
    "valid_path g \ f contour_integrable_on g \ f contour_integrable_on (reversepath g)"
  using has_contour_integral_reversepath contour_integrable_on_def by blast

lemma contour_integrable_reversepath_eq:
    "valid_path g \ (f contour_integrable_on (reversepath g) \ f contour_integrable_on g)"
  using contour_integrable_reversepath valid_path_reversepath by fastforce

lemma contour_integral_reversepath:
  assumes "valid_path g"
    shows "contour_integral (reversepath g) f = - (contour_integral g f)"
proof (cases "f contour_integrable_on g")
  case True then show ?thesis
    by (simp add: assms contour_integral_unique has_contour_integral_integral has_contour_integral_reversepath)
next
  case False then have "\ f contour_integrable_on (reversepath g)"
    by (simp add: assms contour_integrable_reversepath_eq)
  with False show ?thesis by (simp add: not_integrable_contour_integral)
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Joining two paths together\<close>

lemma has_contour_integral_join:
  assumes "(f has_contour_integral i1) g1" "(f has_contour_integral i2) g2"
          "valid_path g1" "valid_path g2"
    shows "(f has_contour_integral (i1 + i2)) (g1 +++ g2)"
proof -
  obtain s1 s2
    where s1: "finite s1" "\x\{0..1} - s1. g1 differentiable at x"
      and s2: "finite s2" "\x\{0..1} - s2. g2 differentiable at x"
    using assms
    by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
  have 1: "((\x. f (g1 x) * vector_derivative g1 (at x)) has_integral i1) {0..1}"
   and 2: "((\x. f (g2 x) * vector_derivative g2 (at x)) has_integral i2) {0..1}"
    using assms
    by (auto simp: has_contour_integral)
  have i1: "((\x. (2*f (g1 (2*x))) * vector_derivative g1 (at (2*x))) has_integral i1) {0..1/2}"
   and i2: "((\x. (2*f (g2 (2*x - 1))) * vector_derivative g2 (at (2*x - 1))) has_integral i2) {1/2..1}"
    using has_integral_affinity01 [OF 1, where m= 2 and c=0, THEN has_integral_cmul [where c=2]]
          has_integral_affinity01 [OF 2, where m= 2 and c="-1", THEN has_integral_cmul [where c=2]]
    by (simp_all only: image_affinity_atLeastAtMost_div_diff, simp_all add: scaleR_conv_of_real mult_ac)
  have g1: "vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
            2 *\<^sub>R vector_derivative g1 (at (z*2))"
      if "0 \ z" "z*2 < 1" "z*2 \ s1" for z
  proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
    show "0 < \z - 1/2\"
      using that by auto
    have "((*) 2 has_vector_derivative 2) (at z)"
      by (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
    moreover have "(g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (2 * z))"
      using s1 that by (auto simp: algebra_simps vector_derivative_works)
    ultimately
    show "((\x. g1 (2 * x)) has_vector_derivative 2 *\<^sub>R vector_derivative g1 (at (z * 2))) (at z)"
      by (intro vector_diff_chain_at [simplified o_def])
  qed (use that in \<open>simp_all add: dist_real_def abs_if split: if_split_asm\<close>)

  have g2: "vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
            2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))"
           if "1 < z*2" "z \ 1" "z*2 - 1 \ s2" for z
  proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
    show "0 < \z - 1/2\"
      using that by auto
    have "((\x. 2 * x - 1) has_vector_derivative 2) (at z)"
      by (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
    moreover have "(g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (2 * z - 1))"
      using s2 that by (auto simp: algebra_simps vector_derivative_works)
    ultimately
    show "((\x. g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))) (at z)"
      by (intro vector_diff_chain_at [simplified o_def])
  qed (use that in \<open>simp_all add: dist_real_def abs_if split: if_split_asm\<close>)

  have "((\x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i1) {0..1/2}"
  proof (rule has_integral_spike_finite [OF _ _ i1])
    show "finite (insert (1/2) ((*) 2 -` s1))"
      using s1 by (force intro: finite_vimageI [where h = "(*)2"] inj_onI)
  qed (auto simp add: joinpaths_def scaleR_conv_of_real mult_ac g1)
  moreover have "((\x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i2) {1/2..1}"
  proof (rule has_integral_spike_finite [OF _ _ i2])
    show "finite (insert (1/2) ((\x. 2 * x - 1) -` s2))"
      using s2 by (force intro: finite_vimageI [where h = "\x. 2*x-1"] inj_onI)
  qed (auto simp add: joinpaths_def scaleR_conv_of_real mult_ac g2)
  ultimately
  show ?thesis
    by (simp add: has_contour_integral has_integral_combine [where c = "1/2"])
qed

lemma contour_integrable_joinI:
  assumes "f contour_integrable_on g1" "f contour_integrable_on g2"
          "valid_path g1" "valid_path g2"
    shows "f contour_integrable_on (g1 +++ g2)"
  using assms
  by (meson has_contour_integral_join contour_integrable_on_def)

lemma contour_integrable_joinD1:
  assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g1"
    shows "f contour_integrable_on g1"
proof -
  obtain s1
    where s1: "finite s1" "\x\{0..1} - s1. g1 differentiable at x"
    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
  have "(\x. f ((g1 +++ g2) (x/2)) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}"
    using assms integrable_affinity [of _ 0 "1/2" "1/2" 0] integrable_on_subcbox [where a=0 and b="1/2"]
    by (fastforce simp: contour_integrable_on)
  then have *: "(\x. (f ((g1 +++ g2) (x/2))/2) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}"
    by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
  have g1: "vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) =
            2 *\<^sub>R vector_derivative g1 (at z)"
    if "0 < z" "z < 1" "z \ s1" for z
  proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
    show "0 < \(z - 1)/2\"
      using that by auto
    have \<section>: "((\<lambda>x. x * 2) has_vector_derivative 2) (at (z/2))"
      using s1 by (auto simp: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
    have "(g1 has_vector_derivative vector_derivative g1 (at z)) (at z)"
      using s1 that by (auto simp: vector_derivative_works)
    then show "((\x. g1 (2 * x)) has_vector_derivative 2 *\<^sub>R vector_derivative g1 (at z)) (at (z/2))"
      using vector_diff_chain_at [OF \<section>] by (auto simp: field_simps o_def)
  qed (use that in \<open>simp_all add: field_simps dist_real_def abs_if split: if_split_asm\<close>)
  have fin01: "finite ({0, 1} \ s1)"
    by (simp add: s1)
  show ?thesis
    unfolding contour_integrable_on
    by (intro integrable_spike_finite [OF fin01 _ *]) (auto simp: joinpaths_def scaleR_conv_of_real g1)
qed

lemma contour_integrable_joinD2:
  assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g2"
    shows "f contour_integrable_on g2"
proof -
  obtain s2
    where s2: "finite s2" "\x\{0..1} - s2. g2 differentiable at x"
    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
  have "(\x. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}"
    using assms integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2"]
                integrable_on_subcbox [where a="1/2" and b=1]
    by (fastforce simp: contour_integrable_on image_affinity_atLeastAtMost_diff)
  then have *: "(\x. (f ((g1 +++ g2) (x/2 + 1/2))/2) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2)))
                integrable_on {0..1}"
    by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
  have g2: "vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2+1/2)) =
            2 *\<^sub>R vector_derivative g2 (at z)"
        if "0 < z" "z < 1" "z \ s2" for z
  proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
    show "0 < \z/2\"
      using that by auto
    have \<section>: "((\<lambda>x. x * 2 - 1) has_vector_derivative 2) (at ((1 + z)/2))"
      using s2 by (auto simp: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
    have "(g2 has_vector_derivative vector_derivative g2 (at z)) (at z)"
      using s2 that by (auto simp: vector_derivative_works)
    then show "((\x. g2 (2*x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at z)) (at (z/2 + 1/2))"
      using vector_diff_chain_at [OF \<section>] by (auto simp: field_simps o_def)
  qed (use that in \<open>simp_all add: field_simps dist_real_def abs_if split: if_split_asm\<close>)
  have fin01: "finite ({0, 1} \ s2)"
    by (simp add: s2)
  show ?thesis
    unfolding contour_integrable_on
    by (intro integrable_spike_finite [OF fin01 _ *]) (auto simp: joinpaths_def scaleR_conv_of_real g2)
qed

lemma contour_integrable_join [simp]:
    "\valid_path g1; valid_path g2\
     \<Longrightarrow> f contour_integrable_on (g1 +++ g2) \<longleftrightarrow> f contour_integrable_on g1 \<and> f contour_integrable_on g2"
using contour_integrable_joinD1 contour_integrable_joinD2 contour_integrable_joinI by blast

lemma contour_integral_join [simp]:
    "\f contour_integrable_on g1; f contour_integrable_on g2; valid_path g1; valid_path g2\
        \<Longrightarrow> contour_integral (g1 +++ g2) f = contour_integral g1 f + contour_integral g2 f"
  by (simp add: has_contour_integral_integral has_contour_integral_join contour_integral_unique)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Shifting the starting point of a (closed) path\<close>

lemma has_contour_integral_shiftpath:
  assumes f: "(f has_contour_integral i) g" "valid_path g"
      and a: "a \ {0..1}"
    shows "(f has_contour_integral i) (shiftpath a g)"
proof -
  obtain S
    where S: "finite S" and g: "\x\{0..1} - S. g differentiable at x"
    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
  have *: "((\x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}"
    using assms by (auto simp: has_contour_integral)
  then have i: "i = integral {a..1} (\x. f (g x) * vector_derivative g (at x)) +
                    integral {0..a} (\<lambda>x. f (g x) * vector_derivative g (at x))"
    apply (rule has_integral_unique)
    apply (subst add.commute)
    apply (subst Henstock_Kurzweil_Integration.integral_combine)
    using assms * integral_unique by auto

  have vd1: "vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a))"
    if "0 \ x" "x + a < 1" "x \ (\x. x - a) ` S" for x
    unfolding shiftpath_def
  proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
    have "((\x. g (x + a)) has_vector_derivative vector_derivative g (at (a + x))) (at x)"
    proof (rule vector_diff_chain_at [of _ 1, simplified o_def scaleR_one])
      show "((\x. x + a) has_vector_derivative 1) (at x)"
        by (rule derivative_eq_intros | simp)+
      have "g differentiable at (x + a)"
        using g a that by force
      then show "(g has_vector_derivative vector_derivative g (at (a + x))) (at (x + a))"
        by (metis add.commute vector_derivative_works)
    qed
    then
    show "((\x. g (a + x)) has_vector_derivative vector_derivative g (at (x + a))) (at x)"
      by (auto simp: field_simps)
    show "0 < dist (1 - a) x"
      using that by auto
  qed (use that in \<open>auto simp: dist_real_def\<close>)

  have vd2: "vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a - 1))"
    if "x \ 1" "1 < x + a" "x \ (\x. x - a + 1) ` S" for x
    unfolding shiftpath_def
  proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
    have "((\x. g (x + a - 1)) has_vector_derivative vector_derivative g (at (a+x-1))) (at x)"
    proof (rule vector_diff_chain_at [of _ 1, simplified o_def scaleR_one])
      show "((\x. x + a - 1) has_vector_derivative 1) (at x)"
        by (rule derivative_eq_intros | simp)+
      have "g differentiable at (x+a-1)"
        using g a that by force
      then show "(g has_vector_derivative vector_derivative g (at (a+x-1))) (at (x + a - 1))"
        by (metis add.commute vector_derivative_works)
    qed
    then show "((\x. g (a + x - 1)) has_vector_derivative vector_derivative g (at (x + a - 1))) (at x)"
      by (auto simp: field_simps)
    show "0 < dist (1 - a) x"
      using that by auto
  qed (use that in \<open>auto simp: dist_real_def\<close>)

  have va1: "(\x. f (g x) * vector_derivative g (at x)) integrable_on ({a..1})"
    using * a   by (fastforce intro: integrable_subinterval_real)
  have v0a: "(\x. f (g x) * vector_derivative g (at x)) integrable_on ({0..a})"
    using * a by (force intro: integrable_subinterval_real)
  have "finite ({1 - a} \ (\x. x - a) ` S)"
    using S by blast
  then have "((\x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x))
        has_integral integral {a..1} (\<lambda>x. f (g x) * vector_derivative g (at x)))  {0..1 - a}"
    apply (rule has_integral_spike_finite
        [where f = "\x. f(g(a+x)) * vector_derivative g (at(a+x))"])
    subgoal
      using a by (simp add: vd1) (force simp: shiftpath_def add.commute)
    subgoal
      using has_integral_affinity [where m=1 and c=a] integrable_integral [OF va1]
      by (force simp add: add.commute)
    done
  moreover
  have "finite ({1 - a} \ (\x. x - a + 1) ` S)"
    using S by blast
  then have "((\x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x))
             has_integral  integral {0..a} (\<lambda>x. f (g x) * vector_derivative g (at x)))  {1 - a..1}"
    apply (rule has_integral_spike_finite
        [where f = "\x. f(g(a+x-1)) * vector_derivative g (at(a+x-1))"])
    subgoal
      using a by (simp add: vd2) (force simp: shiftpath_def add.commute)
    subgoal
      using has_integral_affinity [where m=1 and c="a-1", simplified, OF integrable_integral [OF v0a]]
      by (force simp add: algebra_simps)
    done
  ultimately show ?thesis
    using a
    by (auto simp: i has_contour_integral intro: has_integral_combine [where c = "1-a"])
qed

lemma has_contour_integral_shiftpath_D:
  assumes "(f has_contour_integral i) (shiftpath a g)"
          "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}"
    shows "(f has_contour_integral i) g"
proof -
  obtain S
    where S: "finite S" and g: "\x\{0..1} - S. g differentiable at x"
    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
  { fix x
    assume x: "0 < x" "x < 1" "x \ S"
    then have gx: "g differentiable at x"
      using g by auto
    have \<section>: "shiftpath (1 - a) (shiftpath a g) differentiable at x"
      using assms x
      by (intro differentiable_transform_within [OF gx, of "min x (1-x)"])
         (auto simp: dist_real_def shiftpath_shiftpath abs_if split: if_split_asm)
    have "vector_derivative g (at x within {0..1}) =
          vector_derivative (shiftpath (1 - a) (shiftpath a g)) (at x within {0..1})"
      apply (rule vector_derivative_at_within_ivl
                  [OF has_vector_derivative_transform_within_open
                      [where f = "(shiftpath (1 - a) (shiftpath a g))" and S = "{0<..<1}-S"]])
      using S assms x \<section>
      apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath
                        at_within_interior [of _ "{0..1}"] vector_derivative_works [symmetric])
      done
  } note vd = this
  have fi: "(f has_contour_integral i) (shiftpath (1 - a) (shiftpath a g))"
    using assms  by (auto intro!: has_contour_integral_shiftpath)
  show ?thesis
    unfolding has_contour_integral_def
  proof (rule has_integral_spike_finite [of "{0,1} \ S", OF _ _ fi [unfolded has_contour_integral_def]])
    show "finite ({0, 1} \ S)"
      by (simp add: S)
  qed (use S assms vd in \<open>auto simp: shiftpath_shiftpath\<close>)
qed

lemma has_contour_integral_shiftpath_eq:
  assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}"
    shows "(f has_contour_integral i) (shiftpath a g) \ (f has_contour_integral i) g"
  using assms has_contour_integral_shiftpath has_contour_integral_shiftpath_D by blast

lemma contour_integrable_on_shiftpath_eq:
  assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}"
    shows "f contour_integrable_on (shiftpath a g) \ f contour_integrable_on g"
using assms contour_integrable_on_def has_contour_integral_shiftpath_eq by auto

lemma contour_integral_shiftpath:
  assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}"
    shows "contour_integral (shiftpath a g) f = contour_integral g f"
   using assms
   by (simp add: contour_integral_def contour_integrable_on_def has_contour_integral_shiftpath_eq)

subsection\<^marker>\<open>tag unimportant\<close> \<open>More about straight-line paths\<close>

lemma has_contour_integral_linepath:
  shows "(f has_contour_integral i) (linepath a b) \
         ((\<lambda>x. f(linepath a b x) * (b - a)) has_integral i) {0..1}"
  by (simp add: has_contour_integral)

lemma has_contour_integral_trivial [iff]: "(f has_contour_integral 0) (linepath a a)"
  by (simp add: has_contour_integral_linepath)

lemma has_contour_integral_trivial_iff [simp]: "(f has_contour_integral i) (linepath a a) \ i=0"
  using has_contour_integral_unique by blast

lemma contour_integral_trivial [simp]: "contour_integral (linepath a a) f = 0"
  using has_contour_integral_trivial contour_integral_unique by blast

subsection\<open>Relation to subpath construction\<close>

lemma has_contour_integral_subpath_refl [iff]: "(f has_contour_integral 0) (subpath u u g)"
  by (simp add: has_contour_integral subpath_def)

lemma contour_integrable_subpath_refl [iff]: "f contour_integrable_on (subpath u u g)"
  using has_contour_integral_subpath_refl contour_integrable_on_def by blast

lemma contour_integral_subpath_refl [simp]: "contour_integral (subpath u u g) f = 0"
  by (simp add: contour_integral_unique)

lemma has_contour_integral_subpath:
  assumes f: "f contour_integrable_on g" and g: "valid_path g"
      and uv: "u \ {0..1}" "v \ {0..1}" "u \ v"
    shows "(f has_contour_integral integral {u..v} (\x. f(g x) * vector_derivative g (at x)))
           (subpath u v g)"
proof (cases "v=u")
  case True
  then show ?thesis
    using f   by (simp add: contour_integrable_on_def subpath_def has_contour_integral)
next
  case False
  obtain S where S: "\x. x \ {0..1} - S \ g differentiable at x" and fs: "finite S"
    using g unfolding piecewise_C1_differentiable_on_def C1_differentiable_on_eq valid_path_def by blast
  have \<section>: "(\<lambda>t. f (g t) * vector_derivative g (at t)) integrable_on {u..v}"
    using contour_integrable_on f integrable_on_subinterval uv by fastforce
  then have *: "((\x. f (g ((v - u) * x + u)) * vector_derivative g (at ((v - u) * x + u)))
            has_integral (1 / (v - u)) * integral {u..v} (\<lambda>t. f (g t) * vector_derivative g (at t)))
           {0..1}"
    using uv False unfolding has_integral_integral
    apply simp
    apply (drule has_integral_affinity [where m="v-u" and c=u, simplified])
    apply (simp_all add: image_affinity_atLeastAtMost_div_diff scaleR_conv_of_real)
    apply (simp add: divide_simps)
    done

  have vd: "vector_derivative (\x. g ((v-u) * x + u)) (at x) = (v-u) *\<^sub>R vector_derivative g (at ((v-u) * x + u))"
    if "x \ {0..1}" "x \ (\t. (v-u) *\<^sub>R t + u) -` S" for x
  proof (rule vector_derivative_at [OF vector_diff_chain_at [simplified o_def]])
    show "((\x. (v - u) * x + u) has_vector_derivative v - u) (at x)"
      by (intro derivative_eq_intros | simp)+
  qed (use S uv mult_left_le [of x "v-u"] that in \<open>auto simp: vector_derivative_works\<close>)

  have fin: "finite ((\t. (v - u) *\<^sub>R t + u) -` S)"
    using fs by (auto simp: inj_on_def False finite_vimageI)
  show ?thesis
    unfolding subpath_def has_contour_integral
    apply (rule has_integral_spike_finite [OF fin])
    using has_integral_cmul [OF *, where c = "v-u"] fs assms
    by (auto simp: False vd scaleR_conv_of_real)
qed

lemma contour_integrable_subpath:
  assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}"
    shows "f contour_integrable_on (subpath u v g)"
proof (cases u v rule: linorder_class.le_cases)
  case le
  then show ?thesis
    by (metis contour_integrable_on_def has_contour_integral_subpath [OF assms])
next
  case ge
  with assms show ?thesis
    by (metis (no_types, lifting) contour_integrable_on_def contour_integrable_reversepath_eq has_contour_integral_subpath reversepath_subpath valid_path_subpath)
qed

lemma has_integral_contour_integral_subpath:
  assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "u \ v"
    shows "(((\x. f(g x) * vector_derivative g (at x)))
            has_integral  contour_integral (subpath u v g) f) {u..v}"
  using assms
proof -
  have "(\r. f (g r) * vector_derivative g (at r)) integrable_on {u..v}"
    by (metis (full_types) assms(1) assms(3) assms(4) atLeastAtMost_iff atLeastatMost_subset_iff contour_integrable_on integrable_on_subinterval)
  then have "((\r. f (g r) * vector_derivative g (at r)) has_integral integral {u..v} (\r. f (g r) * vector_derivative g (at r))) {u..v}"
    by blast
  then show ?thesis
    by (metis (full_types) assms contour_integral_unique has_contour_integral_subpath)
qed

lemma contour_integral_subcontour_integral:
  assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "u \ v"
    shows "contour_integral (subpath u v g) f =
           integral {u..v} (\<lambda>x. f(g x) * vector_derivative g (at x))"
  using assms has_contour_integral_subpath contour_integral_unique by blast

lemma contour_integral_subpath_combine_less:
  assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "w \ {0..1}"
          "u "v
    shows "contour_integral (subpath u v g) f + contour_integral (subpath v w g) f =
           contour_integral (subpath u w g) f"
proof -
  have "(\x. f (g x) * vector_derivative g (at x)) integrable_on {u..w}"
    using integrable_on_subcbox [where a=u and b=w and S = "{0..1}"] assms
    by (auto simp: contour_integrable_on)
  with assms show ?thesis
    by (auto simp: contour_integral_subcontour_integral Henstock_Kurzweil_Integration.integral_combine)
qed

lemma contour_integral_subpath_combine:
  assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "w \ {0..1}"
    shows "contour_integral (subpath u v g) f + contour_integral (subpath v w g) f =
           contour_integral (subpath u w g) f"
proof (cases "u\v \ v\w \ u\w")
  case True
    have *: "subpath v u g = reversepath(subpath u v g) \
             subpath w u g = reversepath(subpath u w g) \<and>
             subpath w v g = reversepath(subpath v w g)"
      by (auto simp: reversepath_subpath)
    have "u < v \ v < w \
          u < w \<and> w < v \<or>
          v < u \<and> u < w \<or>
          v < w \<and> w < u \<or>
          w < u \<and> u < v \<or>
          w < v \<and> v < u"
      using True assms by linarith
    with assms show ?thesis
      using contour_integral_subpath_combine_less [of f g u v w]
            contour_integral_subpath_combine_less [of f g u w v]
            contour_integral_subpath_combine_less [of f g v u w]
            contour_integral_subpath_combine_less [of f g v w u]
            contour_integral_subpath_combine_less [of f g w u v]
            contour_integral_subpath_combine_less [of f g w v u]
      by (elim disjE) (auto simp: * contour_integral_reversepath contour_integrable_subpath
                                    valid_path_subpath algebra_simps)
next
  case False
  with assms show ?thesis
    by (metis add.right_neutral contour_integral_reversepath contour_integral_subpath_refl diff_0 eq_diff_eq add_0 reversepath_subpath valid_path_subpath)
qed

lemma contour_integral_integral:
     "contour_integral g f = integral {0..1} (\x. f (g x) * vector_derivative g (at x))"
  by (simp add: contour_integral_def integral_def has_contour_integral contour_integrable_on)

lemma contour_integral_cong:
  assumes "g = g'" "\x. x \ path_image g \ f x = f' x"
  shows   "contour_integral g f = contour_integral g' f'"
  unfolding contour_integral_integral using assms
  by (intro integral_cong) (auto simp: path_image_def)

text \<open>Contour integral along a segment on the real axis\<close>

lemma has_contour_integral_linepath_Reals_iff:
  fixes a b :: complex and f :: "complex \ complex"
  assumes "a \ Reals" "b \ Reals" "Re a < Re b"
  shows   "(f has_contour_integral I) (linepath a b) \
             ((\<lambda>x. f (of_real x)) has_integral I) {Re a..Re b}"
proof -
  from assms have [simp]: "of_real (Re a) = a" "of_real (Re b) = b"
    by (simp_all add: complex_eq_iff)
  from assms have "a \ b" by auto
  have "((\x. f (of_real x)) has_integral I) (cbox (Re a) (Re b)) \
          ((\<lambda>x. f (a + b * of_real x - a * of_real x)) has_integral I /\<^sub>R (Re b - Re a)) {0..1}"
    by (subst has_integral_affinity_iff [of "Re b - Re a" _ "Re a", symmetric])
       (insert assms, simp_all add: field_simps scaleR_conv_of_real)
  also have "(\x. f (a + b * of_real x - a * of_real x)) =
               (\<lambda>x. (f (a + b * of_real x - a * of_real x) * (b - a)) /\<^sub>R (Re b - Re a))"
    using \<open>a \<noteq> b\<close> by (auto simp: field_simps fun_eq_iff scaleR_conv_of_real)
  also have "(\ has_integral I /\<^sub>R (Re b - Re a)) {0..1} \
               ((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1}" using assms
    by (subst has_integral_cmul_iff) (auto simp: linepath_def scaleR_conv_of_real algebra_simps)
  also have "\ \ (f has_contour_integral I) (linepath a b)" unfolding has_contour_integral_def
    by (intro has_integral_cong) (simp add: vector_derivative_linepath_within)
  finally show ?thesis by simp
qed

lemma contour_integrable_linepath_Reals_iff:
  fixes a b :: complex and f :: "complex \ complex"
  assumes "a \ Reals" "b \ Reals" "Re a < Re b"
  shows   "(f contour_integrable_on linepath a b) \
             (\<lambda>x. f (of_real x)) integrable_on {Re a..Re b}"
  using has_contour_integral_linepath_Reals_iff[OF assms, of f]
  by (auto simp: contour_integrable_on_def integrable_on_def)

lemma contour_integral_linepath_Reals_eq:
  fixes a b :: complex and f :: "complex \ complex"
  assumes "a \ Reals" "b \ Reals" "Re a < Re b"
  shows   "contour_integral (linepath a b) f = integral {Re a..Re b} (\x. f (of_real x))"
proof (cases "f contour_integrable_on linepath a b")
  case True
  thus ?thesis using has_contour_integral_linepath_Reals_iff[OF assms, of f]
    using has_contour_integral_integral has_contour_integral_unique by blast
next
  case False
  thus ?thesis using contour_integrable_linepath_Reals_iff[OF assms, of f]
    by (simp add: not_integrable_contour_integral not_integrable_integral)
qed

subsection \<open>Cauchy's theorem where there's a primitive\<close>

lemma contour_integral_primitive_lemma:
  fixes f :: "complex \ complex" and g :: "real \ complex"
  assumes "a \ b"
      and "\x. x \ S \ (f has_field_derivative f' x) (at x within S)"
      and "g piecewise_differentiable_on {a..b}"  "\x. x \ {a..b} \ g x \ S"
    shows "((\x. f'(g x) * vector_derivative g (at x within {a..b}))
             has_integral (f(g b) - f(g a))) {a..b}"
proof -
  obtain K where "finite K" and K: "\x\{a..b} - K. g differentiable (at x within {a..b})" and cg: "continuous_on {a..b} g"
    using assms by (auto simp: piecewise_differentiable_on_def)
  have "continuous_on (g ` {a..b}) f"
    using assms
    by (metis field_differentiable_def field_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff)
  then have cfg: "continuous_on {a..b} (\x. f (g x))"
    by (rule continuous_on_compose [OF cg, unfolded o_def])
  { fix x::real
    assume a: "a < x" and b: "x < b" and xk: "x \ K"
    then have "g differentiable at x within {a..b}"
      using K by (simp add: differentiable_at_withinI)
    then have "(g has_vector_derivative vector_derivative g (at x within {a..b})) (at x within {a..b})"
      by (simp add: vector_derivative_works has_field_derivative_def scaleR_conv_of_real)
    then have gdiff: "(g has_derivative (\u. u * vector_derivative g (at x within {a..b}))) (at x within {a..b})"
      by (simp add: has_vector_derivative_def scaleR_conv_of_real)
    have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {a..b})"
      using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def)
    then have fdiff: "(f has_derivative (*) (f' (g x))) (at (g x) within g ` {a..b})"
      by (simp add: has_field_derivative_def)
    have "((\x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {a..b})) (at x within {a..b})"
      using diff_chain_within [OF gdiff fdiff]
      by (simp add: has_vector_derivative_def scaleR_conv_of_real o_def mult_ac)
  } note * = this
  show ?thesis
    using assms cfg *
    by (force simp: at_within_Icc_at intro: fundamental_theorem_of_calculus_interior_strong [OF \<open>finite K\<close>])
qed

lemma contour_integral_primitive:
  assumes "\x. x \ S \ (f has_field_derivative f' x) (at x within S)"
      and "valid_path g" "path_image g \ S"
    shows "(f' has_contour_integral (f(pathfinish g) - f(pathstart g))) g"
  using assms
  apply (simp add: valid_path_def path_image_def pathfinish_def pathstart_def has_contour_integral_def)
  apply (auto intro!: piecewise_C1_imp_differentiable contour_integral_primitive_lemma [of 0 1 S])
  done

corollary Cauchy_theorem_primitive:
  assumes "\x. x \ S \ (f has_field_derivative f' x) (at x within S)"
      and "valid_path g"  "path_image g \ S" "pathfinish g = pathstart g"
    shows "(f' has_contour_integral 0) g"
  using assms by (metis diff_self contour_integral_primitive)

text\<open>Existence of path integral for continuous function\<close>
lemma contour_integrable_continuous_linepath:
  assumes "continuous_on (closed_segment a b) f"
  shows "f contour_integrable_on (linepath a b)"
proof -
  have "continuous_on (closed_segment a b) (\x. f x * (b - a))"
    by (rule continuous_intros | simp add: assms)+
  then have "continuous_on {0..1} (\x. f (linepath a b x) * (b - a))"
    by (metis (no_types, lifting) continuous_on_compose continuous_on_cong continuous_on_linepath linepath_image_01 o_apply)
  then have "(\x. f (linepath a b x) *
         vector_derivative (linepath a b)
          (at x within {0..1})) integrable_on
    {0..1}"
    by (metis (no_types, lifting) continuous_on_cong integrable_continuous_real vector_derivative_linepath_within)
  then show ?thesis
    by (simp add: contour_integrable_on_def has_contour_integral_def integrable_on_def [symmetric])
qed

lemma has_field_der_id: "((\x. x\<^sup>2/2) has_field_derivative x) (at x)"
  by (rule has_derivative_imp_has_field_derivative)
     (rule derivative_intros | simp)+

lemma contour_integral_id [simp]: "contour_integral (linepath a b) (\y. y) = (b^2 - a^2)/2"
  using contour_integral_primitive [of UNIV "\x. x^2/2" "\x. x" "linepath a b"] contour_integral_unique
  by (simp add: has_field_der_id)

lemma contour_integrable_on_const [iff]: "(\x. c) contour_integrable_on (linepath a b)"
  by (simp add: contour_integrable_continuous_linepath)

lemma contour_integrable_on_id [iff]: "(\x. x) contour_integrable_on (linepath a b)"
  by (simp add: contour_integrable_continuous_linepath)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetical combining theorems\<close>

lemma has_contour_integral_neg:
    "(f has_contour_integral i) g \ ((\x. -(f x)) has_contour_integral (-i)) g"
  by (simp add: has_integral_neg has_contour_integral_def)

lemma has_contour_integral_add:
    "\(f1 has_contour_integral i1) g; (f2 has_contour_integral i2) g\
     \<Longrightarrow> ((\<lambda>x. f1 x + f2 x) has_contour_integral (i1 + i2)) g"
  by (simp add: has_integral_add has_contour_integral_def algebra_simps)

lemma has_contour_integral_diff:
  "\(f1 has_contour_integral i1) g; (f2 has_contour_integral i2) g\
         \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) has_contour_integral (i1 - i2)) g"
  by (simp add: has_integral_diff has_contour_integral_def algebra_simps)

lemma has_contour_integral_lmul:
  "(f has_contour_integral i) g \ ((\x. c * (f x)) has_contour_integral (c*i)) g"
  by (simp add: has_contour_integral_def algebra_simps has_integral_mult_right)

lemma has_contour_integral_rmul:
  "(f has_contour_integral i) g \ ((\x. (f x) * c) has_contour_integral (i*c)) g"
  by (simp add: mult.commute has_contour_integral_lmul)

lemma has_contour_integral_div:
  "(f has_contour_integral i) g \ ((\x. f x/c) has_contour_integral (i/c)) g"
  by (simp add: field_class.field_divide_inverse) (metis has_contour_integral_rmul)

lemma has_contour_integral_eq:
    "\(f has_contour_integral y) p; \x. x \ path_image p \ f x = g x\ \ (g has_contour_integral y) p"
  by (metis (mono_tags, lifting) has_contour_integral_def has_integral_eq image_eqI path_image_def)

lemma has_contour_integral_bound_linepath:
  assumes "(f has_contour_integral i) (linepath a b)"
          "0 \ B" and B: "\x. x \ closed_segment a b \ norm(f x) \ B"
    shows "norm i \ B * norm(b - a)"
proof -
  have "norm i \ (B * norm (b - a)) * content (cbox 0 (1::real))"
  proof (rule has_integral_bound
       [of _ "\x. f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})"])
    show  "cmod (f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1}))
         \<le> B * cmod (b - a)"
      if "x \ cbox 0 1" for x::real
      using that box_real(2) norm_mult
      by (metis B linepath_in_path mult_right_mono norm_ge_zero vector_derivative_linepath_within)
  qed (use assms has_contour_integral_def in auto)
  then show ?thesis
    by (auto simp: content_real)
qed

lemma has_contour_integral_const_linepath: "((\x. c) has_contour_integral c*(b - a))(linepath a b)"
  unfolding has_contour_integral_linepath
  by (metis content_real diff_0_right has_integral_const_real lambda_one of_real_1 scaleR_conv_of_real zero_le_one)

lemma has_contour_integral_0: "((\x. 0) has_contour_integral 0) g"
  by (simp add: has_contour_integral_def)

lemma has_contour_integral_is_0:
    "(\z. z \ path_image g \ f z = 0) \ (f has_contour_integral 0) g"
  by (rule has_contour_integral_eq [OF has_contour_integral_0]) auto

lemma has_contour_integral_sum:
    "\finite s; \a. a \ s \ (f a has_contour_integral i a) p\
     \<Longrightarrow> ((\<lambda>x. sum (\<lambda>a. f a x) s) has_contour_integral sum i s) p"
  by (induction s rule: finite_induct) (auto simp: has_contour_integral_0 has_contour_integral_add)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Operations on path integrals\<close>

lemma contour_integral_const_linepath [simp]: "contour_integral (linepath a b) (\x. c) = c*(b - a)"
  by (rule contour_integral_unique [OF has_contour_integral_const_linepath])

lemma contour_integral_neg:
    "f contour_integrable_on g \ contour_integral g (\x. -(f x)) = -(contour_integral g f)"
  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_neg)

lemma contour_integral_add:
    "f1 contour_integrable_on g \ f2 contour_integrable_on g \ contour_integral g (\x. f1 x + f2 x) =
                contour_integral g f1 + contour_integral g f2"
  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_add)

lemma contour_integral_diff:
    "f1 contour_integrable_on g \ f2 contour_integrable_on g \ contour_integral g (\x. f1 x - f2 x) =
                contour_integral g f1 - contour_integral g f2"
  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_diff)

lemma contour_integral_lmul:
  shows "f contour_integrable_on g
           \<Longrightarrow> contour_integral g (\<lambda>x. c * f x) = c*contour_integral g f"
  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_lmul)

lemma contour_integral_rmul:
  shows "f contour_integrable_on g
        \<Longrightarrow> contour_integral g (\<lambda>x. f x * c) = contour_integral g f * c"
  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_rmul)

lemma contour_integral_div:
  shows "f contour_integrable_on g
        \<Longrightarrow> contour_integral g (\<lambda>x. f x / c) = contour_integral g f / c"
  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_div)

lemma contour_integral_eq:
    "(\x. x \ path_image p \ f x = g x) \ contour_integral p f = contour_integral p g"
  using contour_integral_cong contour_integral_def by fastforce

lemma contour_integral_eq_0:
    "(\z. z \ path_image g \ f z = 0) \ contour_integral g f = 0"
  by (simp add: has_contour_integral_is_0 contour_integral_unique)

lemma contour_integral_bound_linepath:
  shows
    "\f contour_integrable_on (linepath a b);
      0 \<le> B; \<And>x. x \<in> closed_segment a b \<Longrightarrow> norm(f x) \<le> B\<rbrakk>
     \<Longrightarrow> norm(contour_integral (linepath a b) f) \<le> B*norm(b - a)"
  using has_contour_integral_bound_linepath [of f]
  by (auto simp: has_contour_integral_integral)

lemma contour_integral_0 [simp]: "contour_integral g (\x. 0) = 0"
  by (simp add: contour_integral_unique has_contour_integral_0)

lemma contour_integral_sum:
    "\finite s; \a. a \ s \ (f a) contour_integrable_on p\
     \<Longrightarrow> contour_integral p (\<lambda>x. sum (\<lambda>a. f a x) s) = sum (\<lambda>a. contour_integral p (f a)) s"
  by (auto simp: contour_integral_unique has_contour_integral_sum has_contour_integral_integral)

lemma contour_integrable_eq:
    "\f contour_integrable_on p; \x. x \ path_image p \ f x = g x\ \ g contour_integrable_on p"
  unfolding contour_integrable_on_def
  by (metis has_contour_integral_eq)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic theorems for path integrability\<close>

lemma contour_integrable_neg:
    "f contour_integrable_on g \ (\x. -(f x)) contour_integrable_on g"
  using has_contour_integral_neg contour_integrable_on_def by blast

lemma contour_integrable_add:
    "\f1 contour_integrable_on g; f2 contour_integrable_on g\ \ (\x. f1 x + f2 x) contour_integrable_on g"
  using has_contour_integral_add contour_integrable_on_def
  by fastforce

lemma contour_integrable_diff:
    "\f1 contour_integrable_on g; f2 contour_integrable_on g\ \ (\x. f1 x - f2 x) contour_integrable_on g"
  using has_contour_integral_diff contour_integrable_on_def
  by fastforce

lemma contour_integrable_lmul:
    "f contour_integrable_on g \ (\x. c * f x) contour_integrable_on g"
  using has_contour_integral_lmul contour_integrable_on_def
  by fastforce

lemma contour_integrable_rmul:
    "f contour_integrable_on g \ (\x. f x * c) contour_integrable_on g"
  using has_contour_integral_rmul contour_integrable_on_def
  by fastforce

lemma contour_integrable_div:
    "f contour_integrable_on g \ (\x. f x / c) contour_integrable_on g"
  using has_contour_integral_div contour_integrable_on_def
  by fastforce

lemma contour_integrable_sum:
    "\finite s; \a. a \ s \ (f a) contour_integrable_on p\
     \<Longrightarrow> (\<lambda>x. sum (\<lambda>a. f a x) s) contour_integrable_on p"
   unfolding contour_integrable_on_def
   by (metis has_contour_integral_sum)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Reversing a path integral\<close>

lemma has_contour_integral_reverse_linepath:
    "(f has_contour_integral i) (linepath a b)
     \<Longrightarrow> (f has_contour_integral (-i)) (linepath b a)"
  using has_contour_integral_reversepath valid_path_linepath by fastforce

lemma contour_integral_reverse_linepath:
    "continuous_on (closed_segment a b) f
     \<Longrightarrow> contour_integral (linepath a b) f = - (contour_integral(linepath b a) f)"
  by (metis contour_integrable_continuous_linepath contour_integral_unique has_contour_integral_integral has_contour_integral_reverse_linepath)

text \<open>Splitting a path integral in a flat way.*)\<close>

lemma has_contour_integral_split:
  assumes f: "(f has_contour_integral i) (linepath a c)" "(f has_contour_integral j) (linepath c b)"
      and k: "0 \ k" "k \ 1"
      and c: "c - a = k *\<^sub>R (b - a)"
    shows "(f has_contour_integral (i + j)) (linepath a b)"
proof (cases "k = 0 \ k = 1")
  case True
  then show ?thesis
    using assms by auto
next
  case False
  then have k: "0 < k" "k < 1" "complex_of_real k \ 1"
    using assms by auto
  have c': "c = k *\<^sub>R (b - a) + a"
    by (metis diff_add_cancel c)
  have bc: "(b - c) = (1 - k) *\<^sub>R (b - a)"
    by (simp add: algebra_simps c')
  { assume *: "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R c) * (c - a)) has_integral i) {0..1}"
    have "\x. (x / k) *\<^sub>R a + ((k - x) / k) *\<^sub>R a = a"
      using False by (simp add: field_split_simps flip: real_vector.scale_left_distrib)
    then have "\x. ((k - x) / k) *\<^sub>R a + (x / k) *\<^sub>R c = (1 - x) *\<^sub>R a + x *\<^sub>R b"
      using False by (simp add: c' algebra_simps)
    then have "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral i) {0..k}"
      using k has_integral_affinity01 [OF *, of "inverse k" "0"]
      by (force dest: has_integral_cmul [where c = "inverse k"]
              simp add: divide_simps mult.commute [of _ "k"] image_affinity_atLeastAtMost c)
  } note fi = this
  { assume *: "((\x. f ((1 - x) *\<^sub>R c + x *\<^sub>R b) * (b - c)) has_integral j) {0..1}"
    have **: "\x. (((1 - x) / (1 - k)) *\<^sub>R c + ((x - k) / (1 - k)) *\<^sub>R b) = ((1 - x) *\<^sub>R a + x *\<^sub>R b)"
      using k unfolding c' scaleR_conv_of_real
      apply (simp add: divide_simps)
      apply (simp add: distrib_right distrib_left right_diff_distrib left_diff_distrib)
      done
    have "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral j) {k..1}"
      using k has_integral_affinity01 [OF *, of "inverse(1 - k)" "-(k/(1 - k))"]
      apply (simp add: divide_simps mult.commute [of _ "1-k"] image_affinity_atLeastAtMost ** bc)
      apply (auto dest: has_integral_cmul [where k = "(1 - k) *\<^sub>R j" and c = "inverse (1 - k)"])
      done
  } note fj = this
  show ?thesis
    using f k unfolding has_contour_integral_linepath
    by (simp add: linepath_def has_integral_combine [OF _ _ fi fj])
qed

lemma continuous_on_closed_segment_transform:
  assumes f: "continuous_on (closed_segment a b) f"
      and k: "0 \ k" "k \ 1"
      and c: "c - a = k *\<^sub>R (b - a)"
    shows "continuous_on (closed_segment a c) f"
proof -
  have c': "c = (1 - k) *\<^sub>R a + k *\<^sub>R b"
    using c by (simp add: algebra_simps)
  have "closed_segment a c \ closed_segment a b"
    by (metis c' ends_in_segment(1) in_segment(1) k subset_closed_segment)
  then show "continuous_on (closed_segment a c) f"
    by (rule continuous_on_subset [OF f])
qed

lemma contour_integral_split:
  assumes f: "continuous_on (closed_segment a b) f"
      and k: "0 \ k" "k \ 1"
      and c: "c - a = k *\<^sub>R (b - a)"
    shows "contour_integral(linepath a b) f = contour_integral(linepath a c) f + contour_integral(linepath c b) f"
proof -
  have c': "c = (1 - k) *\<^sub>R a + k *\<^sub>R b"
    using c by (simp add: algebra_simps)
  have "closed_segment a c \ closed_segment a b"
    by (metis c' ends_in_segment(1) in_segment(1) k subset_closed_segment)
  moreover have "closed_segment c b \ closed_segment a b"
    by (metis c' ends_in_segment(2) in_segment(1) k subset_closed_segment)
  ultimately
  have *: "continuous_on (closed_segment a c) f" "continuous_on (closed_segment c b) f"
    by (auto intro: continuous_on_subset [OF f])
  show ?thesis
    by (rule contour_integral_unique) (meson "*" c contour_integrable_continuous_linepath has_contour_integral_integral has_contour_integral_split k)
qed

lemma contour_integral_split_linepath:
  assumes f: "continuous_on (closed_segment a b) f"
      and c: "c \ closed_segment a b"
    shows "contour_integral(linepath a b) f = contour_integral(linepath a c) f + contour_integral(linepath c b) f"
  using c by (auto simp: closed_segment_def algebra_simps intro!: contour_integral_split [OF f])

subsection\<open>Reversing the order in a double path integral\<close>

text\<open>The condition is stronger than needed but it's often true in typical situations\<close>

lemma fst_im_cbox [simp]: "cbox c d \ {} \ (fst ` cbox (a,c) (b,d)) = cbox a b"
  by (auto simp: cbox_Pair_eq)

lemma snd_im_cbox [simp]: "cbox a b \ {} \ (snd ` cbox (a,c) (b,d)) = cbox c d"
  by (auto simp: cbox_Pair_eq)

proposition contour_integral_swap:
  assumes fcon:  "continuous_on (path_image g \ path_image h) (\(y1,y2). f y1 y2)"
      and vp:    "valid_path g" "valid_path h"
      and gvcon: "continuous_on {0..1} (\t. vector_derivative g (at t))"
      and hvcon: "continuous_on {0..1} (\t. vector_derivative h (at t))"
  shows "contour_integral g (\w. contour_integral h (f w)) =
         contour_integral h (\<lambda>z. contour_integral g (\<lambda>w. f w z))"
proof -
  have gcon: "continuous_on {0..1} g" and hcon: "continuous_on {0..1} h"
    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
  have fgh1: "\x. (\t. f (g x) (h t)) = (\(y1,y2). f y1 y2) \ (\t. (g x, h t))"
    by (rule ext) simp
  have fgh2: "\x. (\t. f (g t) (h x)) = (\(y1,y2). f y1 y2) \ (\t. (g t, h x))"
    by (rule ext) simp
  have fcon_im1: "\x. 0 \ x \ x \ 1 \ continuous_on ((\t. (g x, h t)) ` {0..1}) (\(x, y). f x y)"
    by (rule continuous_on_subset [OF fcon]) (auto simp: path_image_def)
  have fcon_im2: "\x. 0 \ x \ x \ 1 \ continuous_on ((\t. (g t, h x)) ` {0..1}) (\(x, y). f x y)"
    by (rule continuous_on_subset [OF fcon]) (auto simp: path_image_def)
  have "continuous_on (cbox (0, 0) (1, 1::real)) ((\x. vector_derivative g (at x)) \ fst)"
       "continuous_on (cbox (0, 0) (1::real, 1)) ((\x. vector_derivative h (at x)) \ snd)"
    by (rule continuous_intros | simp add: gvcon hvcon)+
  then have gvcon': "continuous_on (cbox (0, 0) (1, 1::real)) (\z. vector_derivative g (at (fst z)))"
       and  hvcon': "continuous_on (cbox (0, 0) (1::real, 1)) (\x. vector_derivative h (at (snd x)))"
    by auto
  have "continuous_on (cbox (0, 0) (1, 1)) ((\(y1, y2). f y1 y2) \ (\w. ((g \ fst) w, (h \ snd) w)))"
    apply (intro gcon hcon continuous_intros | simp)+
    apply (auto simp: path_image_def intro: continuous_on_subset [OF fcon])
    done
  then have fgh: "continuous_on (cbox (0, 0) (1, 1)) (\x. f (g (fst x)) (h (snd x)))"
    by auto
  have "integral {0..1} (\x. contour_integral h (f (g x)) * vector_derivative g (at x)) =
        integral {0..1} (\<lambda>x. contour_integral h (\<lambda>y. f (g x) y * vector_derivative g (at x)))"
  proof (rule integral_cong [OF contour_integral_rmul [symmetric]])
    have "\x. x \ {0..1} \
         continuous_on {0..1} (\<lambda>xa. f (g x) (h xa))"
    by (subst fgh1) (rule fcon_im1 hcon continuous_intros | simp)+
    then show "\x. x \ {0..1} \ f (g x) contour_integrable_on h"
      unfolding contour_integrable_on
      using continuous_on_mult hvcon integrable_continuous_real by blast
  qed
  also have "\ = integral {0..1}
                     (\<lambda>y. contour_integral g (\<lambda>x. f x (h y) * vector_derivative h (at y)))"
    unfolding contour_integral_integral
    apply (subst integral_swap_continuous [where 'a = real and 'b = real, of 0 0 1 1, simplified])
    subgoal
      by (rule fgh gvcon' hvcon' continuous_intros | simp add: split_def)+
    subgoal
      unfolding integral_mult_left [symmetric]
      by (simp only: mult_ac)
    done
  also have "\ = contour_integral h (\z. contour_integral g (\w. f w z))"
    unfolding contour_integral_integral integral_mult_left [symmetric]
    by (simp add: algebra_simps)
  finally show ?thesis
    by (simp add: contour_integral_integral)
qed

lemma valid_path_negatepath: "valid_path \ \ valid_path (uminus \ \)"
   unfolding o_def using piecewise_C1_differentiable_neg valid_path_def by blast

lemma has_contour_integral_negatepath:
  assumes \<gamma>: "valid_path \<gamma>" and cint: "((\<lambda>z. f (- z)) has_contour_integral - i) \<gamma>"
  shows "(f has_contour_integral i) (uminus \ \)"
proof -
  obtain S where cont: "continuous_on {0..1} \" and "finite S" and diff: "\ C1_differentiable_on {0..1} - S"
    using \<gamma> by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
  have "((\x. - (f (- \ x) * vector_derivative \ (at x within {0..1}))) has_integral i) {0..1}"
    using cint by (auto simp: has_contour_integral_def dest: has_integral_neg)
  then
  have "((\x. f (- \ x) * vector_derivative (uminus \ \) (at x within {0..1})) has_integral i) {0..1}"
  proof (rule rev_iffD1 [OF _ has_integral_spike_eq])
    show "negligible S"
      by (simp add: \<open>finite S\<close> negligible_finite)
    show "f (- \ x) * vector_derivative (uminus \ \) (at x within {0..1}) =
         - (f (- \<gamma> x) * vector_derivative \<gamma> (at x within {0..1}))"
      if "x \ {0..1} - S" for x
    proof -
      have "vector_derivative (uminus \ \) (at x within cbox 0 1) = - vector_derivative \ (at x within cbox 0 1)"
      proof (rule vector_derivative_within_cbox)
        show "(uminus \ \ has_vector_derivative - vector_derivative \ (at x within cbox 0 1)) (at x within cbox 0 1)"
          using that unfolding o_def
          by (metis C1_differentiable_on_eq UNIV_I diff differentiable_subset has_vector_derivative_minus subsetI that vector_derivative_works)
      qed (use that in auto)
      then show ?thesis
        by simp
    qed
  qed
  then show ?thesis by (simp add: has_contour_integral_def)
qed

lemma contour_integrable_negatepath:
  assumes \<gamma>: "valid_path \<gamma>" and pi: "(\<lambda>z. f (- z)) contour_integrable_on \<gamma>"
  shows "f contour_integrable_on (uminus \ \)"
  by (metis \<gamma> add.inverse_inverse contour_integrable_on_def has_contour_integral_negatepath pi)

lemma C1_differentiable_polynomial_function:
  fixes p :: "real \ 'a::euclidean_space"
  shows "polynomial_function p \ p C1_differentiable_on S"
  by (metis continuous_on_polymonial_function C1_differentiable_on_def  has_vector_derivative_polynomial_function)

lemma valid_path_polynomial_function:
  fixes p :: "real \ 'a::euclidean_space"
  shows "polynomial_function p \ valid_path p"
by (force simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_polymonial_function C1_differentiable_polynomial_function)

lemma valid_path_subpath_trivial [simp]:
    fixes g :: "real \ 'a::euclidean_space"
    shows "z \ g x \ valid_path (subpath x x g)"
  by (simp add: subpath_def valid_path_polynomial_function)

subsection\<open>Partial circle path\<close>

definition\<^marker>\<open>tag important\<close> part_circlepath :: "[complex, real, real, real, real] \<Rightarrow> complex"
  where "part_circlepath z r s t \ \x. z + of_real r * exp (\ * of_real (linepath s t x))"

lemma pathstart_part_circlepath [simp]:
     "pathstart(part_circlepath z r s t) = z + r*exp(\ * s)"
by (metis part_circlepath_def pathstart_def pathstart_linepath)

lemma pathfinish_part_circlepath [simp]:
     "pathfinish(part_circlepath z r s t) = z + r*exp(\*t)"
by (metis part_circlepath_def pathfinish_def pathfinish_linepath)

lemma reversepath_part_circlepath[simp]:
    "reversepath (part_circlepath z r s t) = part_circlepath z r t s"
  unfolding part_circlepath_def reversepath_def linepath_def
  by (auto simp:algebra_simps)

lemma has_vector_derivative_part_circlepath [derivative_intros]:
    "((part_circlepath z r s t) has_vector_derivative
      (\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)))
     (at x within X)"
  unfolding part_circlepath_def linepath_def scaleR_conv_of_real
  by (rule has_vector_derivative_real_field derivative_eq_intros | simp)+

lemma differentiable_part_circlepath:
  "part_circlepath c r a b differentiable at x within A"
  using has_vector_derivative_part_circlepath[of c r a b x A] differentiableI_vector by blast

lemma vector_derivative_part_circlepath:
    "vector_derivative (part_circlepath z r s t) (at x) =
       \<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)"
  using has_vector_derivative_part_circlepath vector_derivative_at by blast

lemma vector_derivative_part_circlepath01:
    "\0 \ x; x \ 1\
     \<Longrightarrow> vector_derivative (part_circlepath z r s t) (at x within {0..1}) =
          \<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)"
  using has_vector_derivative_part_circlepath
  by (auto simp: vector_derivative_at_within_ivl)

lemma valid_path_part_circlepath [simp]: "valid_path (part_circlepath z r s t)"
  unfolding valid_path_def
  by (auto simp: C1_differentiable_on_eq vector_derivative_works vector_derivative_part_circlepath has_vector_derivative_part_circlepath
              intro!: C1_differentiable_imp_piecewise continuous_intros)

lemma path_part_circlepath [simp]: "path (part_circlepath z r s t)"
  by (simp add: valid_path_imp_path)

proposition path_image_part_circlepath:
  assumes "s \ t"
    shows "path_image (part_circlepath z r s t) = {z + r * exp(\ * of_real x) | x. s \ x \ x \ t}"
proof -
  { fix z::real
    assume "0 \ z" "z \ 1"
    with \<open>s \<le> t\<close> have "\<exists>x. (exp (\<i> * linepath s t z) = exp (\<i> * of_real x)) \<and> s \<le> x \<and> x \<le> t"
      apply (rule_tac x="(1 - z) * s + z * t" in exI)
      apply (simp add: linepath_def scaleR_conv_of_real algebra_simps)
      by (metis (no_types) affine_ineq mult.commute mult_left_mono)
  }
  moreover
  { fix z
    assume "s \ z" "z \ t"
    then have "z + of_real r * exp (\ * of_real z) \ (\x. z + of_real r * exp (\ * linepath s t x)) ` {0..1}"
      apply (rule_tac x="(z - s)/(t - s)" in image_eqI)
      apply (simp add: linepath_def scaleR_conv_of_real divide_simps exp_eq)
      apply (auto simp: field_split_simps)
      done
  }
  ultimately show ?thesis
    by (fastforce simp add: path_image_def part_circlepath_def)
qed

lemma path_image_part_circlepath':
  "path_image (part_circlepath z r s t) = (\x. z + r * cis x) ` closed_segment s t"
proof -
  have "path_image (part_circlepath z r s t) =
          (\<lambda>x. z + r * exp(\<i> * of_real x)) ` linepath s t ` {0..1}"
    by (simp add: image_image path_image_def part_circlepath_def)
  also have "linepath s t ` {0..1} = closed_segment s t"
    by (rule linepath_image_01)
  finally show ?thesis by (simp add: cis_conv_exp)
qed

lemma path_image_part_circlepath_subset:
    "\s \ t; 0 \ r\ \ path_image(part_circlepath z r s t) \ sphere z r"
by (auto simp: path_image_part_circlepath sphere_def dist_norm algebra_simps norm_mult)

lemma in_path_image_part_circlepath:
  assumes "w \ path_image(part_circlepath z r s t)" "s \ t" "0 \ r"
    shows "norm(w - z) = r"
proof -
  have "w \ {c. dist z c = r}"
    by (metis (no_types) path_image_part_circlepath_subset sphere_def subset_eq assms)
  thus ?thesis
    by (simp add: dist_norm norm_minus_commute)
qed

lemma path_image_part_circlepath_subset':
  assumes "r \ 0"
  shows   "path_image (part_circlepath z r s t) \ sphere z r"
proof (cases "s \ t")
  case True
  thus ?thesis using path_image_part_circlepath_subset[of s t r z] assms by simp
next
  case False
  thus ?thesis using path_image_part_circlepath_subset[of t s r z] assms
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.63 Sekunden (vorverarbeitet) ¤

vermutete Sprache: Sekunden
vermutete Sprache: sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Bille.loaded2.jpg Sprache: Isabelle

Original von: Isabelle©

¤ Dauer der Verarbeitung: 0.63 Sekunden (vorverarbeitet) ¤

Haftungshinweis

Bemerkung:

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©