(* 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