Quelle Contour_Integration.thy Sprache: 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 \<open>has'_contour'_integral\<close> 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 \<open>contour'_integrable'_on\<close> 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"
  unfolding contour_integral_def has_contour_integral_def contour_integrable_on_def
  using has_integral_unique by blast

lemma has_contour_integral_cong:
  assumes "\z. z \ path_image g \ f z = f' z" "g = g'" "c = c'"
  shows   "(f has_contour_integral c) g \ (f' has_contour_integral c') g'"
  unfolding has_contour_integral_def assms(2,3)
  by (intro has_integral_cong) (auto simp: assms path_image_def intro!: assms(1))

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_translate:
  "(f has_contour_integral I) ((+) z \ g) \ ((\x. f (x + z)) has_contour_integral I) g"
  by (simp add: has_contour_integral_def add_ac)

lemma contour_integrable_translate:
  "f contour_integrable_on ((+) z \ g) \ (\x. f (x + z)) contour_integrable_on g"
  by (simp add: contour_integrable_on_def has_contour_integral_translate)

lemma contour_integral_translate:
  "contour_integral ((+) z \ g) f = contour_integral g (\x. f (x + z))"
  by (simp add: contour_integral_def contour_integrable_translate has_contour_integral_translate)

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 p (at x within {a..b})) has_integral i) {a..b} \
     ((\<lambda>x. f (g x) * vector_derivative p (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 p (at x within {a..b})) integrable_on {a..b} \
     (\<lambda>x. f (g x) * vector_derivative p (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)

lemma has_contour_integral_mirror_iff:
  assumes "valid_path g"
  shows   "(f has_contour_integral I) (-g) \ ((\x. -f (- x)) has_contour_integral I) g"
proof -
  from assms have "g piecewise_differentiable_on {0..1}"
    by (auto simp: valid_path_def piecewise_C1_imp_differentiable)
  then obtain S where "finite S" and S: "\x. x \ {0..1} - S \ g differentiable at x within {0..1}"
     unfolding piecewise_differentiable_on_def by blast
  have S': "g differentiable at x" if "x \ {0..1} - ({0, 1} \ S)" for x
  proof -
    from that have "x \ interior {0..1}" by auto
    with S[of x] that show ?thesis by (auto simp: at_within_interior[of _ "{0..1}"])
  qed
  have "(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_contour_integral)
  also have "\ \ ((\x. -f (- g x) * vector_derivative g (at x)) has_integral I) {0..1}"
    by (intro has_integral_spike_finite_eq[of "S \ {0, 1}"])
       (insert \<open>finite S\<close> S', auto simp: o_def fun_Compl_def)
  also have "\ \ ((\x. -f (-x)) has_contour_integral I) g"
    by (simp add: has_contour_integral)
  finally show ?thesis .
qed

lemma contour_integral_on_mirror_iff:
  assumes "valid_path g"
  shows   "f contour_integrable_on (-g) \ (\x. -f (- x)) contour_integrable_on g"
  by (auto simp: contour_integrable_on_def has_contour_integral_mirror_iff assms)

lemma contour_integral_mirror:
  assumes "valid_path g"
  shows   "contour_integral (-g) f = contour_integral g (\x. -f (- x))"
proof (cases "f contour_integrable_on (-g)")
  case True with contour_integral_unique assms show ?thesis
    by (auto simp: contour_integrable_on_def has_contour_integral_mirror_iff)
next
  case False then show ?thesis
    by (simp add: assms contour_integral_on_mirror_iff not_integrable_contour_integral)
qed

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))"
    by (smt (verit, ccfv_threshold) Henstock_Kurzweil_Integration.integral_combine a add.commute atLeastAtMost_iff has_integral_iff)
  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)"
  by (smt (verit, ccfv_threshold) assms contour_integrable_on_def contour_integrable_reversepath_eq
      has_contour_integral_subpath reversepath_subpath valid_path_subpath)

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}"
          (is "(?fg has_integral _)_")
proof -
  have "(?fg has_integral integral {u..v} ?fg) {u..v}"
    using assms contour_integrable_on integrable_on_subinterval by fastforce
  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"
  by (smt (verit) Henstock_Kurzweil_Integration.integral_combine assms
      has_integral_contour_integral_subpath has_integral_iff)

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)

lemma contour_integral_spike_finite_simple_path:
  assumes "finite A" "simple_path g" "g = g'" "\x. x \ path_image g - A \ f x = f' x"
  shows   "contour_integral g f = contour_integral g' f'"
  unfolding contour_integral_integral
proof (rule integral_spike)
  have "finite (g -` A \ {0<..<1})" using \simple_path g\ \finite A\
    by (intro finite_vimage_IntI simple_path_inj_on) auto
  hence "finite ({0, 1} \ g -` A \ {0<..<1})" by auto
  thus "negligible ({0, 1} \ g -` A \ {0<..<1})" by (rule negligible_finite)
next
  fix x assume "x \ {0..1} - ({0, 1} \ g -` A \ {0<..<1})"
  hence "g x \ path_image g - A" by (auto simp: path_image_def)
  with assms show "f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)"
    by simp
qed

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 -
  have [simp]: "of_real (Re a) = a" "of_real (Re b) = b" and "a \ b"
    using assms by (simp_all add: complex_eq_iff)
  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
    using has_contour_integral_def has_contour_integral_linepath by presburger
  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
    by (metis assms has_contour_integral_integral
        has_contour_integral_linepath_Reals_iff integral_unique)
next
  case False
  thus ?thesis
    by (simp add: assms contour_integrable_linepath_Reals_iff
        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 DERIV_continuous_on continuous_on_subset image_subsetI)
  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)
  } then 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)

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)) * measure lborel (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: "contour_integral g (\z. -f z) = -contour_integral g f"
  by (simp add: contour_integral_integral)

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)"
  by (meson has_contour_integral_bound_linepath 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)

lemma contour_integrable_neg_iff:
  "(\x. -f x) contour_integrable_on g \ f contour_integrable_on g"
  using contour_integrable_neg[of f g] contour_integrable_neg[of "\x. -f x" g] by auto

lemma contour_integrable_lmul_iff:
    "c \ 0 \ (\x. c * f x) contour_integrable_on g \ f contour_integrable_on g"
  using contour_integrable_lmul[of f g c] contour_integrable_lmul[of "\x. c * f x" g "inverse c"]
  by (auto simp: field_simps)

lemma contour_integrable_rmul_iff:
    "c \ 0 \ (\x. f x * c) contour_integrable_on g \ f contour_integrable_on g"
  using contour_integrable_rmul[of f g c] contour_integrable_rmul[of "\x. c * f x" g "inverse c"]
  by (auto simp: field_simps)

lemma contour_integrable_div_iff:
    "c \ 0 \ (\x. f x / c) contour_integrable_on g \ f contour_integrable_on g"
  using contour_integrable_rmul_iff[of "inverse c"] by (simp add: field_simps)

(* TODO: generalise to any path *)
lemma uniform_limit_contour_integral_linepath:
  assumes u: "uniform_limit (path_image (linepath a b)) f g F"
  assumes c: "\n. continuous_on (path_image (linepath a b)) (f n)"
  assumes [simp]: "F \ bot"
  obtains I J where
    "\n. (f n has_contour_integral I n) (linepath a b)"
    "(g has_contour_integral J) (linepath a b)"
    "(I \ J) F"
proof (rule uniform_limit_integral)
  note [continuous_intros] = continuous_on_compose2[OF c]

  show "uniform_limit {0..1} (\x t. f x (linepath a b t) * (b - a))
          (\<lambda>t. g (linepath a b t) * (b - a)) F"
  proof (rule uniform_limit_intros)
    show "uniform_limit {0..1} (\x t. f x (linepath a b t))
            (\<lambda>t. g (linepath a b t)) F"
      using u unfolding path_image_def by (rule uniform_limit_compose') auto
  qed

  show "continuous_on {0..1} (\t. f n (linepath a b t) * (b - a))" for n
    by (intro continuous_intros; unfold path_image_def) auto

  fix I J
  assume I: "\n. ((\t. f n (linepath a b t) * (b - a)) has_integral I n) {0..1}"
     and J: "((\t. g (linepath a b t) * (b - a)) has_integral J) {0..1}"
     and lim: "(I \ J) F"
  show ?thesis
   by (rule that[of I J]) (use I J lim in \<open>auto simp: has_contour_integral\<close>)
qed auto

(* TODO: generalise to any path *)
lemma contour_integral_sums_linepath:
  assumes u: "uniform_limit (closed_segment a b) (\N w. \n
  assumes c: "\n. continuous_on (closed_segment a b) (f n)"
  obtains J where
    "(g has_contour_integral J) (linepath a b)"
    "(\n. contour_integral (linepath a b) (f n)) sums J"
proof (rule uniform_limit_contour_integral_linepath)
  show "uniform_limit (path_image (linepath a b)) (\N w. \n
    using u by simp
next
  show "continuous_on (path_image (linepath a b)) (\w. \n
    by (intro continuous_intros continuous_on_subset[OF c]) simp_all
next
  fix I J
  assume 1: "\N. ((\w. \n
  assume 2: "(g has_contour_integral J) (linepath a b)" and 3: "(I \ J) sequentially"
  have 4: "I = (\N. (\n
  proof
    fix N :: nat
    have "f n contour_integrable_on (linepath a b)" for n
      by (intro contour_integrable_continuous_linepath assms)
    hence "((\w. \n
             (\<Sum>n<N. contour_integral (linepath a b) (f n))) (linepath a b)"
      using c by (intro has_contour_integral_sum) (simp_all add: has_contour_integral_integral)
    with 1[of N] show "I N = (\n
      using contour_integral_unique by metis
  qed
  have 5: "(\n. contour_integral (linepath a b) (f n)) sums J"
    using 1 2 3 4 unfolding sums_def by blast
  from that[OF 2 5] show ?thesis .
qed auto

lemma contour_integral_linepath_same_Re:
  assumes "Re z = c" "Re z' = c" "Im z = a" "Im z' = b" "a < b"
  shows   "contour_integral (linepath z z') f =
           \<i> * integral {a..b} (\<lambda>x. f (Complex c x))"
proof -
  have zz': "z = Complex c a" "z' = Complex c b"
    using assms by (auto simp: complex_eq_iff)
  have "contour_integral (linepath z z') f =
         (z' - z) * integral {0..1} (\x. f (linepath z z' x))"
    by (simp add: contour_integral_integral)
  also have "z' - z = \ * of_real (b - a)"
    by (simp add: zz' Complex_eq algebra_simps)
  also have "integral {0..1} (\x. f (linepath z z' x)) =
             integral {0..1} (\<lambda>x. f (Complex c (linepath a b x)))"
    by (simp add: linepath_def Complex_eq scaleR_conv_of_real algebra_simps zz')
  also have "\ = integral {0..(b - a) / (b - a)} (\x. f (Complex c (a + (b - a) * x)))"
    using \<open>a < b\<close> by (simp add: algebra_simps linepath_def)
  also have "{0..(b - a) / (b - a)} = (\x. x / (b - a)) ` {0..b - a}"
    using \<open>a < b\<close> by simp
  also have "integral \ (\x. f (Complex c (a + (b - a) * x))) =
             integral {a-a..b-a} (\<lambda>x. f (Complex c (x + a))) / of_real (b - a)"
    using \<open>a < b\<close> by (subst integral_stretch_real) (auto simp: scaleR_conv_of_real add_ac)
  also have "\ = integral {a..b} (\x. f (Complex c x)) / of_real (b - a)"
    by (subst integral_shift_real_ivl) (rule refl)
  finally show ?thesis
    using \<open>a < b\<close> by simp
qed

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 \ contour_integral (linepath a b) f = - (contour_integral(linepath b a) f)"
  using contour_integral_reversepath by fastforce

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"
    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
      apply (simp add: c' scaleR_conv_of_real 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
  }
  then show ?thesis
    using f k unfolding has_contour_integral_linepath
    by (simp add: linepath_def has_integral_combine [OF _ _ fi])
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])
  then have "(f has_contour_integral
                contour_integral (linepath a c) f + contour_integral (linepath c b) f) (linepath a b)"
    by (meson c contour_integrable_continuous_linepath
        has_contour_integral_integral has_contour_integral_split k)
  then show ?thesis
    by (metis contour_integral_unique)
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 ((\x. (g (fst x), h (snd x))) ` cbox (0,0) (1,1)) (\(y1, y2). f y1 y2)"
    by (auto simp: path_image_def intro: continuous_on_subset [OF fcon])
  then have "continuous_on (cbox (0, 0) (1, 1)) ((\(y1, y2). f y1 y2) \ (\w. ((g \ fst) w, (h \ snd) w)))"
    by (intro gcon hcon continuous_intros | simp)+
  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
--> --------------------

--> maximum size reached

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

quality100%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.