Theory Parallelogram_Paths

subsection ‹Parallelogram-shaped paths›
theory Parallelogram_Paths
  imports "HOL-Complex_Analysis.Complex_Analysis"
begin

definition parallelogram_path :: "'a :: real_normed_vector ⇒ 'a ⇒ 'a ⇒ real ⇒ 'a" where
  "parallelogram_path z a b = 
     linepath z (z + a) +++ linepath (z + a) (z + a + b) +++ 
     linepath (z + a + b) (z + b) +++ linepath (z + b) z"

lemma path_parallelogram_path [intro]: "path (parallelogram_path z a b)"
  and valid_path_parallelogram_path [intro]: "valid_path (parallelogram_path z a b)"
  and pathstart_parallelogram_path [simp]: "pathstart (parallelogram_path z a b) = z"
  and pathfinish_parallelogram_path [simp]: "pathfinish (parallelogram_path z a b) = z"
  by (auto simp: parallelogram_path_def intro!: valid_path_join)

lemma parallelogram_path_altdef:
  fixes z a b :: complex
  defines "g ≡ (λw. z + Re w *⇩R a + Im w *⇩R b)"
  shows   "parallelogram_path z a b = g ∘ rectpath 0 (1 + 𝗂)"
  by (simp add: parallelogram_path_def rectpath_def g_def Let_def o_def joinpaths_def
                fun_eq_iff linepath_def scaleR_conv_of_real algebra_simps)

lemma
  fixes f :: "complex ⇒ complex" and z ω1 ω2 :: complex
  defines "I ≡ (λa b. contour_integral (linepath (z + a) (z + b)) f)"
  defines "P ≡ parallelogram_path z ω1 ω2"
  assumes "continuous_on (path_image P) f"
  shows contour_integral_parallelogram_path:
          "contour_integral P f =
             (I 0 ω1 - I ω2 (ω1 + ω2)) - (I 0 ω2 - I ω1 (ω1 + ω2))"
    and contour_integral_parallelogram_path':
          "contour_integral P f =
             contour_integral (linepath z (z + ω1)) (λx. f x - f (x + ω2)) -
             contour_integral (linepath z (z + ω2)) (λx. f x - f (x + ω1))"
proof -
  define L where "L = (λa b. linepath (z + a) (z + b))"
  have I: "(f has_contour_integral (I a b)) (L a b)"
    if "closed_segment (z + a) (z + b) ⊆ path_image P" for a b
    unfolding I_def L_def
    by (intro has_contour_integral_integral contour_integrable_continuous_linepath
              continuous_on_subset[OF assms(3)] that)
  have "(f has_contour_integral
          (I 0 ω1 + (I ω1 (ω1 + ω2) + ((-I ω2 (ω1 + ω2)) + (-I 0 ω2)))))
          (L 0 ω1 +++ L ω1 (ω1 + ω2) +++ reversepath (L ω2 (ω1 + ω2)) +++ reversepath (L 0 ω2))"
    unfolding P_def parallelogram_path_def
    by (intro has_contour_integral_join valid_path_join valid_path_linepath has_contour_integral_reversepath I)
       (auto simp: parallelogram_path_def path_image_join closed_segment_commute P_def L_def add_ac)
  thus "contour_integral P f =
           (I 0 ω1 - I ω2 (ω1 + ω2)) - (I 0 ω2 - I ω1 (ω1 + ω2))"
    by (intro contour_integral_unique)
       (simp_all add: parallelogram_path_def P_def L_def algebra_simps)

  also have "I 0 ω2 - I ω1 (ω1 + ω2) = contour_integral (L 0 ω2) (λx. f x - f (x + ω1))"
  proof -
    have "(f has_contour_integral I ω1 (ω1 + ω2)) (L ω1 (ω1 + ω2))"
      by (rule I) (auto simp: parallelogram_path_def path_image_join P_def add_ac)
    also have "L ω1 (ω1 + ω2) = (+) ω1 ∘ L 0 ω2"
      by (simp add: linepath_def L_def fun_eq_iff algebra_simps)
    finally have "((λx. f (x + ω1)) has_contour_integral I ω1 (ω1 + ω2)) (L 0 ω2)"
      unfolding has_contour_integral_translate .
    hence "((λx. f x - f (x + ω1)) has_contour_integral (I 0 ω2 - I ω1 (ω1 + ω2))) (L 0 ω2)"
      by (intro has_contour_integral_diff I) 
         (auto simp: parallelogram_path_def path_image_join closed_segment_commute L_def P_def)
    thus ?thesis
      by (rule contour_integral_unique [symmetric])
  qed

  also have "I 0 ω1 - I ω2 (ω1 + ω2) = contour_integral (L 0 ω1) (λx. f x - f (x + ω2))"
  proof -
    have "(f has_contour_integral I ω2 (ω1 + ω2)) (L ω2 (ω1 + ω2))"
      by (rule I) (auto simp: parallelogram_path_def path_image_join closed_segment_commute P_def L_def add_ac)
    also have "L ω2 (ω1 + ω2) = (+) ω2 ∘ L 0 ω1"
      by (simp add: linepath_def L_def o_def algebra_simps)
    finally have "((λx. f (x + ω2)) has_contour_integral I ω2 (ω1 + ω2)) (L 0 ω1)"
      unfolding has_contour_integral_translate .
    hence "((λx. f x - f (x + ω2)) has_contour_integral (I 0 ω1 - I ω2 (ω1 + ω2))) (L 0 ω1)"
      by (intro has_contour_integral_diff I) 
         (auto simp: parallelogram_path_def path_image_join closed_segment_commute P_def)
    thus ?thesis
      by (rule contour_integral_unique [symmetric])
  qed

  finally show "contour_integral P f =
                  contour_integral (linepath z (z + ω1)) (λx. f x - f (x + ω2)) -
                  contour_integral (linepath z (z + ω2)) (λx. f x - f (x + ω1))"
    by (simp add: L_def add_ac)
qed

end