Theory Winding_Number_Eval.Missing_Analysis

(*
    Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section ‹Some useful lemmas in analysis›

theory Missing_Analysis
  imports "HOL-Complex_Analysis.Complex_Analysis"
begin  

subsection ‹More about paths›
   
lemma pathfinish_offset[simp]:
  "pathfinish (λt. g t - z) = pathfinish g - z"
  unfolding pathfinish_def by simp 
    
lemma pathstart_offset[simp]:
  "pathstart (λt. g t - z) = pathstart g - z"
  unfolding pathstart_def by simp
    
lemma pathimage_offset[simp]:
  fixes g :: "_  'b::topological_group_add"
  shows "p  path_image (λt. g t - z)  p+z  path_image g " 
unfolding path_image_def by (auto simp:algebra_simps)
  
lemma path_offset[simp]:
 fixes g :: "_  'b::topological_group_add"
 shows "path (λt. g t - z)  path g"
unfolding path_def
proof 
  assume "continuous_on {0..1} (λt. g t - z)" 
  hence "continuous_on {0..1} (λt. (g t - z) + z)"
    using continuous_on_add continuous_on_const by blast 
  then show "continuous_on {0..1} g" by auto
qed (auto intro:continuous_intros)   
  
lemma not_on_circlepathI:
  assumes "cmod (z-z0)  ¦r¦"
  shows "z  path_image (part_circlepath z0 r st tt)"
  using assms
  by (auto simp add: path_image_def image_def part_circlepath_def norm_mult)

lemma circlepath_inj_on: 
  assumes "r>0"
  shows "inj_on (circlepath z r) {0..<1}"
proof (rule inj_onI)
  fix x y assume asm: "x  {0..<1}" "y  {0..<1}" "circlepath z r x = circlepath z r y"
  define c where "c=2 * pi * 𝗂"
  have "c0" unfolding c_def by auto 
  from asm(3) have "exp (c * x) =exp (c * y)"
    unfolding circlepath c_def using r>0 by auto
  then obtain n where "c * x =c * (y + of_int n)"
    by (auto simp add:exp_eq c_def algebra_simps)
  then have "x=y+n" using c0
    by (meson mult_cancel_left of_real_eq_iff)
  then show "x=y" using asm(1,2) by auto
qed

subsection ‹More lemmas related to @{term winding_number}  
  
lemma winding_number_comp:
  assumes "open s" "f holomorphic_on s" "path_image γ  s"  
    "valid_path γ" "z  path_image (f  γ)" 
  shows "winding_number (f  γ) z = 1/(2*pi*𝗂)* contour_integral γ (λw. deriv f w / (f w - z))"
proof -
  obtain spikes where "finite spikes" and γ_diff: "γ C1_differentiable_on {0..1} - spikes"
    using valid_path γ unfolding valid_path_def piecewise_C1_differentiable_on_def by auto  
  have "valid_path (f  γ)" 
    using valid_path_compose_holomorphic assms by blast
  moreover have "contour_integral (f  γ) (λw. 1 / (w - z)) 
      = contour_integral γ (λw. deriv f w / (f w - z))"
    unfolding contour_integral_integral
  proof (rule integral_spike[rule_format,OF negligible_finite[OF finite spikes]])
    fix t::real assume t:"t  {0..1} - spikes"
    then have "γ differentiable at t" 
      using γ_diff unfolding C1_differentiable_on_eq by auto
    moreover have "f field_differentiable at (γ t)" 
    proof -
      have "γ t  s" using path_image γ  s t unfolding path_image_def by auto 
      thus ?thesis 
        using open s f holomorphic_on s  holomorphic_on_imp_differentiable_at by blast
    qed
    ultimately show " deriv f (γ t) / (f (γ t) - z) * vector_derivative γ (at t) =
         1 / ((f  γ) t - z) * vector_derivative (f  γ) (at t)"
      by (simp add: vector_derivative_chain_at_general)
  qed
  moreover note z  path_image (f  γ) 
  ultimately show ?thesis
    using winding_number_valid_path by presburger
qed  
  
lemma winding_number_uminus_comp:
  assumes "valid_path γ" "- z  path_image γ" 
  shows "winding_number (uminus  γ) z = winding_number γ (-z)"
proof -
  define c where "c= 2 * pi * 𝗂"
  have "winding_number (uminus  γ) z = 1/c * contour_integral γ (λw. deriv uminus w / (-w-z)) "
  proof (rule winding_number_comp[of UNIV, folded c_def])
    show "open UNIV" "uminus holomorphic_on UNIV" "path_image γ  UNIV" "valid_path γ"
      using valid_path γ by (auto intro:holomorphic_intros)
    show "z  path_image (uminus  γ)" 
      unfolding path_image_compose using - z  path_image γ by auto
  qed
  also have " = 1/c * contour_integral γ (λw. 1 / (w- (-z)))"
    by (auto intro!:contour_integral_eq simp add:field_simps minus_divide_right)
  also have " = winding_number γ (-z)"
    using winding_number_valid_path[OF valid_path γ - z  path_image γ,folded c_def]
    by simp
  finally show ?thesis by auto
qed  
  
lemma winding_number_comp_linear:
  assumes "c0" "valid_path γ" and not_image: "(z-b)/c  path_image γ"
  shows "winding_number ((λx. c*x+b)  γ) z = winding_number γ ((z-b)/c)" (is "?L = ?R")
proof -
  define cc where "cc=1 / (complex_of_real (2 * pi) * 𝗂)"
  define zz where "zz=(z-b)/c"
  have "?L = cc * contour_integral γ (λw. deriv (λx. c * x + b) w / (c * w + b - z))"
    apply (subst winding_number_comp[of UNIV,simplified])
    subgoal by (auto intro:holomorphic_intros)
    subgoal using valid_path γ .
    subgoal using not_image c0 unfolding path_image_compose by auto
    subgoal unfolding cc_def by auto
    done
  also have " = cc * contour_integral γ (λw.1 / (w - zz))"
  proof -
    have "deriv (λx. c * x + b) = (λx. c)"
      by (auto intro:derivative_intros) 
    then show ?thesis
      unfolding zz_def cc_def using c0
      by (auto simp:field_simps)
  qed
  also have " = winding_number γ zz"
    using winding_number_valid_path[OF valid_path γ not_image,folded zz_def cc_def]
    by simp
  finally show "winding_number ((λx. c * x + b)  γ) z = winding_number γ zz" .
qed  
 
end