Theory Missing_Analysis

theory Missing_Analysis
imports Complex_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)" 
    apply (rule continuous_intros)
    by (intro continuous_intros)
  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)"
proof (rule ccontr)
  assume "¬ z ∉ path_image (part_circlepath z0 r st tt)"
  then have "z∈path_image (part_circlepath z0 r st tt)" by simp
  then obtain t where "t∈{0..1}" and *:"z = z0 + r * exp (𝗂 * (linepath st tt t))"
    unfolding path_image_def image_def part_circlepath_def by blast
  define θ where "θ = linepath st tt t"
  then have "z-z0 = r * exp (𝗂 * θ)" using * by auto
  then have "cmod (z-z0) = cmod (r * exp (𝗂 * θ))" by auto
  also have "… = ¦r¦ * cmod (exp (𝗂 * θ))" by (simp add: norm_mult)
  also have "… = ¦r¦" by auto
  finally have "cmod (z-z0) = ¦r¦" .
  then show False using assms by auto
qed    

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 "c≠0" 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 ‹c≠0›
    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)"
      apply (subst vector_derivative_chain_at_general)
      by (simp_all add:field_simps)
  qed
  moreover note ‹z ∉ path_image (f ∘ γ)› 
  ultimately show ?thesis
    apply (subst winding_number_valid_path)
    by simp_all
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 "c≠0" "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 ‹c≠0› 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 ‹c≠0›
      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