Theory Winding_Number_Eval.Missing_Analysis
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 "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)"
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 "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