Theory Cauchy_Index_Theorem
section ‹Cauchy's index theorem›
theory Cauchy_Index_Theorem imports
"HOL-Complex_Analysis.Complex_Analysis"
"Sturm_Tarski.Sturm_Tarski"
"HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
Missing_Transcendental
Missing_Algebraic
Missing_Analysis
begin
text ‹This theory formalises Cauchy indices on the complex plane and relate them to winding numbers›
subsection ‹Misc›
lemma atMostAtLeast_subset_convex:
fixes C :: "real set"
assumes "convex C"
and "x ∈ C" "y ∈ C"
shows "{x .. y} ⊆ C"
proof safe
fix z assume z: "z ∈ {x .. y}"
have "z ∈ C" if *: "x < z" "z < y"
proof -
let ?μ = "(y - z) / (y - x)"
have "0 ≤ ?μ" "?μ ≤ 1"
using assms * by (auto simp: field_simps)
then have comb: "?μ * x + (1 - ?μ) * y ∈ C"
using assms iffD1[OF convex_alt, rule_format, of C y x ?μ]
by (simp add: algebra_simps)
have "?μ * x + (1 - ?μ) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y"
by (auto simp: field_simps)
also have "… = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)"
using * by (simp only: add_divide_distrib) (auto simp: field_simps)
also have "… = z"
using assms * by (auto simp: field_simps)
finally show ?thesis
using comb by auto
qed
then show "z ∈ C"
using z assms by (auto simp: le_less)
qed
lemma arg_elim:
"f x ⟹ x= y ⟹ f y"
by auto
lemma arg_elim2:
"f x1 x2 ⟹ x1= y1 ⟹x2=y2 ⟹ f y1 y2"
by auto
lemma arg_elim3:
"⟦f x1 x2 x3;x1= y1;x2=y2;x3=y3 ⟧ ⟹ f y1 y2 y3"
by auto
lemma IVT_strict:
fixes f :: "'a::linear_continuum_topology ⇒ 'b::linorder_topology"
assumes "(f a > y ∧ y > f b) ∨ (f a < y ∧ y < f b)" "a<b" "continuous_on {a .. b} f"
shows "∃x. a < x ∧ x < b ∧ f x = y"
by (metis IVT' IVT2' assms(1) assms(2) assms(3) linorder_neq_iff order_le_less order_less_imp_le)
lemma (in dense_linorder) atLeastAtMost_subseteq_greaterThanLessThan_iff:
"{a .. b} ⊆ { c <..< d } ⟷ (a ≤ b ⟶ c < a ∧ b < d)"
using dense[of "a" "min c b"] dense[of "max a d" "b"]
by (force simp: subset_eq Ball_def not_less[symmetric])
lemma Re_winding_number_half_right:
assumes "∀p∈path_image γ. Re p ≥ Re z" and "valid_path γ" and "z∉path_image γ"
shows "Re(winding_number γ z) = (Im (Ln (pathfinish γ - z)) - Im (Ln (pathstart γ - z)))/(2*pi)"
proof -
define g where "g=(λt. γ t - z)"
define st fi where "st≡pathstart g" and "fi≡pathfinish g"
have "valid_path g" "0∉path_image g" and pos_img:"∀p∈path_image g. Re p ≥ 0" unfolding g_def
subgoal using assms(2) by auto
subgoal using assms(3) by auto
subgoal using assms(1) by fastforce
done
have "(inverse has_contour_integral Ln fi - Ln st) g"
unfolding fi_def st_def
proof (rule contour_integral_primitive[OF _ ‹valid_path g›,of " - ℝ⇩≤⇩0"])
fix x::complex assume "x ∈ - ℝ⇩≤⇩0"
then have "(Ln has_field_derivative inverse x) (at x)" using has_field_derivative_Ln
by auto
then show "(Ln has_field_derivative inverse x) (at x within - ℝ⇩≤⇩0)"
using has_field_derivative_at_within by auto
next
show "path_image g ⊆ - ℝ⇩≤⇩0" using pos_img ‹0∉path_image g›
by (metis ComplI antisym assms(3) complex_nonpos_Reals_iff complex_surj
subsetI zero_complex.code)
qed
then have winding_eq:"2*pi*𝗂*winding_number g 0 = (Ln fi - Ln st)"
using has_contour_integral_winding_number[OF ‹valid_path g› ‹0∉path_image g›
,simplified,folded inverse_eq_divide] has_contour_integral_unique
by auto
have "Re(winding_number g 0)
= (Im (Ln fi) - Im (Ln st))/(2*pi)"
(is "?L=?R")
proof -
have "?L = Re((Ln fi - Ln st)/(2*pi*𝗂))"
using winding_eq[symmetric] by auto
also have "... = ?R"
by (metis Im_divide_of_real Im_i_times complex_i_not_zero minus_complex.simps(2)
mult.commute mult_divide_mult_cancel_left_if times_divide_eq_right)
finally show ?thesis .
qed
then show ?thesis unfolding g_def fi_def st_def using winding_number_offset by simp
qed
lemma Re_winding_number_half_upper:
assumes pimage:"∀p∈path_image γ. Im p ≥ Im z" and "valid_path γ" and "z∉path_image γ"
shows "Re(winding_number γ z) =
(Im (Ln (𝗂*z - 𝗂*pathfinish γ)) - Im (Ln (𝗂*z - 𝗂*pathstart γ )))/(2*pi)"
proof -
define γ' where "γ'=(λt. - 𝗂 * (γ t - z) + z)"
have "Re (winding_number γ' z) = (Im (Ln (pathfinish γ' - z)) - Im (Ln (pathstart γ' - z))) / (2 * pi)"
unfolding γ'_def
apply (rule Re_winding_number_half_right)
subgoal using pimage unfolding path_image_def by auto
subgoal
apply (rule valid_path_compose_holomorphic[OF ‹valid_path γ›,of "λx. -𝗂 * (x-z) + z" UNIV
, unfolded comp_def])
by (auto intro!:holomorphic_intros)
subgoal using ‹z∉path_image γ› unfolding path_image_def by auto
done
moreover have "winding_number γ' z = winding_number γ z"
proof -
define f where "f=(λx. -𝗂 * (x-z) + z)"
define c where "c= 1 / (complex_of_real (2 * pi) * 𝗂)"
have "winding_number γ' z = winding_number (f o γ) z"
unfolding γ'_def comp_def f_def by auto
also have "... = c * contour_integral γ (λw. deriv f w / (f w - z))" unfolding c_def
proof (rule winding_number_comp[of UNIV])
show "z ∉ path_image (f ∘ γ)" using ‹z∉path_image γ› unfolding f_def path_image_def by auto
qed (auto simp add:f_def ‹valid_path γ› intro!:holomorphic_intros)
also have "... = c * contour_integral γ (λw. 1 / (w - z))"
proof -
have "deriv f x = -𝗂" for x
unfolding f_def
by (auto intro!:derivative_eq_intros DERIV_imp_deriv)
then show ?thesis
unfolding f_def c_def
by (auto simp add:field_simps divide_simps intro!:arg_cong2[where f=contour_integral])
qed
also have "... = winding_number γ z"
using winding_number_valid_path[OF ‹valid_path γ› ‹z∉path_image γ›,folded c_def] by simp
finally show ?thesis .
qed
moreover have "pathfinish γ' = z+ 𝗂*z -𝗂* pathfinish γ" "pathstart γ' = z+ 𝗂*z -𝗂*pathstart γ"
unfolding γ'_def path_defs by (auto simp add:algebra_simps)
ultimately show ?thesis by auto
qed
lemma Re_winding_number_half_lower:
assumes pimage:"∀p∈path_image γ. Im p ≤ Im z" and "valid_path γ" and "z∉path_image γ"
shows "Re(winding_number γ z) =
(Im (Ln ( 𝗂*pathfinish γ - 𝗂*z)) - Im (Ln (𝗂*pathstart γ - 𝗂*z)))/(2*pi)"
proof -
define γ' where "γ'=(λt. 𝗂 * (γ t - z) + z)"
have "Re (winding_number γ' z) = (Im (Ln (pathfinish γ' - z)) - Im (Ln (pathstart γ' - z))) / (2 * pi)"
unfolding γ'_def
apply (rule Re_winding_number_half_right)
subgoal using pimage unfolding path_image_def by auto
subgoal
apply (rule valid_path_compose_holomorphic[OF ‹valid_path γ›,of "λx. 𝗂 * (x-z) + z" UNIV
, unfolded comp_def])
by (auto intro!:holomorphic_intros)
subgoal using ‹z∉path_image γ› unfolding path_image_def by auto
done
moreover have "winding_number γ' z = winding_number γ z"
proof -
define f where "f=(λx. 𝗂 * (x-z) + z)"
define c where "c= 1 / (complex_of_real (2 * pi) * 𝗂)"
have "winding_number γ' z = winding_number (f o γ) z"
unfolding γ'_def comp_def f_def by auto
also have "... = c * contour_integral γ (λw. deriv f w / (f w - z))" unfolding c_def
proof (rule winding_number_comp[of UNIV])
show "z ∉ path_image (f ∘ γ)" using ‹z∉path_image γ› unfolding f_def path_image_def by auto
qed (auto simp add:f_def ‹valid_path γ› intro!:holomorphic_intros)
also have "... = c * contour_integral γ (λw. 1 / (w - z))"
proof -
have "deriv f x = 𝗂" for x
unfolding f_def
by (auto intro!:derivative_eq_intros DERIV_imp_deriv)
then show ?thesis
unfolding f_def c_def
by (auto simp add:field_simps divide_simps intro!:arg_cong2[where f=contour_integral])
qed
also have "... = winding_number γ z"
using winding_number_valid_path[OF ‹valid_path γ› ‹z∉path_image γ›,folded c_def] by simp
finally show ?thesis .
qed
moreover have "pathfinish γ' = z+ 𝗂* pathfinish γ - 𝗂*z" "pathstart γ' = z+ 𝗂*pathstart γ - 𝗂*z"
unfolding γ'_def path_defs by (auto simp add:algebra_simps)
ultimately show ?thesis by auto
qed
lemma Re_winding_number_half_left:
assumes neg_img:"∀p∈path_image γ. Re p ≤ Re z" and "valid_path γ" and "z∉path_image γ"
shows "Re(winding_number γ z) = (Im (Ln (z - pathfinish γ)) - Im (Ln (z - pathstart γ )))/(2*pi)"
proof -
define γ' where "γ'≡(λt. 2*z - γ t)"
have "Re (winding_number γ' z) = (Im (Ln (pathfinish γ' - z)) - Im (Ln (pathstart γ' - z))) / (2 * pi)"
unfolding γ'_def
apply (rule Re_winding_number_half_right)
subgoal using neg_img unfolding path_image_def by auto
subgoal
apply (rule valid_path_compose_holomorphic[OF ‹valid_path γ›,of "λt. 2*z-t" UNIV,
unfolded comp_def])
by (auto intro:holomorphic_intros)
subgoal using ‹z∉path_image γ› unfolding path_image_def by auto
done
moreover have "winding_number γ' z = winding_number γ z"
proof -
define f where "f=(λt. 2*z-t)"
define c where "c= 1 / (complex_of_real (2 * pi) * 𝗂)"
have "winding_number γ' z = winding_number (f o γ) z"
unfolding γ'_def comp_def f_def by auto
also have "... = c * contour_integral γ (λw. deriv f w / (f w - z))" unfolding c_def
proof (rule winding_number_comp[of UNIV])
show "z ∉ path_image (f ∘ γ)" using ‹z∉path_image γ› unfolding f_def path_image_def by auto
qed (auto simp add:f_def ‹valid_path γ› intro:holomorphic_intros)
also have "... = c * contour_integral γ (λw. 1 / (w - z))"
unfolding f_def c_def
by (auto simp add:field_simps divide_simps intro!:arg_cong2[where f=contour_integral])
also have "... = winding_number γ z"
using winding_number_valid_path[OF ‹valid_path γ› ‹z∉path_image γ›,folded c_def] by simp
finally show ?thesis .
qed
moreover have "pathfinish γ' = 2*z - pathfinish γ" "pathstart γ' = 2*z - pathstart γ"
unfolding γ'_def path_defs by auto
ultimately show ?thesis by auto
qed
lemma continuous_on_open_Collect_neq:
fixes f g :: "'a::topological_space ⇒ 'b::t2_space"
assumes f: "continuous_on S f" and g: "continuous_on S g" and "open S"
shows "open {x∈S. f x ≠ g x}"
proof (rule topological_space_class.openI)
fix t
assume "t ∈ {x∈S. f x ≠ g x}"
then obtain U0 V0 where "open U0" "open V0" "f t ∈ U0" "g t ∈ V0" "U0 ∩ V0 = {}" "t∈S"
by (auto simp add: separation_t2)
obtain U1 where "open U1" "t ∈ U1" "∀y∈(S ∩ U1). f y ∈ U0"
using f[unfolded continuous_on_topological,rule_format,OF ‹t∈S› ‹open U0› ‹f t ∈U0›] by auto
obtain V1 where "open V1" "t ∈ V1" "∀y∈(S ∩ V1). g y ∈ V0"
using g[unfolded continuous_on_topological,rule_format,OF ‹t∈S› ‹open V0› ‹g t ∈V0›] by auto
define T where "T=V1 ∩ U1 ∩ S"
have "open T" unfolding T_def using ‹open U1› ‹open V1› ‹open S› by auto
moreover have "t ∈ T" unfolding T_def using ‹t∈U1› ‹t∈V1› ‹t∈S› by auto
moreover have "T ⊆ {x ∈ S. f x ≠ g x}" unfolding T_def
using ‹U0 ∩ V0 = {}› ‹∀y∈S ∩ U1. f y ∈ U0› ‹∀y∈S ∩ V1. g y ∈ V0› by auto
ultimately show "∃T. open T ∧ t ∈ T ∧ T ⊆ {x ∈ S. f x ≠ g x}" by auto
qed
subsection ‹Sign at a filter›
definition has_sgnx::"(real ⇒ real) ⇒ real ⇒ real filter ⇒ bool"
(infixr "has'_sgnx" 55) where
"(f has_sgnx c) F= (eventually (λx. sgn(f x) = c) F)"
definition sgnx_able (infixr "sgnx'_able" 55) where
"(f sgnx_able F) = (∃c. (f has_sgnx c) F)"
definition sgnx where
"sgnx f F = (SOME c. (f has_sgnx c) F)"
lemma has_sgnx_eq_rhs: "(f has_sgnx x) F ⟹ x = y ⟹ (f has_sgnx y) F"
by simp
named_theorems sgnx_intros "introduction rules for has_sgnx"
setup ‹
Global_Theory.add_thms_dynamic (@{binding sgnx_eq_intros},
fn context =>
Named_Theorems.get (Context.proof_of context) @{named_theorems sgnx_intros}
|> map_filter (try (fn thm => @{thm has_sgnx_eq_rhs} OF [thm])))
›
lemma sgnx_able_sgnx:"f sgnx_able F ⟹ (f has_sgnx (sgnx f F)) F"
unfolding sgnx_able_def sgnx_def using someI_ex by metis
lemma has_sgnx_imp_sgnx_able[elim]:
"(f has_sgnx c) F ⟹ f sgnx_able F"
unfolding sgnx_able_def by auto
lemma has_sgnx_unique:
assumes "F≠bot" "(f has_sgnx c1) F" "(f has_sgnx c2) F"
shows "c1=c2"
proof (rule ccontr)
assume "c1 ≠ c2 "
have "eventually (λx. sgn(f x) = c1 ∧ sgn(f x) = c2) F"
using assms unfolding has_sgnx_def eventually_conj_iff by simp
then have "eventually (λ_. c1 = c2) F" by (elim eventually_mono,auto)
then have "eventually (λ_. False) F" using ‹c1 ≠ c2› by auto
then show False using ‹F ≠ bot› eventually_False by auto
qed
lemma has_sgnx_imp_sgnx[elim]:
"(f has_sgnx c) F ⟹F≠bot ⟹ sgnx f F = c"
using has_sgnx_unique sgnx_def by auto
lemma has_sgnx_const[simp,sgnx_intros]:
"((λ_. c) has_sgnx sgn c) F"
by (simp add: has_sgnx_def)
lemma finite_sgnx_at_left_at_right:
assumes "finite {t. f t=0 ∧ a<t ∧ t<b}" "continuous_on ({a<..<b} - s) f" "finite s"
and x:"x∈{a<..<b}"
shows "f sgnx_able (at_left x)" "sgnx f (at_left x)≠0"
"f sgnx_able (at_right x)" "sgnx f (at_right x)≠0"
proof -
define ls where "ls ≡ {t. (f t=0 ∨ t∈s) ∧ a<t ∧t<x }"
define l where "l≡(if ls = {} then (a+x)/2 else (Max ls + x)/2)"
have "finite ls"
proof -
have "{t. f t=0 ∧ a<t ∧ t<x} ⊆ {t. f t=0 ∧ a<t ∧ t<b}" using x by auto
then have "finite {t. f t=0 ∧ a<t ∧ t<x}" using assms(1)
using finite_subset by blast
moreover have "finite {t. t∈s ∧ a<t ∧ t<x}" using assms(3) by auto
moreover have "ls = {t. f t=0 ∧ a<t ∧ t<x} ∪ {t. t∈s ∧ a<t ∧ t<x}"
unfolding ls_def by auto
ultimately show ?thesis by auto
qed
have [simp]: "l<x" "a<l" "l<b"
proof -
have "l<x ∧ a<l ∧ l<b" when "ls = {}"
using that x unfolding l_def by auto
moreover have "l<x ∧ a<l ∧ l<b" when "ls ≠{}"
proof -
have "Max ls ∈ ls" using assms(1,3) that ‹finite ls›
apply (intro linorder_class.Max_in)
by auto
then have "a<Max ls ∧ Max ls < x" unfolding ls_def by auto
then show ?thesis unfolding l_def using that x by auto
qed
ultimately show "l<x" "a<l" "l<b" by auto
qed
have noroot:"f t≠0" when t:"t∈{l..<x}" for t
proof (cases "ls = {}")
case True
have False when "f t=0"
proof -
have "t>a" using t ‹l>a› by (meson atLeastLessThan_iff less_le_trans)
then have "t∈ls" using that t unfolding ls_def by auto
then show False using True by auto
qed
then show ?thesis by auto
next
case False
have "t>Max ls" using that False ‹l<x› unfolding l_def by auto
have False when "f t=0"
proof -
have "t>a" using t ‹l>a› by (meson atLeastLessThan_iff less_le_trans)
then have "t∈ls" using that t unfolding ls_def by auto
then have "t≤Max ls" using ‹finite ls› by auto
then show False using ‹t>Max ls› by auto
qed
then show ?thesis by auto
qed
have "(f has_sgnx sgn (f l)) (at_left x)" unfolding has_sgnx_def
proof (rule eventually_at_leftI[OF _ ‹l<x›])
fix t assume t:"t∈{l<..<x}"
then have [simp]:"t>a" "t<b" using ‹l>a› x
by (meson greaterThanLessThan_iff less_trans)+
have False when "f t = 0"
using noroot t that by auto
moreover have False when "f l=0"
using noroot t that by auto
moreover have False when "f l>0 ∧ f t<0 ∨ f l <0 ∧ f t >0"
proof -
have False when "{l..t} ∩ s ≠{}"
proof -
obtain t' where t':"t'∈{l..t}" "t'∈s"
using ‹{l..t} ∩ s ≠ {}› by blast
then have "a<t' ∧ t'<x"
by (metis ‹a < l› atLeastAtMost_iff greaterThanLessThan_iff le_less less_trans t)
then have "t'∈ls" unfolding ls_def using ‹t'∈s› by auto
then have "t'≤Max ls" using ‹finite ls› by auto
moreover have "Max ls<l"
using ‹l<x› ‹t'∈ls› ‹finite ls› unfolding l_def by (auto simp add:ls_def )
ultimately show False using t'(1) by auto
qed
moreover have "{l..t} ⊆ {a<..<b}"
by (intro atMostAtLeast_subset_convex,auto)
ultimately have "continuous_on {l..t} f" using assms(2)
by (elim continuous_on_subset,auto)
then have "∃x>l. x < t ∧ f x = 0"
apply (intro IVT_strict)
using that t assms(2) by auto
then obtain t' where "l<t'" "t'<t" "f t'=0" by auto
then have "t'∈{l..<x}" unfolding ls_def using t by auto
then show False using noroot ‹f t'=0› by auto
qed
ultimately show "sgn (f t) = sgn (f l)"
by (metis le_less not_less sgn_if)
qed
then show "f sgnx_able (at_left x)" by auto
show "sgnx f (at_left x)≠0"
using noroot[of l,simplified] ‹(f has_sgnx sgn (f l)) (at_left x)›
by (simp add: has_sgnx_imp_sgnx sgn_if)
next
define rs where "rs ≡ {t. (f t=0 ∨ t∈s) ∧ x<t ∧ t<b}"
define r where "r≡(if rs = {} then (x+b)/2 else (Min rs + x)/2)"
have "finite rs"
proof -
have "{t. f t=0 ∧ x<t ∧ t<b} ⊆ {t. f t=0 ∧ a<t ∧ t<b}" using x by auto
then have "finite {t. f t=0 ∧ x<t ∧ t<b}" using assms(1)
using finite_subset by blast
moreover have "finite {t. t∈s ∧ x<t ∧ t<b}" using assms(3) by auto
moreover have "rs = {t. f t=0 ∧ x<t ∧ t<b} ∪ {t. t∈s ∧ x<t ∧ t<b}"
unfolding rs_def by auto
ultimately show ?thesis by auto
qed
have [simp]: "r>x" "a<r" "r<b"
proof -
have "r>x ∧ a<r ∧ r<b" when "rs = {}"
using that x unfolding r_def by auto
moreover have "r>x ∧ a<r ∧ r<b" when "rs ≠{}"
proof -
have "Min rs ∈ rs" using assms(1,3) that ‹finite rs›
apply (intro linorder_class.Min_in)
by auto
then have "x<Min rs ∧ Min rs < b" unfolding rs_def by auto
then show ?thesis unfolding r_def using that x by auto
qed
ultimately show "r>x" "a<r" "r<b" by auto
qed
have noroot:"f t≠0" when t:"t∈{x<..r}" for t
proof (cases "rs = {}")
case True
have False when "f t=0"
proof -
have "t<b" using t ‹r<b›
using greaterThanAtMost_iff by fastforce
then have "t∈rs" using that t unfolding rs_def by auto
then show False using True by auto
qed
then show ?thesis by auto
next
case False
have "t<Min rs" using that False ‹r>x› unfolding r_def by auto
have False when "f t=0"
proof -
have "t<b" using t ‹r<b› by (metis greaterThanAtMost_iff le_less less_trans)
then have "t∈rs" using that t unfolding rs_def by auto
then have "t≥Min rs" using ‹finite rs› by auto
then show False using ‹t<Min rs› by auto
qed
then show ?thesis by auto
qed
have "(f has_sgnx sgn (f r)) (at_right x)" unfolding has_sgnx_def
proof (rule eventually_at_rightI[OF _ ‹r>x›])
fix t assume t:"t∈{x<..<r}"
then have [simp]:"t>a" "t<b" using ‹r<b› x
by (meson greaterThanLessThan_iff less_trans)+
have False when "f t = 0"
using noroot t that by auto
moreover have False when "f r=0"
using noroot t that by auto
moreover have False when "f r>0 ∧ f t<0 ∨ f r <0 ∧ f t >0"
proof -
have False when "{t..r} ∩ s ≠{}"
proof -
obtain t' where t':"t'∈{t..r}" "t'∈s"
using ‹{t..r} ∩ s ≠ {}› by blast
then have "x<t' ∧ t'<b"
by (meson ‹r < b› atLeastAtMost_iff greaterThanLessThan_iff less_le_trans not_le t)
then have "t'∈rs" unfolding rs_def using t ‹t'∈s› by auto
then have "t'≥Min rs" using ‹finite rs› by auto
moreover have "Min rs>r"
using ‹r>x› ‹t'∈rs› ‹finite rs› unfolding r_def by (auto simp add:rs_def )
ultimately show False using t'(1) by auto
qed
moreover have "{t..r} ⊆ {a<..<b}"
by (intro atMostAtLeast_subset_convex,auto)
ultimately have "continuous_on {t..r} f" using assms(2) by (elim continuous_on_subset,auto)
then have "∃x>t. x < r ∧ f x = 0"
apply (intro IVT_strict)
using that t assms(2) by auto
then obtain t' where "t<t'" "t'<r" "f t'=0" by auto
then have "t'∈{x<..r}" unfolding rs_def using t by auto
then show False using noroot ‹f t'=0› by auto
qed
ultimately show "sgn (f t) = sgn (f r)"
by (metis le_less not_less sgn_if)
qed
then show "f sgnx_able (at_right x)" by auto
show "sgnx f (at_right x)≠0"
using noroot[of r,simplified] ‹(f has_sgnx sgn (f r)) (at_right x)›
by (simp add: has_sgnx_imp_sgnx sgn_if)
qed
lemma sgnx_able_poly[simp]:
"(poly p) sgnx_able (at_right a)"
"(poly p) sgnx_able (at_left a)"
"(poly p) sgnx_able at_top"
"(poly p) sgnx_able at_bot"
proof -
show "(poly p) sgnx_able at_top"
using has_sgnx_def poly_sgn_eventually_at_top sgnx_able_def by blast
show "(poly p) sgnx_able at_bot"
using has_sgnx_def poly_sgn_eventually_at_bot sgnx_able_def by blast
show "(poly p) sgnx_able (at_right a)"
proof (cases "p=0")
case True
then show ?thesis unfolding sgnx_able_def has_sgnx_def eventually_at_right
using linordered_field_no_ub by force
next
case False
obtain ub where "ub>a" and ub:"∀z. a<z∧z≤ub⟶poly p z≠0"
using next_non_root_interval[OF False] by auto
have "∀z. a<z∧z≤ub⟶sgn(poly p z) = sgn (poly p ub)"
proof (rule ccontr)
assume "¬ (∀z. a < z ∧ z ≤ ub ⟶ sgn (poly p z) = sgn (poly p ub))"
then obtain z where "a<z" "z≤ub" "sgn(poly p z) ≠ sgn (poly p ub)" by auto
moreover then have "poly p z≠0" "poly p ub≠0" "z≠ub" using ub ‹ub>a› by blast+
ultimately have "(poly p z>0 ∧ poly p ub<0) ∨ (poly p z<0 ∧ poly p ub>0)"
by (metis linorder_neqE_linordered_idom sgn_neg sgn_pos)
then have "∃x>z. x < ub ∧ poly p x = 0"
using poly_IVT_neg[of z ub p] poly_IVT_pos[of z ub p] ‹z≤ub› ‹z≠ub› by argo
then show False using ub ‹a < z› by auto
qed
then show ?thesis unfolding sgnx_able_def has_sgnx_def eventually_at_right
apply (rule_tac exI[where x="sgn(poly p ub)"])
apply (rule_tac exI[where x="ub"])
using less_eq_real_def ‹ub>a› by blast
qed
show "(poly p) sgnx_able (at_left a)"
proof (cases "p=0")
case True
then show ?thesis unfolding sgnx_able_def has_sgnx_def eventually_at_right
using linordered_field_no_ub by force
next
case False
obtain lb where "lb<a" and ub:"∀z. lb≤z∧z<a⟶poly p z≠0"
using last_non_root_interval[OF False] by auto
have "∀z. lb≤z∧z<a⟶sgn(poly p z) = sgn (poly p lb)"
proof (rule ccontr)
assume "¬ (∀z. lb≤z∧z<a ⟶ sgn (poly p z) = sgn (poly p lb))"
then obtain z where "lb≤z" "z<a" "sgn(poly p z) ≠ sgn (poly p lb)" by auto
moreover then have "poly p z≠0" "poly p lb≠0" "z≠lb" using ub ‹lb<a› by blast+
ultimately have "(poly p z>0 ∧ poly p lb<0) ∨ (poly p z<0 ∧ poly p lb>0)"
by (metis linorder_neqE_linordered_idom sgn_neg sgn_pos)
then have "∃x>lb. x < z ∧ poly p x = 0"
using poly_IVT_neg[of lb z p] poly_IVT_pos[of lb z p] ‹lb≤z› ‹z≠lb› by argo
then show False using ub ‹z < a› by auto
qed
then show ?thesis unfolding sgnx_able_def has_sgnx_def eventually_at_left
apply (rule_tac exI[where x="sgn(poly p lb)"])
apply (rule_tac exI[where x="lb"])
using less_eq_real_def ‹lb<a› by blast
qed
qed
lemma has_sgnx_identity[intro,sgnx_intros]:
shows "x≥0 ⟹((λx. x) has_sgnx 1) (at_right x)"
"x≤0 ⟹ ((λx. x) has_sgnx -1) (at_left x)"
proof -
show "x≥0 ⟹ ((λx. x) has_sgnx 1) (at_right x)"
unfolding has_sgnx_def eventually_at_right
apply (intro exI[where x="x+1"])
by auto
show "x≤0 ⟹ ((λx. x) has_sgnx -1) (at_left x)"
unfolding has_sgnx_def eventually_at_left
apply (intro exI[where x="x-1"])
by auto
qed
lemma has_sgnx_divide[sgnx_intros]:
assumes "(f has_sgnx c1) F" "(g has_sgnx c2) F"
shows "((λx. f x / g x) has_sgnx c1 / c2) F"
proof -
have "∀⇩F x in F. sgn (f x) = c1 ∧ sgn (g x) = c2"
using assms unfolding has_sgnx_def by (intro eventually_conj,auto)
then have "∀⇩F x in F. sgn (f x / g x) = c1 / c2"
apply (elim eventually_mono)
by (simp add: sgn_mult sgn_divide)
then show "((λx. f x / g x) has_sgnx c1 / c2) F" unfolding has_sgnx_def by auto
qed
lemma sgnx_able_divide[sgnx_intros]:
assumes "f sgnx_able F" "g sgnx_able F"
shows "(λx. f x / g x) sgnx_able F"
using has_sgnx_divide by (meson assms(1) assms(2) sgnx_able_def)
lemma sgnx_divide:
assumes "F≠bot" "f sgnx_able F" "g sgnx_able F"
shows "sgnx (λx. f x / g x) F =sgnx f F / sgnx g F"
proof -
obtain c1 c2 where c1:"(f has_sgnx c1) F" and c2:"(g has_sgnx c2) F"
using assms unfolding sgnx_able_def by auto
have "sgnx f F=c1" "sgnx g F=c2" using c1 c2 ‹F≠bot› by auto
moreover have "((λx. f x / g x) has_sgnx c1 / c2) F"
using has_sgnx_divide[OF c1 c2] .
ultimately show ?thesis using assms(1) has_sgnx_imp_sgnx by blast
qed
lemma has_sgnx_times[sgnx_intros]:
assumes "(f has_sgnx c1) F" "(g has_sgnx c2) F"
shows "((λx. f x* g x) has_sgnx c1 * c2) F"
proof -
have "∀⇩F x in F. sgn (f x) = c1 ∧ sgn (g x) = c2"
using assms unfolding has_sgnx_def by (intro eventually_conj,auto)
then have "∀⇩F x in F. sgn (f x * g x) = c1 * c2"
apply (elim eventually_mono)
by (simp add: sgn_mult)
then show "((λx. f x* g x) has_sgnx c1 * c2) F" unfolding has_sgnx_def by auto
qed
lemma sgnx_able_times[sgnx_intros]:
assumes "f sgnx_able F" "g sgnx_able F"
shows "(λx. f x * g x) sgnx_able F"
using has_sgnx_times by (meson assms(1) assms(2) sgnx_able_def)
lemma sgnx_times:
assumes "F≠bot" "f sgnx_able F" "g sgnx_able F"
shows "sgnx (λx. f x * g x) F =sgnx f F * sgnx g F"
proof -
obtain c1 c2 where c1:"(f has_sgnx c1) F" and c2:"(g has_sgnx c2) F"
using assms unfolding sgnx_able_def by auto
have "sgnx f F=c1" "sgnx g F=c2" using c1 c2 ‹F≠bot› by auto
moreover have "((λx. f x* g x) has_sgnx c1 * c2) F"
using has_sgnx_times[OF c1 c2] .
ultimately show ?thesis using assms(1) has_sgnx_imp_sgnx by blast
qed
lemma tendsto_nonzero_has_sgnx:
assumes "(f ⤏ c) F" "c≠0"
shows "(f has_sgnx sgn c) F"
proof (cases rule:linorder_cases[of c 0])
case less
then have "∀⇩F x in F. f x<0"
using order_topology_class.order_tendstoD[OF assms(1),of 0] by auto
then show ?thesis
unfolding has_sgnx_def
apply (elim eventually_mono)
using less by auto
next
case equal
then show ?thesis using ‹c≠0› by auto
next
case greater
then have "∀⇩F x in F. f x>0"
using order_topology_class.order_tendstoD[OF assms(1),of 0] by auto
then show ?thesis
unfolding has_sgnx_def
apply (elim eventually_mono)
using greater by auto
qed
lemma tendsto_nonzero_sgnx:
assumes "(f ⤏ c) F" "F≠bot" "c≠0"
shows "sgnx f F = sgn c"
using tendsto_nonzero_has_sgnx
by (simp add: assms has_sgnx_imp_sgnx)
lemma filterlim_divide_at_bot_at_top_iff:
assumes "(f ⤏ c) F" "c≠0"
shows
"(LIM x F. f x / g x :> at_bot) ⟷ (g ⤏ 0) F
∧ ((λx. g x) has_sgnx - sgn c) F"
"(LIM x F. f x / g x :> at_top) ⟷ (g ⤏ 0) F
∧ ((λx. g x) has_sgnx sgn c) F"
proof -
show "(LIM x F. f x / g x :> at_bot) ⟷ ((g ⤏ 0) F )
∧ ((λx. g x) has_sgnx - sgn c) F"
proof
assume asm:"LIM x F. f x / g x :> at_bot"
then have "filterlim g (at 0) F"
using filterlim_at_infinity_divide_iff[OF assms(1,2),of g]
at_bot_le_at_infinity filterlim_mono by blast
then have "(g ⤏ 0) F" using filterlim_at by blast
moreover have "(g has_sgnx - sgn c) F"
proof -
have "((λx. sgn c * inverse (f x)) ⤏ sgn c * inverse c) F"
using assms(1,2) by (auto intro:tendsto_intros)
then have "LIM x F. sgn c * inverse (f x) * (f x / g x) :> at_bot"
apply (elim filterlim_tendsto_pos_mult_at_bot[OF _ _ asm])
using ‹c≠0› sgn_real_def by auto
then have "LIM x F. sgn c / g x :> at_bot"
apply (elim filterlim_mono_eventually)
using eventually_times_inverse_1[OF assms] by (auto elim:eventually_mono)
then have "∀⇩F x in F. sgn c / g x < 0"
using filterlim_at_bot_dense[of "λx. sgn c/g x" F] by auto
then show ?thesis unfolding has_sgnx_def
apply (elim eventually_mono)
by (metis add.inverse_inverse divide_less_0_iff sgn_neg sgn_pos sgn_sgn)
qed
ultimately show "(g ⤏ 0) F ∧ (g has_sgnx - sgn c) F" by auto
next
assume "(g ⤏ 0) F ∧ (g has_sgnx - sgn c) F"
then have asm:"(g ⤏ 0) F" "(g has_sgnx - sgn c) F" by auto
have "LIM x F. inverse (g x * sgn c) :> at_bot"
proof (rule filterlim_inverse_at_bot)
show "((λx. g x * sgn c) ⤏ 0) F"
apply (rule tendsto_mult_left_zero)
using asm(1) by blast
next
show "∀⇩F x in F. g x * sgn c < 0" using asm(2) unfolding has_sgnx_def
apply (elim eventually_mono)
by (metis add.inverse_inverse assms(2) linorder_neqE_linordered_idom mult_less_0_iff
neg_0_less_iff_less sgn_greater sgn_zero_iff)
qed
moreover have "((λx. f x * sgn c) ⤏ c * sgn c) F"
using ‹(f ⤏ c) F› ‹c≠0›
apply (intro tendsto_intros)
by (auto simp add:sgn_zero_iff)
moreover have "c * sgn c >0" using ‹c≠0› by (simp add: sgn_real_def)
ultimately have "LIM x F. (f x * sgn c) *inverse (g x * sgn c) :> at_bot"
using filterlim_tendsto_pos_mult_at_bot by blast
then show "LIM x F. f x / g x :> at_bot"
using ‹c≠0› by (auto simp add:field_simps sgn_zero_iff)
qed
show "(LIM x F. f x / g x :> at_top) ⟷ ((g ⤏ 0) F )
∧ ((λx. g x) has_sgnx sgn c) F"
proof
assume asm:"LIM x F. f x / g x :> at_top"
then have "filterlim g (at 0) F"
using filterlim_at_infinity_divide_iff[OF assms(1,2),of g]
at_top_le_at_infinity filterlim_mono by blast
then have "(g ⤏ 0) F" using filterlim_at by blast
moreover have "(g has_sgnx sgn c) F"
proof -
have "((λx. sgn c * inverse (f x)) ⤏ sgn c * inverse c) F"
using assms(1,2) by (auto intro:tendsto_intros)
then have "LIM x F. sgn c * inverse (f x) * (f x / g x) :> at_top"
apply (elim filterlim_tendsto_pos_mult_at_top[OF _ _ asm])
using ‹c≠0› sgn_real_def by auto
then have "LIM x F. sgn c / g x :> at_top"
apply (elim filterlim_mono_eventually)
using eventually_times_inverse_1[OF assms] by (auto elim:eventually_mono)
then have "∀⇩F x in F. sgn c / g x > 0"
using filterlim_at_top_dense[of "λx. sgn c/g x" F] by auto
then show ?thesis unfolding has_sgnx_def
apply (elim eventually_mono)
by (metis sgn_greater sgn_less sgn_neg sgn_pos zero_less_divide_iff)
qed
ultimately show "(g ⤏ 0) F ∧ (g has_sgnx sgn c) F" by auto
next
assume "(g ⤏ 0) F ∧ (g has_sgnx sgn c) F"
then have asm:"(g ⤏ 0) F" "(g has_sgnx sgn c) F" by auto
have "LIM x F. inverse (g x * sgn c) :> at_top"
proof (rule filterlim_inverse_at_top)
show "((λx. g x * sgn c) ⤏ 0) F"
apply (rule tendsto_mult_left_zero)
using asm(1) by blast
next
show "∀⇩F x in F. g x * sgn c > 0" using asm(2) unfolding has_sgnx_def
apply (elim eventually_mono)
by (metis assms(2) sgn_1_neg sgn_greater sgn_if zero_less_mult_iff)
qed
moreover have "((λx. f x * sgn c) ⤏ c * sgn c) F"
using ‹(f ⤏ c) F› ‹c≠0›
apply (intro tendsto_intros)
by (auto simp add:sgn_zero_iff)
moreover have "c * sgn c >0" using ‹c≠0› by (simp add: sgn_real_def)
ultimately have "LIM x F. (f x * sgn c) *inverse (g x * sgn c) :> at_top"
using filterlim_tendsto_pos_mult_at_top by blast
then show "LIM x F. f x / g x :> at_top"
using ‹c≠0› by (auto simp add:field_simps sgn_zero_iff)
qed
qed
lemma poly_sgnx_left_right:
fixes c a::real and p::"real poly"
assumes "p≠0"
shows "sgnx (poly p) (at_left a) = (if even (order a p)
then sgnx (poly p) (at_right a)
else -sgnx (poly p) (at_right a))"
using assms
proof (induction "degree p" arbitrary: p rule: less_induct)
case less
have ?case when "poly p a≠0"
proof -
have "sgnx (poly p) (at_left a) = sgn (poly p a)"
by (simp add: has_sgnx_imp_sgnx tendsto_nonzero_has_sgnx that)
moreover have "sgnx (poly p) (at_right a) = sgn (poly p a)"
by (simp add: has_sgnx_imp_sgnx tendsto_nonzero_has_sgnx that)
moreover have "order a p = 0" using that by (simp add: order_0I)
ultimately show ?thesis by auto
qed
moreover have ?case when "poly p a=0"
proof -
obtain q where pq:"p= [:-a,1:] * q"
using ‹poly p a=0› by (meson dvdE poly_eq_0_iff_dvd)
then have "q≠0" using ‹p≠0› by auto
then have "degree q < degree p" unfolding pq by (subst degree_mult_eq,auto)
have "sgnx (poly p) (at_left a) = - sgnx (poly q) (at_left a)"
proof -
have "sgnx (λx. poly p x) (at_left a)
= sgnx (poly q) (at_left a) * sgnx (poly [:-a,1:]) (at_left a)"
unfolding pq
apply (subst poly_mult)
apply (subst sgnx_times)
by auto
moreover have "sgnx (λx. poly [:-a,1:] x) (at_left a) = -1"
apply (intro has_sgnx_imp_sgnx)
unfolding has_sgnx_def eventually_at_left
by (auto simp add: linordered_field_no_lb)
ultimately show ?thesis by auto
qed
moreover have "sgnx (poly p) (at_right a) = sgnx (poly q) (at_right a)"
proof -
have "sgnx (λx. poly p x) (at_right a)
= sgnx (poly q) (at_right a) * sgnx (poly [:-a,1:]) (at_right a)"
unfolding pq
apply (subst poly_mult)
apply (subst sgnx_times)
by auto
moreover have "sgnx (λx. poly [:-a,1:] x) (at_right a) = 1"
apply (intro has_sgnx_imp_sgnx)
unfolding has_sgnx_def eventually_at_right
by (auto simp add: linordered_field_no_ub)
ultimately show ?thesis by auto
qed
moreover have "even (order a p) ⟷ odd (order a q)"
unfolding pq
apply (subst order_mult[OF ‹p ≠ 0›[unfolded pq]])
using ‹q≠0› by (auto simp add:order_power_n_n[of _ 1, simplified])
moreover note less.hyps[OF ‹degree q < degree p› ‹q≠0›]
ultimately show ?thesis by auto
qed
ultimately show ?case by blast
qed
lemma poly_has_sgnx_left_right:
fixes c a::real and p::"real poly"
assumes "p≠0"
shows "(poly p has_sgnx c) (at_left a) ⟷ (if even (order a p)
then (poly p has_sgnx c) (at_right a)
else (poly p has_sgnx -c) (at_right a))"
using poly_sgnx_left_right
by (metis (no_types, opaque_lifting) add.inverse_inverse assms has_sgnx_unique
sgnx_able_poly sgnx_able_sgnx trivial_limit_at_left_real trivial_limit_at_right_real)
lemma sign_r_pos_sgnx_iff:
"sign_r_pos p a ⟷ sgnx (poly p) (at_right a) > 0"
proof
assume asm:"0 < sgnx (poly p) (at_right a)"
obtain c where c_def:"(poly p has_sgnx c) (at_right a)"
using sgnx_able_poly(1) sgnx_able_sgnx by blast
then have "c>0" using asm
using has_sgnx_imp_sgnx trivial_limit_at_right_real by blast
then show "sign_r_pos p a" using c_def unfolding sign_r_pos_def has_sgnx_def
apply (elim eventually_mono)
by force
next
assume asm:"sign_r_pos p a"
define c where "c = sgnx (poly p) (at_right a)"
then have "(poly p has_sgnx c) (at_right a)"
by (simp add: sgnx_able_sgnx)
then have "(∀⇩F x in (at_right a). poly p x>0 ∧ sgn (poly p x) = c)"
using asm unfolding has_sgnx_def sign_r_pos_def
by (simp add:eventually_conj_iff)
then have "∀⇩F x in (at_right a). c > 0"
apply (elim eventually_mono)
by fastforce
then show "c>0" by auto
qed
lemma sgnx_values:
assumes "f sgnx_able F" "F ≠ bot"
shows "sgnx f F = -1 ∨ sgnx f F = 0 ∨ sgnx f F = 1"
proof -
obtain c where c_def:"(f has_sgnx c) F"
using assms(1) unfolding sgnx_able_def by auto
then obtain x where "sgn(f x) = c"
unfolding has_sgnx_def using assms(2) eventually_happens
by blast
then have "c=-1 ∨ c=0 ∨ c=1" using sgn_if by metis
moreover have "sgnx f F = c" using c_def by (simp add: assms(2) has_sgnx_imp_sgnx)
ultimately show ?thesis by auto
qed
lemma has_sgnx_poly_at_top:
"(poly p has_sgnx sgn_pos_inf p) at_top"
using has_sgnx_def poly_sgn_eventually_at_top by blast
lemma has_sgnx_poly_at_bot:
"(poly p has_sgnx sgn_neg_inf p) at_bot"
using has_sgnx_def poly_sgn_eventually_at_bot by blast
lemma sgnx_poly_at_top:
"sgnx (poly p) at_top = sgn_pos_inf p"
by (simp add: has_sgnx_def has_sgnx_imp_sgnx poly_sgn_eventually_at_top)
lemma sgnx_poly_at_bot:
"sgnx (poly p) at_bot = sgn_neg_inf p"
by (simp add: has_sgnx_def has_sgnx_imp_sgnx poly_sgn_eventually_at_bot)
lemma poly_has_sgnx_values:
assumes "p≠0"
shows
"(poly p has_sgnx 1) (at_left a) ∨ (poly p has_sgnx - 1) (at_left a)"
"(poly p has_sgnx 1) (at_right a) ∨ (poly p has_sgnx - 1) (at_right a)"
"(poly p has_sgnx 1) at_top ∨ (poly p has_sgnx - 1) at_top"
"(poly p has_sgnx 1) at_bot ∨ (poly p has_sgnx - 1) at_bot"
proof -
have "sgn_pos_inf p = 1 ∨ sgn_pos_inf p = -1"
unfolding sgn_pos_inf_def by (simp add: assms sgn_if)
then show "(poly p has_sgnx 1) at_top ∨ (poly p has_sgnx - 1) at_top"
using has_sgnx_poly_at_top by metis
next
have "sgn_neg_inf p = 1 ∨ sgn_neg_inf p = -1"
unfolding sgn_neg_inf_def by (simp add: assms sgn_if)
then show "(poly p has_sgnx 1) at_bot ∨ (poly p has_sgnx - 1) at_bot"
using has_sgnx_poly_at_bot by metis
next
obtain c where c_def:"(poly p has_sgnx c) (at_left a)"
using sgnx_able_poly(2) sgnx_able_sgnx by blast
then have "sgnx (poly p) (at_left a) = c" using assms by auto
then have "c=-1 ∨ c=0 ∨ c=1"
using sgnx_values sgnx_able_poly(2) trivial_limit_at_left_real by blast
moreover have False when "c=0"
proof -
have "(poly p has_sgnx 0) (at_left a)" using c_def that by auto
then obtain lb where "lb<a" "∀y. (lb<y ∧ y < a) ⟶ poly p y = 0"
unfolding has_sgnx_def eventually_at_left sgn_if
by (metis one_neq_zero zero_neq_neg_one)
then have "{lb<..<a} ⊆ proots p" unfolding proots_within_def by auto
then have "infinite (proots p)"
apply (elim infinite_super)
using ‹lb<a› by auto
moreover have "finite (proots p)" using finite_proots[OF ‹p≠0›] by auto
ultimately show False by auto
qed
ultimately have "c=-1 ∨ c=1" by auto
then show "(poly p has_sgnx 1) (at_left a) ∨ (poly p has_sgnx - 1) (at_left a)"
using c_def by auto
next
obtain c where c_def:"(poly p has_sgnx c) (at_right a)"
using sgnx_able_poly(1) sgnx_able_sgnx by blast
then have "sgnx (poly p) (at_right a) = c" using assms by auto
then have "c=-1 ∨ c=0 ∨ c=1"
using sgnx_values sgnx_able_poly(1) trivial_limit_at_right_real by blast
moreover have False when "c=0"
proof -
have "(poly p has_sgnx 0) (at_right a)" using c_def that by auto
then obtain ub where "ub>a" "∀y. (a<y ∧ y < ub) ⟶ poly p y = 0"
unfolding has_sgnx_def eventually_at_right sgn_if
by (metis one_neq_zero zero_neq_neg_one)
then have "{a<..<ub} ⊆ proots p" unfolding proots_within_def by auto
then have "infinite (proots p)"
apply (elim infinite_super)
using ‹ub>a› by auto
moreover have "finite (proots p)" using finite_proots[OF ‹p≠0›] by auto
ultimately show False by auto
qed
ultimately have "c=-1 ∨ c=1" by auto
then show "(poly p has_sgnx 1) (at_right a) ∨ (poly p has_sgnx - 1) (at_right a)"
using c_def by auto
qed
lemma poly_sgnx_values:
assumes "p≠0"
shows "sgnx (poly p) (at_left a) = 1 ∨ sgnx (poly p) (at_left a) = -1"
"sgnx (poly p) (at_right a) = 1 ∨ sgnx (poly p) (at_right a) = -1"
using poly_has_sgnx_values[OF ‹p≠0›] has_sgnx_imp_sgnx trivial_limit_at_left_real
trivial_limit_at_right_real by blast+
lemma has_sgnx_inverse: "(f has_sgnx c) F ⟷ ((inverse o f) has_sgnx (inverse c)) F"
unfolding has_sgnx_def comp_def
apply (rule eventually_subst)
apply (rule always_eventually)
by (metis inverse_inverse_eq sgn_inverse)
lemma has_sgnx_derivative_at_left:
assumes g_deriv:"(g has_field_derivative c) (at x)" and "g x=0" and "c≠0"
shows "(g has_sgnx - sgn c) (at_left x)"
proof -
have "(g has_sgnx -1) (at_left x)" when "c>0"
proof -
obtain d1 where "d1>0" and d1_def:"∀h>0. h < d1 ⟶ g (x - h) < g x"
using DERIV_pos_inc_left[OF g_deriv ‹c>0›] ‹g x=0› by auto
have "(g has_sgnx -1) (at_left x)"
unfolding has_sgnx_def eventually_at_left
apply (intro exI[where x="x-d1"])
using ‹d1>0› d1_def
by (metis (no_types, opaque_lifting) add.commute add_uminus_conv_diff assms(2) diff_add_cancel
diff_strict_left_mono diff_zero minus_diff_eq sgn_neg)
thus ?thesis by auto
qed
moreover have "(g has_sgnx 1) (at_left x)" when "c<0"
proof -
obtain d1 where "d1>0" and d1_def:"∀h>0. h < d1 ⟶ g (x - h) > g x"
using DERIV_neg_dec_left[OF g_deriv ‹c<0›] ‹g x=0› by auto
have "(g has_sgnx 1) (at_left x)"
unfolding has_sgnx_def eventually_at_left
apply (intro exI[where x="x-d1"])
using ‹d1>0› d1_def
by (metis (no_types, opaque_lifting) add.commute add_uminus_conv_diff assms(2) diff_add_cancel
diff_zero less_diff_eq minus_diff_eq sgn_pos)
thus ?thesis using ‹c<0› by auto
qed
ultimately show ?thesis using ‹c≠0› using sgn_real_def by auto
qed
lemma has_sgnx_derivative_at_right:
assumes g_deriv:"(g has_field_derivative c) (at x)" and "g x=0" and "c≠0"
shows "(g has_sgnx sgn c) (at_right x)"
proof -
have "(g has_sgnx 1) (at_right x)" when "c>0"
proof -
obtain d2 where "d2>0" and d2_def:"∀h>0. h < d2 ⟶ g x < g (x + h)"
using DERIV_pos_inc_right[OF g_deriv ‹c>0›] ‹g x=0› by auto
have "(g has_sgnx 1) (at_right x)"
unfolding has_sgnx_def eventually_at_right
apply (intro exI[where x="x+d2"])
using ‹d2>0› d2_def
by (metis add.commute assms(2) diff_add_cancel diff_less_eq less_add_same_cancel1 sgn_pos)
thus ?thesis using ‹c>0› by auto
qed
moreover have "(g has_sgnx -1) (at_right x)" when "c<0"
proof -
obtain d2 where "d2>0" and d2_def:"∀h>0. h < d2 ⟶ g x > g (x + h)"
using DERIV_neg_dec_right[OF g_deriv ‹c<0›] ‹g x=0› by auto
have "(g has_sgnx -1) (at_right x)"
unfolding has_sgnx_def eventually_at_right
apply (intro exI[where x="x+d2"])
using ‹d2>0› d2_def
by (metis (no_types, opaque_lifting) add.commute add.right_inverse add_uminus_conv_diff assms(2)
diff_add_cancel diff_less_eq sgn_neg)
thus ?thesis using ‹c<0› by auto
qed
ultimately show ?thesis using ‹c≠0› using sgn_real_def by auto
qed
lemma has_sgnx_split:
"(f has_sgnx c) (at x) ⟷ (f has_sgnx c) (at_left x) ∧ (f has_sgnx c) (at_right x)"
unfolding has_sgnx_def using eventually_at_split by auto
lemma sgnx_at_top_IVT:
assumes "sgnx (poly p) (at_right a) ≠ sgnx (poly p) at_top"
shows "∃x>a. poly p x=0"
proof (cases "p=0")
case True
then show ?thesis using gt_ex[of a] by simp
next
case False
from poly_has_sgnx_values[OF this]
have "(poly p has_sgnx 1) (at_right a) ∨ (poly p has_sgnx - 1) (at_right a)"
"(poly p has_sgnx 1) at_top ∨ (poly p has_sgnx - 1) at_top"
by auto
moreover have ?thesis when has_r:"(poly p has_sgnx 1) (at_right a)"
and has_top:"(poly p has_sgnx -1) at_top"
proof -
obtain b where "b>a" "poly p b>0"
proof -
obtain a' where "a'>a" and a'_def:"∀y>a. y < a' ⟶ sgn (poly p y) = 1"
using has_r[unfolded has_sgnx_def eventually_at_right] by auto
define b where "b=(a+a')/2"
have "a<b" "b<a'" unfolding b_def using ‹a'>a› by auto
moreover have "poly p b>0"
using a'_def[rule_format,OF ‹b>a› ‹b<a'›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
moreover obtain c where "c>b" "poly p c<0"
proof -
obtain b' where b'_def:"∀n≥b'. sgn (poly p n) = - 1"
using has_top[unfolded has_sgnx_def eventually_at_top_linorder] by auto
define c where "c=1+max b b'"
have "c>b" "c≥b'" unfolding c_def using ‹b>a› by auto
moreover have "poly p c<0"
using b'_def[rule_format,OF ‹b'≤c›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
ultimately show ?thesis using poly_IVT_neg[of b c p] not_less by fastforce
qed
moreover have ?thesis when has_r:"(poly p has_sgnx -1) (at_right a)"
and has_top:"(poly p has_sgnx 1) at_top"
proof -
obtain b where "b>a" "poly p b<0"
proof -
obtain a' where "a'>a" and a'_def:"∀y>a. y < a' ⟶ sgn (poly p y) = -1"
using has_r[unfolded has_sgnx_def eventually_at_right] by auto
define b where "b=(a+a')/2"
have "a<b" "b<a'" unfolding b_def using ‹a'>a› by auto
moreover have "poly p b<0"
using a'_def[rule_format,OF ‹b>a› ‹b<a'›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
moreover obtain c where "c>b" "poly p c>0"
proof -
obtain b' where b'_def:"∀n≥b'. sgn (poly p n) = 1"
using has_top[unfolded has_sgnx_def eventually_at_top_linorder] by auto
define c where "c=1+max b b'"
have "c>b" "c≥b'" unfolding c_def using ‹b>a› by auto
moreover have "poly p c>0"
using b'_def[rule_format,OF ‹b'≤c›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
ultimately show ?thesis using poly_IVT_pos[of b c p] not_less by fastforce
qed
moreover have ?thesis when
"(poly p has_sgnx 1) (at_right a) ∧ (poly p has_sgnx 1) at_top
∨ (poly p has_sgnx - 1) (at_right a) ∧ (poly p has_sgnx -1) at_top"
proof -
have "sgnx (poly p) (at_right a) = sgnx (poly p) at_top"
using that has_sgnx_imp_sgnx by auto
then have False using assms by simp
then show ?thesis by auto
qed
ultimately show ?thesis by blast
qed
lemma sgnx_at_left_at_right_IVT:
assumes "sgnx (poly p) (at_right a) ≠ sgnx (poly p) (at_left b)" "a<b"
shows "∃x. a<x ∧ x<b ∧ poly p x=0"
proof (cases "p=0")
case True
then show ?thesis using ‹a<b› by (auto intro:exI[where x="(a+b)/2"])
next
case False
from poly_has_sgnx_values[OF this]
have "(poly p has_sgnx 1) (at_right a) ∨ (poly p has_sgnx - 1) (at_right a)"
"(poly p has_sgnx 1) (at_left b) ∨ (poly p has_sgnx - 1) (at_left b)"
by auto
moreover have ?thesis when has_r:"(poly p has_sgnx 1) (at_right a)"
and has_l:"(poly p has_sgnx -1) (at_left b)"
proof -
obtain c where "a<c" "c<b" "poly p c>0"
proof -
obtain a' where "a'>a" and a'_def:"∀y>a. y < a' ⟶ sgn (poly p y) = 1"
using has_r[unfolded has_sgnx_def eventually_at_right] by auto
define c where "c=(a+min a' b)/2"
have "a<c" "c<a'" "c<b" unfolding c_def using ‹a'>a› ‹b>a› by auto
moreover have "poly p c>0"
using a'_def[rule_format,OF ‹c>a› ‹c<a'›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
moreover obtain d where "c<d""d<b" "poly p d<0"
proof -
obtain b' where "b'<b" and b'_def:"∀y>b'. y < b ⟶ sgn (poly p y) = - 1"
using has_l[unfolded has_sgnx_def eventually_at_left] by auto
define d where "d=(b+max b' c)/2"
have "b'<d" "d<b" "d>c"
unfolding d_def using ‹b>b'› ‹b>c› by auto
moreover have "poly p d<0"
using b'_def[rule_format, OF ‹b'<d› ‹d<b›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
ultimately obtain x where "c<x" "x<d" "poly p x=0"
using poly_IVT_neg[of c d p] by auto
then show ?thesis using ‹c>a› ‹d<b› by (auto intro: exI[where x=x])
qed
moreover have ?thesis when has_r:"(poly p has_sgnx -1) (at_right a)"
and has_l:"(poly p has_sgnx 1) (at_left b)"
proof -
obtain c where "a<c" "c<b" "poly p c<0"
proof -
obtain a' where "a'>a" and a'_def:"∀y>a. y < a' ⟶ sgn (poly p y) = -1"
using has_r[unfolded has_sgnx_def eventually_at_right] by auto
define c where "c=(a+min a' b)/2"
have "a<c" "c<a'" "c<b" unfolding c_def using ‹a'>a› ‹b>a› by auto
moreover have "poly p c<0"
using a'_def[rule_format,OF ‹c>a› ‹c<a'›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
moreover obtain d where "c<d""d<b" "poly p d>0"
proof -
obtain b' where "b'<b" and b'_def:"∀y>b'. y < b ⟶ sgn (poly p y) = 1"
using has_l[unfolded has_sgnx_def eventually_at_left] by auto
define d where "d=(b+max b' c)/2"
have "b'<d" "d<b" "d>c"
unfolding d_def using ‹b>b'› ‹b>c› by auto
moreover have "poly p d>0"
using b'_def[rule_format, OF ‹b'<d› ‹d<b›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
ultimately obtain x where "c<x" "x<d" "poly p x=0"
using poly_IVT_pos[of c d p] by auto
then show ?thesis using ‹c>a› ‹d<b› by (auto intro: exI[where x=x])
qed
moreover have ?thesis when
"(poly p has_sgnx 1) (at_right a) ∧ (poly p has_sgnx 1) (at_left b)
∨ (poly p has_sgnx - 1) (at_right a) ∧ (poly p has_sgnx -1) (at_left b)"
proof -
have "sgnx (poly p) (at_right a) = sgnx (poly p) (at_left b)"
using that has_sgnx_imp_sgnx by auto
then have False using assms by simp
then show ?thesis by auto
qed
ultimately show ?thesis by blast
qed
lemma sgnx_at_bot_IVT:
assumes "sgnx (poly p) (at_left a) ≠ sgnx (poly p) at_bot"
shows "∃x<a. poly p x=0"
proof (cases "p=0")
case True
then show ?thesis using lt_ex[of a] by simp
next
case False
from poly_has_sgnx_values[OF this]
have "(poly p has_sgnx 1) (at_left a) ∨ (poly p has_sgnx - 1) (at_left a)"
"(poly p has_sgnx 1) at_bot ∨ (poly p has_sgnx - 1) at_bot"
by auto
moreover have ?thesis when has_l:"(poly p has_sgnx 1) (at_left a)"
and has_bot:"(poly p has_sgnx -1) at_bot"
proof -
obtain b where "b<a" "poly p b>0"
proof -
obtain a' where "a'<a" and a'_def:"∀y>a'. y < a ⟶ sgn (poly p y) = 1"
using has_l[unfolded has_sgnx_def eventually_at_left] by auto
define b where "b=(a+a')/2"
have "a>b" "b>a'" unfolding b_def using ‹a'<a› by auto
moreover have "poly p b>0"
using a'_def[rule_format,OF ‹b>a'› ‹b<a›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
moreover obtain c where "c<b" "poly p c<0"
proof -
obtain b' where b'_def:"∀n≤b'. sgn (poly p n) = - 1"
using has_bot[unfolded has_sgnx_def eventually_at_bot_linorder] by auto
define c where "c=min b b'- 1"
have "c<b" "c≤b'" unfolding c_def using ‹b<a› by auto
moreover have "poly p c<0"
using b'_def[rule_format,OF ‹b'≥c›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
ultimately show ?thesis using poly_IVT_pos[of c b p] using not_less by fastforce
qed
moreover have ?thesis when has_l:"(poly p has_sgnx -1) (at_left a)"
and has_bot:"(poly p has_sgnx 1) at_bot"
proof -
obtain b where "b<a" "poly p b<0"
proof -
obtain a' where "a'<a" and a'_def:"∀y>a'. y < a ⟶ sgn (poly p y) = -1"
using has_l[unfolded has_sgnx_def eventually_at_left] by auto
define b where "b=(a+a')/2"
have "a>b" "b>a'" unfolding b_def using ‹a'<a› by auto
moreover have "poly p b<0"
using a'_def[rule_format,OF ‹b>a'› ‹b<a›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
moreover obtain c where "c<b" "poly p c>0"
proof -
obtain b' where b'_def:"∀n≤b'. sgn (poly p n) = 1"
using has_bot[unfolded has_sgnx_def eventually_at_bot_linorder] by auto
define c where "c=min b b'- 1"
have "c<b" "c≤b'" unfolding c_def using ‹b<a› by auto
moreover have "poly p c>0"
using b'_def[rule_format,OF ‹b'≥c›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
ultimately show ?thesis using poly_IVT_neg[of c b p] using not_less by fastforce
qed
moreover have ?thesis when
"(poly p has_sgnx 1) (at_left a) ∧ (poly p has_sgnx 1) at_bot
∨ (poly p has_sgnx - 1) (at_left a) ∧ (poly p has_sgnx -1) at_bot"
proof -
have "sgnx (poly p) (at_left a) = sgnx (poly p) at_bot"
using that has_sgnx_imp_sgnx by auto
then have False using assms by simp
then show ?thesis by auto
qed
ultimately show ?thesis by blast
qed
lemma sgnx_poly_nz:
assumes "poly p x≠0"
shows "sgnx (poly p) (at_left x) = sgn (poly p x)"
"sgnx (poly p) (at_right x) = sgn (poly p x)"
proof -
have "(poly p has_sgnx sgn(poly p x)) (at x)"
apply (rule tendsto_nonzero_has_sgnx)
using assms by auto
then show "sgnx (poly p) (at_left x) = sgn (poly p x)"
"sgnx (poly p) (at_right x) = sgn (poly p x)"
unfolding has_sgnx_split by auto
qed
subsection ‹Finite predicate segments over an interval›
inductive finite_Psegments::"(real ⇒ bool) ⇒ real ⇒ real ⇒ bool" for P where
emptyI: "a≥b ⟹ finite_Psegments P a b"|
insertI_1: "⟦s∈{a..<b};s=a∨P s;∀t∈{s<..<b}. P t; finite_Psegments P a s⟧
⟹ finite_Psegments P a b"|
insertI_2: "⟦s∈{a..<b};s=a∨P s;(∀t∈{s<..<b}. ¬P t);finite_Psegments P a s⟧
⟹ finite_Psegments P a b"
lemma finite_Psegments_pos_linear:
assumes "finite_Psegments P (b*lb+c) (b*ub+c) " and "b>0"
shows "finite_Psegments (P o (λt. b*t+c)) lb ub"
proof -
have [simp]:"b≠0" using ‹b>0› by auto
show ?thesis
proof (rule finite_Psegments.induct[OF assms(1),
of "λlb' ub'. finite_Psegments (P o (λt. b*t+c)) ((lb'-c)/b) ((ub'-c)/b)",simplified])
fix lb ub f assume "(lb::real)≤ub"
then have "(lb - c) / b ≤ (ub - c) / b"
using ‹b>0› by (auto simp add:field_simps)
then show "finite_Psegments (f ∘ (λt. b * t + c)) ((ub - c) / b) ((lb - c) / b)"
by (rule finite_Psegments.emptyI)
next
fix s lb ub P
assume asm: "lb ≤ s ∧ s < ub"
"∀t∈{s<..<ub}. P t"
"finite_Psegments (P ∘ (λt. b * t + c)) ((lb - c) / b) ((s - c) / b)"
"s = lb ∨ P s"
show "finite_Psegments (P ∘ (λt. b * t + c)) ((lb - c) / b) ((ub - c) / b)"
apply (rule finite_Psegments.insertI_1[of "(s-c)/b"])
using asm ‹b>0› by (auto simp add:field_simps)
next
fix s lb ub P
assume asm: "lb ≤ s ∧ s < ub"
"∀t∈{s<..<ub}. ¬ P t"
"finite_Psegments (P ∘ (λt. b * t + c)) ((lb - c) / b) ((s - c) / b)"
"s=lb ∨ P s"
show "finite_Psegments (P ∘ (λt. b * t + c)) ((lb - c) / b) ((ub - c) / b)"
apply (rule finite_Psegments.insertI_2[of "(s-c)/b"])
using asm ‹b>0› by (auto simp add:field_simps)
qed
qed
lemma finite_Psegments_congE:
assumes "finite_Psegments Q lb ub"
"⋀t. ⟦lb<t;t<ub⟧ ⟹ Q t ⟷ P t "
shows "finite_Psegments P lb ub" using assms
proof (induct rule:finite_Psegments.induct)
case (emptyI a b)
then show ?case using finite_Psegments.emptyI by auto
next
case (insertI_1 s a b)
show ?case
proof (rule finite_Psegments.insertI_1[of s])
have "P s" when "s≠a"
proof -
have "s∈{a<..<b}" using ‹s ∈ {a..<b}› that by auto
then show ?thesis using insertI_1 by auto
qed
then show "s = a ∨ P s" by auto
next
show "s ∈ {a..<b}" " ∀t∈{s<..<b}. P t" "finite_Psegments P a s" using insertI_1 by auto
qed
next
case (insertI_2 s a b)
show ?case
proof (rule finite_Psegments.insertI_2[of s])
have "P s" when "s≠a"
proof -
have "s∈{a<..<b}" using ‹s ∈ {a..<b}› that by auto
then show ?thesis using insertI_2 by auto
qed
then show "s = a ∨ P s" by auto
next
show "s ∈ {a..<b}" " ∀t∈{s<..<b}. ¬ P t" "finite_Psegments P a s" using insertI_2 by auto
qed
qed
lemma finite_Psegments_constI:
assumes "⋀t. ⟦a<t;t<b⟧ ⟹ P t = c"
shows "finite_Psegments P a b"
proof -
have "finite_Psegments (λ_. c) a b"
proof -
have ?thesis when "a≥b"
using that finite_Psegments.emptyI by auto
moreover have ?thesis when "a<b" "c"
apply (rule finite_Psegments.insertI_1[of a])
using that by (auto intro: finite_Psegments.emptyI)
moreover have ?thesis when "a<b" "¬c"
apply (rule finite_Psegments.insertI_2[of a])
using that by (auto intro: finite_Psegments.emptyI)
ultimately show ?thesis by argo
qed
then show ?thesis
apply (elim finite_Psegments_congE)
using assms by auto
qed
context
begin
private lemma finite_Psegments_less_eq1:
assumes "finite_Psegments P a c" "b≤c"
shows "finite_Psegments P a b" using assms
proof (induct arbitrary: b rule:finite_Psegments.induct)
case (emptyI a c)
then show ?case using finite_Psegments.emptyI by auto
next
case (insertI_1 s a c)
have ?case when "b≤s" using insertI_1 that by auto
moreover have ?case when "b>s"
proof -
have "s ∈ {a..<b}" using that ‹s ∈ {a..<c}› ‹b ≤ c› by auto
moreover have "∀t∈{s<..<b}. P t" using ‹∀t∈{s<..<c}. P t› that ‹b ≤ c› by auto
ultimately show ?case
using finite_Psegments.insertI_1[OF _ _ _ ‹finite_Psegments P a s›] ‹ s = a ∨ P s› by auto
qed
ultimately show ?case by fastforce
next
case (insertI_2 s a c)
have ?case when "b≤s" using insertI_2 that by auto
moreover have ?case when "b>s"
proof -
have "s ∈ {a..<b}" using that ‹s ∈ {a..<c}› ‹b ≤ c› by auto
moreover have "∀t∈{s<..<b}. ¬ P t" using ‹∀t∈{s<..<c}. ¬ P t› that ‹b ≤ c› by auto
ultimately show ?case
using finite_Psegments.insertI_2[OF _ _ _ ‹finite_Psegments P a s›] ‹ s = a ∨ P s› by auto
qed
ultimately show ?case by fastforce
qed
private lemma finite_Psegments_less_eq2:
assumes "finite_Psegments P a c" "a≤b"
shows "finite_Psegments P b c" using assms
proof (induct arbitrary: rule:finite_Psegments.induct)
case (emptyI a c)
then show ?case using finite_Psegments.emptyI by auto
next
case (insertI_1 s a c)
have ?case when "s≤b"
proof -
have "∀t∈{b<..<c}. P t" using insertI_1 that by auto
then show ?thesis by (simp add: finite_Psegments_constI)
qed
moreover have ?case when "s>b"
apply (rule finite_Psegments.insertI_1[where s=s])
using insertI_1 that by auto
ultimately show ?case by linarith
next
case (insertI_2 s a c)
have ?case when "s≤b"
proof -
have "∀t∈{b<..<c}. ¬ P t" using insertI_2 that by auto
then show ?thesis by (metis finite_Psegments_constI greaterThanLessThan_iff)
qed
moreover have ?case when "s>b"
apply (rule finite_Psegments.insertI_2[where s=s])
using insertI_2 that by auto
ultimately show ?case by linarith
qed
lemma finite_Psegments_included:
assumes "finite_Psegments P a d" "a≤b" "c≤d"
shows "finite_Psegments P b c"
using finite_Psegments_less_eq2 finite_Psegments_less_eq1 assms by blast
end
lemma finite_Psegments_combine:
assumes "finite_Psegments P a b" "finite_Psegments P b c" "b∈{a..c}" "closed ({x. P x} ∩ {a..c})"
shows "finite_Psegments P a c" using assms(2,1,3,4)
proof (induct rule:finite_Psegments.induct)
case (emptyI b c)
then show ?case using finite_Psegments_included by auto
next
case (insertI_1 s b c)
have "P s"
proof -
have "s<c" using insertI_1 by auto
define S where "S = {x. P x} ∩ {s..(s+c)/2}"
have "closed S"
proof -
have "closed ({a. P a} ∩ {a..c})" using insertI_1(8) .
moreover have "S = ({a. P a} ∩ {a..c}) ∩ {s..(s+c)/2}"
using insertI_1(1,7) unfolding S_def by (auto simp add:field_simps)
ultimately show ?thesis
using closed_Int[of "{a. P a} ∩ {a..c}" "{s..(s+c)/2}"] by blast
qed
moreover have "∃y∈S. dist y s < e" when "e>0" for e
proof -
define y where "y = min ((s+c)/2) (e/2+s)"
have "y∈S"
proof -
have "y∈{s..(s+c)/2}" unfolding y_def
using ‹e>0› ‹s<c› by (auto simp add:min_mult_distrib_left algebra_simps)
moreover have "P y"
apply (rule insertI_1(3)[rule_format])
unfolding y_def
using ‹e>0› ‹s<c›
by (auto simp add:algebra_simps min_mult_distrib_left min_less_iff_disj)
ultimately show ?thesis unfolding S_def by auto
qed
moreover have "dist y s <e"
unfolding y_def using ‹e>0› ‹s<c›
by (auto simp add:algebra_simps min_mult_distrib_left min_less_iff_disj dist_real_def)
ultimately show ?thesis by auto
qed
ultimately have "s∈S" using closed_approachable by auto
then show ?thesis unfolding S_def by auto
qed
show ?case
proof (rule finite_Psegments.insertI_1[of s])
show " s ∈ {a..<c}" "s = a ∨ P s" "∀t∈{s<..<c}. P t"
using insertI_1 ‹P s› by auto
next
have "closed ({a. P a} ∩ {a..s})"
using closed_Int[OF ‹closed ({a. P a} ∩ {a..c})›,of "{a..s}",simplified]
apply (elim arg_elim[of closed])
using ‹s ∈ {b..<c}› ‹b ∈ {a..c}› by auto
then show "finite_Psegments P a s" using insertI_1 by auto
qed
next
case (insertI_2 s b c)
have ?case when "P s"
proof (rule finite_Psegments.insertI_2[of s])
show "s ∈ {a..<c}" "s = a ∨ P s" "∀t∈{s<..<c}. ¬ P t" using that insertI_2 by auto
next
have "closed ({a. P a} ∩ {a..s})"
using closed_Int[OF ‹closed ({a. P a} ∩ {a..c})›,of "{a..s}",simplified]
apply (elim arg_elim[of closed])
using ‹s ∈ {b..<c}› ‹b ∈ {a..c}› by auto
then show "finite_Psegments P a s" using insertI_2 by auto
qed
moreover have ?case when "¬ P s" "s=b" using ‹finite_Psegments P a b›
proof (cases rule:finite_Psegments.cases)
case emptyI
then show ?thesis using insertI_2 that
by (metis antisym_conv atLeastAtMost_iff finite_Psegments.insertI_2)
next
case (insertI_1 s0)
have "P s"
proof -
have "s0<s" using insertI_1 atLeastLessThan_iff that(2) by blast
define S where "S = {x. P x} ∩ {(s0+s)/2..s}"
have "closed S"
using closed_Int[OF ‹closed ({a. P a} ∩ {a..c})›,of "{(s0+s)/2..s}",simplified]
apply (elim arg_elim[of closed])
unfolding S_def using ‹s0 ∈ {a..<b}› ‹ s ∈ {b..<c}› ‹b ∈ {a..c}› by auto
moreover have "∃y∈S. dist y s < e" when "e>0" for e
proof -
define y where "y = max ((s+s0)/2) (s-e/2)"
have "y∈S"
proof -
have "y∈{(s0+s)/2..s}" unfolding y_def
using ‹e>0› ‹s0<s› by (auto simp add:field_simps min_mult_distrib_left)
moreover have "P y"
apply (rule insertI_1(3)[rule_format])
unfolding y_def
using ‹e>0› ‹s0<s› ‹s=b›
by (auto simp add:field_simps max_mult_distrib_left less_max_iff_disj)
ultimately show ?thesis unfolding S_def by auto
qed
moreover have "dist y s <e"
unfolding y_def using ‹e>0› ‹s0<s›
by (auto simp add:algebra_simps max_mult_distrib_left less_max_iff_disj dist_real_def
max_add_distrib_right)
ultimately show ?thesis by auto
qed
ultimately have "s∈S" using closed_approachable by auto
then show ?thesis unfolding S_def by auto
qed
then have False using ‹¬ P s› by auto
then show ?thesis by simp
next
case (insertI_2 s0)
have *: "∀t∈{s0<..<c}. ¬ P t"
using ‹ ∀t∈{s<..<c}. ¬ P t› that ‹∀t∈{s0<..<b}. ¬ P t›
by force
show ?thesis
apply (rule finite_Psegments.insertI_2[of s0])
subgoal using insertI_2.prems(2) local.insertI_2(1) by auto
subgoal using ‹s0 = a ∨ P s0› .
subgoal using * .
subgoal using ‹finite_Psegments P a s0› .
done
qed
moreover note ‹s = b ∨ P s›
ultimately show ?case by auto
qed
subsection ‹Finite segment intersection of a path with the imaginary axis›
definition finite_ReZ_segments::"(real ⇒ complex) ⇒ complex ⇒ bool" where
"finite_ReZ_segments g z = finite_Psegments (λt. Re (g t - z) = 0) 0 1"
lemma finite_ReZ_segments_joinpaths:
assumes g1:"finite_ReZ_segments g1 z" and g2: "finite_ReZ_segments g2 z" and
"path g1" "path g2" "pathfinish g1=pathstart g2"
shows "finite_ReZ_segments (g1+++g2) z"
proof -
define P where "P = (λt. (Re ((g1 +++ g2) t - z) = 0 ∧ 0<t ∧ t<1) ∨ t=0 ∨ t=1)"
have "finite_Psegments P 0 (1/2)"
proof -
have "finite_Psegments (λt. Re (g1 t - z) = 0) 0 1"
using g1 unfolding finite_ReZ_segments_def .
then have "finite_Psegments (λt. Re (g1 (2 * t) - z) = 0) 0 (1/2)"
apply (drule_tac finite_Psegments_pos_linear[of _ 2 0 0 "1/2",simplified])
by (auto simp add:comp_def)
then show ?thesis
unfolding P_def joinpaths_def
by (elim finite_Psegments_congE,auto)
qed
moreover have "finite_Psegments P (1/2) 1"
proof -
have "finite_Psegments (λt. Re (g2 t - z) = 0) 0 1"
using g2 unfolding finite_ReZ_segments_def .
then have "finite_Psegments (λt. Re (g2 (2 * t-1) - z) = 0) (1/2) 1"
apply (drule_tac finite_Psegments_pos_linear[of _ 2 "1/2" "-1" 1,simplified])
by (auto simp add:comp_def)
then show ?thesis
unfolding P_def joinpaths_def
apply (elim finite_Psegments_congE)
by auto
qed
moreover have "closed {x. P x}"
proof -
define Q where "Q=(λt. Re ((g1 +++ g2) t - z) = 0)"
have "continuous_on {0<..<1} (g1+++g2)"
using path_join_imp[OF ‹path g1› ‹path g2› ‹pathfinish g1=pathstart g2›]
unfolding path_def by (auto elim:continuous_on_subset)
from continuous_on_Re[OF this] have "continuous_on {0<..<1} (λx. Re ((g1 +++ g2) x))" .
from continuous_on_open_Collect_neq[OF this,of "λ_. Re z",OF continuous_on_const,simplified]
have "open {t. Re ((g1 +++ g2) t - z) ≠ 0 ∧ 0<t ∧ t<1}"
by (elim arg_elim[where f="open"],auto)
from closed_Diff[of "{0::real..1}",OF _ this,simplified]
show "closed {x. P x}"
apply (elim arg_elim[where f=closed])
by (auto simp add:P_def)
qed
ultimately have "finite_Psegments P 0 1"
using finite_Psegments_combine[of _ 0 "1/2" 1] by auto
then show ?thesis
unfolding finite_ReZ_segments_def P_def
by (elim finite_Psegments_congE,auto)
qed
lemma finite_ReZ_segments_congE:
assumes "finite_ReZ_segments p1 z1"
"⋀t. ⟦0<t;t<1⟧ ⟹ Re(p1 t- z1) = Re(p2 t - z2)"
shows "finite_ReZ_segments p2 z2"
using assms unfolding finite_ReZ_segments_def
apply (elim finite_Psegments_congE)
by auto
lemma finite_ReZ_segments_constI:
assumes "∀t. 0<t∧t<1 ⟶ g t = c"
shows "finite_ReZ_segments g z"
proof -
have "finite_ReZ_segments (λ_. c) z"
unfolding finite_ReZ_segments_def
by (rule finite_Psegments_constI,auto)
then show ?thesis using assms
by (elim finite_ReZ_segments_congE,auto)
qed
lemma finite_ReZ_segment_cases [consumes 1, case_names subEq subNEq,cases pred:finite_ReZ_segments]:
assumes "finite_ReZ_segments g z"
and subEq:"(⋀s. ⟦s ∈ {0..<1};s=0∨Re (g s) = Re z;
∀t∈{s<..<1}. Re (g t) = Re z;finite_ReZ_segments (subpath 0 s g) z⟧ ⟹ P)"
and subNEq:"(⋀s. ⟦s ∈ {0..<1};s=0∨Re (g s) = Re z;
∀t∈{s<..<1}. Re (g t) ≠ Re z;finite_ReZ_segments (subpath 0 s g) z⟧ ⟹ P)"
shows "P"
using assms(1) unfolding finite_ReZ_segments_def
proof (cases rule:finite_Psegments.cases)
case emptyI
then show ?thesis by auto
next
case (insertI_1 s)
have "finite_ReZ_segments (subpath 0 s g) z"
proof (cases "s=0")
case True
show ?thesis
apply (rule finite_ReZ_segments_constI)
using True unfolding subpath_def by auto
next
case False
then have "s>0" using ‹s∈{0..<1}› by auto
from finite_Psegments_pos_linear[OF _ this,of _ 0 0 1] insertI_1(4)
show "finite_ReZ_segments (subpath 0 s g) z"
unfolding finite_ReZ_segments_def comp_def subpath_def by auto
qed
then show ?thesis using subEq insertI_1 by force
next
case (insertI_2 s)
have "finite_ReZ_segments (subpath 0 s g) z"
proof (cases "s=0")
case True
show ?thesis
apply (rule finite_ReZ_segments_constI)
using True unfolding subpath_def by auto
next
case False
then have "s>0" using ‹s∈{0..<1}› by auto
from finite_Psegments_pos_linear[OF _ this,of _ 0 0 1] insertI_2(4)
show "finite_ReZ_segments (subpath 0 s g) z"
unfolding finite_ReZ_segments_def comp_def subpath_def by auto
qed
then show ?thesis using subNEq insertI_2 by force
qed
lemma finite_ReZ_segments_induct [case_names sub0 subEq subNEq, induct pred:finite_ReZ_segments]:
assumes "finite_ReZ_segments g z"
assumes sub0:"⋀g z. (P (subpath 0 0 g) z)"
and subEq:"(⋀s g z. ⟦s ∈ {0..<1};s=0∨Re (g s) = Re z;
∀t∈{s<..<1}. Re (g t) = Re z;finite_ReZ_segments (subpath 0 s g) z;
P (subpath 0 s g) z⟧ ⟹ P g z)"
and subNEq:"(⋀s g z. ⟦s ∈ {0..<1};s=0∨Re (g s) = Re z;
∀t∈{s<..<1}. Re (g t) ≠ Re z;finite_ReZ_segments (subpath 0 s g) z;
P (subpath 0 s g) z⟧ ⟹ P g z)"
shows "P g z"
proof -
have "finite_Psegments (λt. Re (g t - z) = 0) 0 1"
using assms(1) unfolding finite_ReZ_segments_def by auto
then have "(0::real)≤1 ⟶ P (subpath 0 1 g) z"
proof (induct rule: finite_Psegments.induct[of _ 0 1 "λa b. b≥a ⟶ P (subpath a b g) z"] )
case (emptyI a b)
then show ?case using sub0[of "subpath a b g"] unfolding subpath_def by auto
next
case (insertI_1 s a b)
have ?case when "a=b"
using sub0[of "subpath a b g"] that unfolding subpath_def by auto
moreover have ?case when "a≠b"
proof -
have "b>a" using that ‹s ∈ {a..<b}› by auto
define s'::real where "s'=(s-a)/(b-a)"
have "P (subpath a b g) z"
proof (rule subEq[of s' "subpath a b g"])
show "∀t∈{s'<..<1}. Re (subpath a b g t) = Re z"
proof
fix t assume "t ∈ {s'<..<1}"
then have "(b - a) * t + a∈{s<..<b}"
unfolding s'_def using ‹b>a› ‹s ∈ {a..<b}›
apply (auto simp add:field_simps)
by (sos "((((A<0 * (A<1 * A<2)) * R<1) + (((A<=1 * (A<0 * R<1)) * (R<1 * [1]^2))
+ ((A<=0 * (A<0 * (A<1 * R<1))) * (R<1 * [1]^2)))))")
then have "Re (g ((b - a) * t + a) - z) = 0"
using insertI_1(3)[rule_format,of "(b - a) * t + a"] by auto
then show "Re (subpath a b g t) = Re z"
unfolding subpath_def by auto
qed
show "finite_ReZ_segments (subpath 0 s' (subpath a b g)) z"
proof (cases "s=a")
case True
then show ?thesis unfolding s'_def subpath_def
by (auto intro:finite_ReZ_segments_constI)
next
case False
have "finite_Psegments (λt. Re (g t - z) = 0) a s"
using insertI_1(4) unfolding finite_ReZ_segments_def by auto
then have "finite_Psegments ((λt. Re (g t - z) = 0) ∘ (λt. (s - a) * t + a)) 0 1"
apply (elim finite_Psegments_pos_linear[of _ "s-a" 0 a 1,simplified])
using False ‹s∈{a..<b}› by auto
then show ?thesis
using ‹b>a› unfolding finite_ReZ_segments_def subpath_def s'_def comp_def
by auto
qed
show "s' ∈ {0..<1}"
using ‹b>a› ‹s∈{a..<b}› unfolding s'_def
by (auto simp add:field_simps)
show "P (subpath 0 s' (subpath a b g)) z"
proof -
have "P (subpath a s g) z" using insertI_1(1,5) by auto
then show ?thesis
using ‹b>a› unfolding s'_def subpath_def by simp
qed
show "s' = 0 ∨ Re (subpath a b g s') = Re z"
proof -
have ?thesis when "s=a"
using that unfolding s'_def by auto
moreover have ?thesis when "Re (g s - z) = 0"
using that unfolding s'_def subpath_def by auto
ultimately show ?thesis using ‹s = a ∨ Re (g s - z) = 0› by auto
qed
qed
then show ?thesis using ‹b>a› by auto
qed
ultimately show ?case by auto
next
case (insertI_2 s a b)
have ?case when "a=b"
using sub0[of "subpath a b g"] that unfolding subpath_def by auto
moreover have ?case when "a≠b"
proof -
have "b>a" using that ‹s ∈ {a..<b}› by auto
define s'::real where "s'=(s-a)/(b-a)"
have "P (subpath a b g) z"
proof (rule subNEq[of s' "subpath a b g"])
show "∀t∈{s'<..<1}. Re (subpath a b g t) ≠ Re z"
proof
fix t assume "t ∈ {s'<..<1}"
then have "(b - a) * t + a∈{s<..<b}"
unfolding s'_def using ‹b>a› ‹s ∈ {a..<b}›
apply (auto simp add:field_simps)
by (sos "((((A<0 * (A<1 * A<2)) * R<1) + (((A<=1 * (A<0 * R<1)) * (R<1 * [1]^2)) +
((A<=0 * (A<0 * (A<1 * R<1))) * (R<1 * [1]^2)))))")
then have "Re (g ((b - a) * t + a) - z) ≠ 0"
using insertI_2(3)[rule_format,of "(b - a) * t + a"] by auto
then show "Re (subpath a b g t) ≠ Re z"
unfolding subpath_def by auto
qed
show "finite_ReZ_segments (subpath 0 s' (subpath a b g)) z"
proof (cases "s=a")
case True
then show ?thesis unfolding s'_def subpath_def
by (auto intro:finite_ReZ_segments_constI)
next
case False
have "finite_Psegments (λt. Re (g t - z) = 0) a s"
using insertI_2(4) unfolding finite_ReZ_segments_def by auto
then have "finite_Psegments ((λt. Re (g t - z) = 0) ∘ (λt. (s - a) * t + a)) 0 1"
apply (elim finite_Psegments_pos_linear[of _ "s-a" 0 a 1,simplified])
using False ‹s∈{a..<b}› by auto
then show ?thesis
using ‹b>a› unfolding finite_ReZ_segments_def subpath_def s'_def comp_def
by auto
qed
show "s' ∈ {0..<1}"
using ‹b>a› ‹s∈{a..<b}› unfolding s'_def
by (auto simp add:field_simps)
show "P (subpath 0 s' (subpath a b g)) z"
proof -
have "P (subpath a s g) z" using insertI_2(1,5) by auto
then show ?thesis
using ‹b>a› unfolding s'_def subpath_def by simp
qed
show "s' = 0 ∨ Re (subpath a b g s') = Re z"
proof -
have ?thesis when "s=a"
using that unfolding s'_def by auto
moreover have ?thesis when "Re (g s - z) = 0"
using that unfolding s'_def subpath_def by auto
ultimately show ?thesis using ‹s = a ∨ Re (g s - z) = 0› by auto
qed
qed
then show ?thesis using ‹b>a› by auto
qed
ultimately show ?case by auto
qed
then show ?thesis by auto
qed
lemma finite_ReZ_segments_shiftpah:
assumes "finite_ReZ_segments g z" "s∈{0..1}" "path g" and loop:"pathfinish g = pathstart g"
shows "finite_ReZ_segments (shiftpath s g) z"
proof -
have "finite_Psegments (λt. Re (shiftpath s g t - z) = 0) 0 (1-s)"
proof -
have "finite_Psegments (λt. Re (g t) = Re z) s 1"
using assms finite_Psegments_included[of _ 0 1 s] unfolding finite_ReZ_segments_def
by force
then have "finite_Psegments (λt. Re (g (s + t) - z) = 0) 0 (1-s)"
using finite_Psegments_pos_linear[of "λt. Re (g t - z) =0" 1 0 s "1-s",simplified]
unfolding comp_def by (auto simp add:algebra_simps)
then show ?thesis unfolding shiftpath_def
apply (elim finite_Psegments_congE)
using ‹s∈{0..1}› by auto
qed
moreover have "finite_Psegments (λt. Re (shiftpath s g t - z) = 0) (1-s) 1"
proof -
have "finite_Psegments (λt. Re (g t) = Re z) 0 s "
using assms finite_Psegments_included unfolding finite_ReZ_segments_def
by force
then have "finite_Psegments (λt. Re (g (s + t - 1) - z) = 0) (1-s) 1"
using finite_Psegments_pos_linear[of "λt. Re (g t - z) =0" 1 "1-s" "s-1" 1,simplified]
unfolding comp_def by (auto simp add:algebra_simps)
then show ?thesis unfolding shiftpath_def
apply (elim finite_Psegments_congE)
using ‹s∈{0..1}› by auto
qed
moreover have "1 - s ∈ {0..1}" using ‹s∈{0..1}› by auto
moreover have "closed ({x. Re (shiftpath s g x - z) = 0} ∩ {0..1})"
proof -
let ?f = "λx. Re (shiftpath s g x - z)"
have "continuous_on {0..1} ?f"
using path_shiftpath[OF ‹path g› loop ‹s∈{0..1}›] unfolding path_def
by (auto intro: continuous_intros)
from continuous_closed_preimage_constant[OF this,of 0,simplified]
show ?thesis
apply (elim arg_elim[of closed])
by force
qed
ultimately show ?thesis unfolding finite_ReZ_segments_def
by (rule finite_Psegments_combine[where b="1-s"])
qed
lemma finite_imp_finite_ReZ_segments:
assumes "finite {t. Re (g t - z) = 0 ∧ 0 ≤ t ∧ t≤1}"
shows "finite_ReZ_segments g z"
proof -
define P where "P = (λt. Re (g t - z) = 0)"
define rs where "rs=(λb. {t. P t ∧ 0 < t ∧ t<b})"
have "finite_Psegments P 0 b" when "finite (rs b)" "b>0" for b
using that
proof (induct "card (rs b)" arbitrary:b rule:nat_less_induct)
case ind:1
have ?case when "rs b= {}"
apply (rule finite_Psegments.intros(3)[of 0])
using that ‹0 < b› unfolding rs_def by (auto intro:finite_Psegments.intros)
moreover have ?case when "rs b≠{}"
proof -
define lj where "lj = Max (rs b)"
have "0<lj" "lj<b" "P lj"
using Max_in[OF ‹finite (rs b)› ‹rs b≠{}›,folded lj_def]
unfolding rs_def by auto
show ?thesis
proof (rule finite_Psegments.intros(3)[of lj])
show "lj ∈ {0..<b}" " lj = 0 ∨ P lj"
using ‹0<lj› ‹lj<b› ‹P lj› by auto
show "∀t∈{lj<..<b}. ¬ P t"
proof (rule ccontr)
assume " ¬ (∀t∈{lj<..<b}. ¬ P t) "
then obtain t where t:"P t" "lj < t" "t < b" by auto
then have "t∈rs b" unfolding rs_def using ‹lj>0› by auto
then have "t≤lj" using Max_ge[OF ‹finite (rs b)›,of t] unfolding lj_def by auto
then show False using ‹t>lj› by auto
qed
show "finite_Psegments P 0 lj"
proof (rule ind.hyps[rule_format,of "card (rs lj)" lj,simplified])
show "finite (rs lj)"
using ‹finite (rs b)› unfolding rs_def using ‹lj<b›
by (auto elim!:rev_finite_subset )
show "card (rs lj) < card (rs b)"
apply (rule psubset_card_mono[OF ‹finite (rs b)›])
using Max_in ‹finite (rs lj)› ‹lj < b› lj_def rs_def that by fastforce
show "0 < lj" using ‹0<lj› .
qed
qed
qed
ultimately show ?case by auto
qed
moreover have "finite (rs 1)"
using assms unfolding rs_def P_def
by (auto elim:rev_finite_subset)
ultimately have "finite_Psegments P 0 1" by auto
then show ?thesis unfolding P_def finite_ReZ_segments_def .
qed
lemma finite_ReZ_segments_poly_linepath:
shows "finite_ReZ_segments (poly p o linepath a b) z"
proof -
define P where "P=map_poly Re (pcompose (p-[:z:]) [:a,b-a:])"
have *:"Re ((poly p ∘ linepath a b) t - z) = 0 ⟷ poly P t=0" for t
unfolding inner_complex_def P_def linepath_def comp_def
apply (subst Re_poly_of_real[symmetric])
by (auto simp add: algebra_simps poly_pcompose scaleR_conv_of_real)
have ?thesis when "P≠0"
proof -
have "finite {t. poly P t=0}" using that poly_roots_finite by auto
then have "finite {t. Re ((poly p ∘ linepath a b) t - z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}"
using *
by auto
then show ?thesis
using finite_imp_finite_ReZ_segments[of "poly p o linepath a b" z] by auto
qed
moreover have ?thesis when "P=0"
unfolding finite_ReZ_segments_def
apply (rule finite_Psegments_constI[where c=True])
apply (subst *)
using that by auto
ultimately show ?thesis by auto
qed
lemma part_circlepath_half_finite_inter:
assumes "st≠tt" "r≠0" "c≠0"
shows "finite {t. part_circlepath z0 r st tt t ∙ c = d ∧ 0≤ t ∧ t≤1}" (is "finite ?T")
proof -
let ?S = "{θ. (z0+r*exp (𝗂 * θ )) ∙ c = d ∧ θ ∈ closed_segment st tt}"
define S where "S ≡ {θ. (z0+r*exp (𝗂 * θ )) ∙ c = d ∧ θ ∈ closed_segment st tt}"
have "S = linepath st tt ` ?T"
proof
define g where "g≡(λt. (t-st)/(tt -st))"
have "0≤g t" "g t≤1" when "t ∈ closed_segment st tt " for t
using that ‹st≠tt› closed_segment_eq_real_ivl unfolding g_def real_scaleR_def
by (auto simp add:divide_simps)
moreover have "linepath st tt (g t) =t" "g (linepath st tt t) = t" for t
unfolding linepath_def g_def real_scaleR_def using ‹st≠tt›
apply (simp_all add:divide_simps)
by (auto simp add:algebra_simps )
ultimately have "x∈linepath st tt ` ?T" when "x∈S" for x
using that unfolding S_def
by (auto intro!:image_eqI[where x="g x"] simp add:part_circlepath_def)
then show "S ⊆ linepath st tt ` ?T" by auto
next
have "x∈S" when "x∈linepath st tt ` ?T" for x
using that unfolding part_circlepath_def S_def
by (auto simp add: linepath_in_path)
then show "linepath st tt ` ?T ⊆ S" by auto
qed
moreover have "finite S"
proof -
define a' b' c' where "a'=r * Re c" and "b' = r* Im c" and "c'=Im c * Im z0 + Re z0 * Re c - d"
define f where "f θ= a' * cos θ + b' * sin θ + c'" for θ
have "(z0+r*exp (𝗂 * θ )) ∙ c = d ⟷ f θ = 0" for θ
unfolding exp_Euler inner_complex_def f_def a'_def b'_def c'_def
by (auto simp add:algebra_simps cos_of_real sin_of_real)
then have *:"S = roots f ∩ closed_segment st tt"
unfolding S_def roots_within_def by auto
have "uniform_discrete S"
proof -
have "a' ≠ 0 ∨ b' ≠ 0 ∨ c' ≠ 0"
using assms complex_eq_iff unfolding a'_def b'_def c'_def
by auto
then have "periodic_set (roots f) (4 * pi)"
using periodic_set_sin_cos_linear[of a' b' c',folded f_def] by auto
then have "uniform_discrete (roots f)" using periodic_imp_uniform_discrete by auto
then show ?thesis unfolding * by auto
qed
moreover have "bounded S" unfolding *
by (simp add: bounded_Int bounded_closed_segment)
ultimately show ?thesis using uniform_discrete_finite_iff by auto
qed
moreover have "inj_on (linepath st tt) ?T"
proof -
have "inj (linepath st tt)"
unfolding linepath_def using assms inj_segment by blast
then show ?thesis by (auto elim:subset_inj_on)
qed
ultimately show ?thesis by (auto elim!: finite_imageD)
qed
lemma linepath_half_finite_inter:
assumes "a ∙ c ≠ d ∨ b ∙ c ≠ d"
shows "finite {t. linepath a b t ∙ c = d ∧ 0≤ t ∧ t≤1}" (is "finite ?S")
proof (rule ccontr)
assume asm:"infinite ?S"
obtain t1 t2 where u1u2:"t1≠t2" "t1∈?S" "t2∈?S"
proof -
obtain t1 where "t1∈?S" using not_finite_existsD asm by blast
moreover have "∃u2. u2∈?S-{t1}"
using infinite_remove[OF asm,of t1]
by (meson finite.emptyI rev_finite_subset subsetI)
ultimately show ?thesis using that by auto
qed
have t1:"(1-t1)*(a ∙ c) + t1 * (b ∙ c) = d"
using ‹t1∈?S› unfolding linepath_def by (simp add: inner_left_distrib)
have t2:"(1-t2)*(a ∙ c) + t2 * (b ∙ c) = d"
using ‹t2∈?S› unfolding linepath_def by (simp add: inner_left_distrib)
have "a ∙ c = d"
proof -
have "t2*((1-t1)*(a ∙ c) + t1 * (b ∙ c)) = t2*d" using t1 by auto
then have *:"(t2-t1*t2)*(a ∙ c) + t1*t2 * (b ∙ c) = t2*d" by (auto simp add:algebra_simps)
have "t1*((1-t2)*(a ∙ c) + t2 * (b ∙ c)) = t1*d" using t2 by auto
then have **:"(t1-t1*t2)*(a ∙ c) + t1*t2 * (b ∙ c) = t1*d" by (auto simp add:algebra_simps)
have "(t2-t1)*(a ∙ c) = (t2-t1)*d" using arg_cong2[OF * **,of minus]
by (auto simp add:algebra_simps)
then show ?thesis using ‹t1≠t2› by auto
qed
moreover have "b ∙ c = d"
proof -
have "(1-t2)*((1-t1)*(a ∙ c) + t1 * (b ∙ c)) = (1-t2)*d" using t1 by auto
then have *:"(1-t1)*(1-t2)*(a ∙ c) + (t1-t1*t2) * (b ∙ c) = (1-t2)*d" by (auto simp add:algebra_simps)
have "(1-t1)*((1-t2)*(a ∙ c) + t2 * (b ∙ c)) = (1-t1)*d" using t2 by auto
then have **:"(1-t1)*(1-t2)*(a ∙ c) + (t2-t1*t2) * (b ∙ c) = (1-t1)*d" by (auto simp add:algebra_simps)
have "(t2-t1)*(b ∙ c) = (t2-t1)*d" using arg_cong2[OF ** *,of minus]
by (auto simp add:algebra_simps)
then show ?thesis using ‹t1≠t2› by auto
qed
ultimately show False using assms by auto
qed
lemma finite_half_joinpaths_inter:
assumes "finite {t. l1 t ∙ c = d ∧ 0≤ t ∧ t≤1}" "finite {t. l2 t ∙ c = d ∧ 0≤ t ∧ t≤1}"
shows "finite {t. (l1+++l2) t ∙ c = d ∧ 0≤ t ∧ t≤1}"
proof -
let ?l1s = "{t. l1 (2*t) ∙ c = d ∧ 0≤ t ∧ t≤1/2}"
let ?l2s = "{t. l2 (2 * t - 1) ∙ c = d ∧ 1/2< t ∧ t≤1}"
let ?ls = "λl. {t. l t ∙ c = d ∧ 0≤ t ∧ t≤1}"
have "{t. (l1+++l2) t ∙ c = d ∧ 0≤ t ∧ t≤1} = ?l1s ∪ ?l2s"
unfolding joinpaths_def by auto
moreover have "finite ?l1s"
proof -
have "?l1s = ((*) (1/2)) ` ?ls l1" by (auto intro:rev_image_eqI)
thus ?thesis using assms by simp
qed
moreover have "finite ?l2s"
proof -
have "?l2s ⊆ (λx. x/2 + 1/2) ` ?ls l2" by (auto intro:rev_image_eqI simp add:field_simps)
thus ?thesis using assms
by (auto elim:finite_subset)
qed
ultimately show ?thesis by simp
qed
lemma finite_ReZ_segments_linepath:
"finite_ReZ_segments (linepath a b) z"
proof -
have ?thesis when "Re a≠Re z ∨ Re b ≠Re z"
proof -
let ?S1="{t. Re (linepath a b t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}"
have "finite ?S1"
using linepath_half_finite_inter[of a "Complex 1 0" "Re z" b] that
using one_complex.code by auto
from finite_imp_finite_ReZ_segments[OF this] show ?thesis .
qed
moreover have ?thesis when "Re a=Re z" "Re b=Re z"
unfolding finite_ReZ_segments_def
apply (rule finite_Psegments.intros(2)[of 0])
using that unfolding linepath_def by (auto simp add:algebra_simps intro:finite_Psegments.intros)
ultimately show ?thesis by blast
qed
lemma finite_ReZ_segments_part_circlepath:
"finite_ReZ_segments (part_circlepath z0 r st tt) z"
proof -
have ?thesis when "st ≠ tt" "r ≠ 0"
proof -
let ?S1="{t. Re (part_circlepath z0 r st tt t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}"
have "finite ?S1"
using part_circlepath_half_finite_inter[of st tt r "Complex 1 0" z0 "Re z"] that one_complex.code
by (auto simp add:inner_complex_def )
from finite_imp_finite_ReZ_segments[OF this] show ?thesis .
qed
moreover have ?thesis when "st =tt ∨ r=0"
proof -
define c where "c = z0 + r * exp (𝗂 * tt)"
have "part_circlepath z0 r st tt = (λt. c)"
unfolding part_circlepath_def c_def using that linepath_refl by auto
then show ?thesis
using finite_ReZ_segments_linepath[of c c z] linepath_refl[of c]
by auto
qed
ultimately show ?thesis by blast
qed
lemma finite_ReZ_segments_poly_of_real:
shows "finite_ReZ_segments (poly p o of_real) z"
using finite_ReZ_segments_poly_linepath[of p 0 1 z] unfolding linepath_def
by (auto simp add:scaleR_conv_of_real)
lemma finite_ReZ_segments_subpath:
assumes "finite_ReZ_segments g z"
"0≤u" "u≤v" "v≤1"
shows "finite_ReZ_segments (subpath u v g) z"
proof (cases "u=v")
case True
then show ?thesis
unfolding subpath_def by (auto intro:finite_ReZ_segments_constI)
next
case False
then have "u<v" using ‹u≤v› by auto
define P where "P=(λt. Re (g t - z) = 0)"
have "finite_ReZ_segments (subpath u v g) z
= finite_Psegments (P o (λt. (v - u) * t + u)) 0 1"
unfolding finite_ReZ_segments_def subpath_def P_def comp_def by auto
also have "..."
apply (rule finite_Psegments_pos_linear)
using assms False unfolding finite_ReZ_segments_def
by (fold P_def,auto elim:finite_Psegments_included)
finally show ?thesis .
qed
subsection ‹jump and jumpF›
definition jump::"(real ⇒ real) ⇒ real ⇒ int" where
"jump f a = (if
(LIM x (at_left a). f x :> at_bot) ∧ (LIM x (at_right a). f x :> at_top)
then 1 else if
(LIM x (at_left a). f x :> at_top) ∧ (LIM x (at_right a). f x :> at_bot)
then -1 else 0)"
definition jumpF::"(real ⇒ real) ⇒ real filter ⇒ real" where
"jumpF f F ≡ (if filterlim f at_top F then 1/2 else
if filterlim f at_bot F then -1/2 else (0::real))"
lemma jumpF_const[simp]:
assumes "F≠bot"
shows "jumpF (λ_. c) F = 0"
proof -
have False when "LIM x F. c :> at_bot"
using filterlim_at_bot_nhds[OF that _ ‹F≠bot›] by auto
moreover have False when "LIM x F. c :> at_top"
using filterlim_at_top_nhds[OF that _ ‹F≠bot›] by auto
ultimately show ?thesis unfolding jumpF_def by auto
qed
lemma jumpF_not_infinity:
assumes "continuous F g" "F≠bot"
shows "jumpF g F = 0"
proof -
have "¬ filterlim g at_infinity F"
using not_tendsto_and_filterlim_at_infinity[OF ‹F ≠bot› assms(1)[unfolded continuous_def]]
by auto
then have "¬ filterlim g at_bot F" "¬ filterlim g at_top F"
using at_bot_le_at_infinity at_top_le_at_infinity filterlim_mono by blast+
then show ?thesis unfolding jumpF_def by auto
qed
lemma jumpF_linear_comp:
assumes "c≠0"
shows
"jumpF (f o (λx. c*x+b)) (at_left x) =
(if c>0 then jumpF f (at_left (c*x+b)) else jumpF f (at_right (c*x+b)))"
(is ?case1)
"jumpF (f o (λx. c*x+b)) (at_right x) =
(if c>0 then jumpF f (at_right (c*x+b)) else jumpF f (at_left (c*x+b)))"
(is ?case2)
proof -
let ?g = "λx. c*x+b"
have ?case1 ?case2 when "¬ c>0"
proof -
have "c<0" using ‹c≠0› that by auto
have "filtermap ?g (at_left x) = at_right (?g x)"
"filtermap ?g (at_right x) = at_left (?g x)"
using ‹c<0›
filtermap_linear_at_left[OF ‹c≠0›, of b x]
filtermap_linear_at_right[OF ‹c≠0›, of b x] by auto
then have
"jumpF (f ∘ ?g) (at_left x) = jumpF f (at_right (?g x))"
"jumpF (f ∘ ?g) (at_right x) = jumpF f (at_left (?g x))"
unfolding jumpF_def filterlim_def comp_def
by (auto simp add: filtermap_filtermap[of f ?g,symmetric])
then show ?case1 ?case2 using ‹c<0› by auto
qed
moreover have ?case1 ?case2 when "c>0"
proof -
have "filtermap ?g (at_left x) = at_left (?g x)"
"filtermap ?g (at_right x) = at_right (?g x)"
using that
filtermap_linear_at_left[OF ‹c≠0›, of b x]
filtermap_linear_at_right[OF ‹c≠0›, of b x] by auto
then have
"jumpF (f ∘ ?g) (at_left x) = jumpF f (at_left (?g x))"
"jumpF (f ∘ ?g) (at_right x) = jumpF f (at_right (?g x))"
unfolding jumpF_def filterlim_def comp_def
by (auto simp add: filtermap_filtermap[of f ?g,symmetric])
then show ?case1 ?case2 using that by auto
qed
ultimately show ?case1 ?case2 by auto
qed
lemma jump_const[simp]:"jump (λ_. c) a = 0"
proof -
have False when "LIM x (at_left a). c :> at_bot"
apply (rule not_tendsto_and_filterlim_at_infinity[of "at_left a" "λ_. c" c])
apply auto
using at_bot_le_at_infinity filterlim_mono that by blast
moreover have False when "LIM x (at_left a). c :> at_top"
apply (rule not_tendsto_and_filterlim_at_infinity[of "at_left a" "λ_. c" c])
apply auto
using at_top_le_at_infinity filterlim_mono that by blast
ultimately show ?thesis unfolding jump_def by auto
qed
lemma jump_not_infinity:
"isCont f a ⟹ jump f a =0"
by (meson at_bot_le_at_infinity at_top_le_at_infinity filterlim_at_split
filterlim_def isCont_def jump_def not_tendsto_and_filterlim_at_infinity
order_trans trivial_limit_at_left_real)
lemma jump_jump_poly_aux:
assumes "p≠0" "coprime p q"
shows "jump (λx. poly q x / poly p x) a = jump_poly q p a"
proof (cases "q=0")
case True
then show ?thesis by auto
next
case False
define f where "f ≡ (λx. poly q x / poly p x)"
have ?thesis when "poly q a = 0"
proof -
have "poly p a≠0" using coprime_poly_0[OF ‹coprime p q›] that by blast
then have "isCont f a" unfolding f_def by simp
then have "jump f a=0" using jump_not_infinity by auto
moreover have "jump_poly q p a=0"
using jump_poly_not_root[OF ‹poly p a≠0›] by auto
ultimately show ?thesis unfolding f_def by auto
qed
moreover have ?thesis when "poly q a≠0"
proof (cases "even(order a p)")
case True
define c where "c≡sgn (poly q a)"
note
filterlim_divide_at_bot_at_top_iff
[OF _ that,of "poly q" "at_left a" "poly p",folded f_def c_def,simplified]
filterlim_divide_at_bot_at_top_iff
[OF _ that,of "poly q" "at_right a" "poly p",folded f_def c_def,simplified]
moreover have "(poly p has_sgnx - c) (at_left a) = (poly p has_sgnx - c) (at_right a)"
"(poly p has_sgnx c) (at_left a) = (poly p has_sgnx c) (at_right a)"
using poly_has_sgnx_left_right[OF ‹p≠0›] True by auto
moreover have "c≠0" by (simp add: c_def sgn_if that)
then have False when
"(poly p has_sgnx - c) (at_right a)"
"(poly p has_sgnx c) (at_right a)"
using has_sgnx_unique[OF _ that] by auto
ultimately have "jump f a = 0"
unfolding jump_def by auto
moreover have "jump_poly q p a = 0" unfolding jump_poly_def
using True by (simp add: order_0I that)
ultimately show ?thesis unfolding f_def by auto
next
case False
define c where "c≡sgn (poly q a)"
have "(poly p ⤏ 0) (at a)" using False
by (metis even_zero order_0I poly_tendsto(1))
then have "(poly p ⤏ 0) (at_left a)" and "(poly p ⤏ 0) (at_right a)"
by (auto simp add: filterlim_at_split)
moreover note
filterlim_divide_at_bot_at_top_iff
[OF _ that,of "poly q" _ "poly p",folded f_def c_def]
moreover have "(poly p has_sgnx c) (at_left a) = (poly p has_sgnx - c) (at_right a)"
"(poly p has_sgnx - c) (at_left a) = (poly p has_sgnx c) (at_right a)"
using poly_has_sgnx_left_right[OF ‹p≠0›] False by auto
ultimately have "jump f a = (if (poly p has_sgnx c) (at_right a) then 1
else if (poly p has_sgnx - c) (at_right a) then -1 else 0)"
unfolding jump_def by auto
also have "... = (if sign_r_pos (q * p) a then 1 else - 1)"
proof -
have "(poly p has_sgnx c) (at_right a) ⟷ sign_r_pos (q * p) a "
proof
assume "(poly p has_sgnx c) (at_right a)"
then have "sgnx (poly p) (at_right a) = c" by auto
moreover have "sgnx (poly q) (at_right a) = c"
unfolding c_def using that by (auto intro!: tendsto_nonzero_sgnx)
ultimately have "sgnx (λx. poly (q*p) x) (at_right a) = c * c"
by (simp add:sgnx_times)
moreover have "c≠0" by (simp add: c_def sgn_if that)
ultimately have "sgnx (λx. poly (q*p) x) (at_right a) > 0"
using not_real_square_gt_zero by fastforce
then show "sign_r_pos (q * p) a" using sign_r_pos_sgnx_iff
by blast
next
assume asm:"sign_r_pos (q * p) a"
let ?c1 = "sgnx (poly p) (at_right a)"
let ?c2 = "sgnx (poly q) (at_right a)"
have "0 < sgnx (λx. poly (q * p) x) (at_right a)"
using asm sign_r_pos_sgnx_iff by blast
then have "?c2 * ?c1 >0"
apply (subst (asm) poly_mult)
apply (subst (asm) sgnx_times)
by auto
then have "?c2>0 ∧ ?c1>0 ∨ ?c2<0 ∧ ?c1<0"
by (simp add: zero_less_mult_iff)
then have "?c1=?c2"
using sgnx_values[OF sgnx_able_poly(1), of a,simplified]
by (metis add.inverse_neutral less_minus_iff less_not_sym)
moreover have "sgnx (poly q) (at_right a) = c"
unfolding c_def using that by (auto intro!: tendsto_nonzero_sgnx)
ultimately have "?c1 = c" by auto
then show "(poly p has_sgnx c) (at_right a)"
using sgnx_able_poly(1) sgnx_able_sgnx by blast
qed
then show ?thesis
unfolding jump_poly_def using poly_has_sgnx_values[OF ‹p≠0›]
by (metis add.inverse_inverse c_def sgn_if that)
qed
also have "... = jump_poly q p a"
unfolding jump_poly_def using False order_root that by (simp add: order_root assms(1))
finally show ?thesis unfolding f_def by auto
qed
ultimately show ?thesis by auto
qed
lemma jump_jumpF:
assumes cont:"isCont (inverse o f) a" and
sgnxl:"(f has_sgnx l) (at_left a)" and sgnxr:"(f has_sgnx r) (at_right a)" and
"l≠0 " "r≠0"
shows "jump f a = jumpF f (at_right a) - jumpF f (at_left a)"
proof -
have ?thesis when "filterlim f at_bot (at_left a)" "filterlim f at_top (at_right a)"
unfolding jump_def jumpF_def
using that filterlim_at_top_at_bot[OF _ _ trivial_limit_at_left_real]
by auto
moreover have ?thesis when "filterlim f at_top (at_left a)" "filterlim f at_bot (at_right a)"
unfolding jump_def jumpF_def
using that filterlim_at_top_at_bot[OF _ _ trivial_limit_at_right_real]
by auto
moreover have ?thesis when
"¬ filterlim f at_bot (at_left a) ∨ ¬ filterlim f at_top (at_right a)"
"¬ filterlim f at_top (at_left a) ∨ ¬ filterlim f at_bot (at_right a)"
proof (cases "f a=0")
case False
have "jumpF f (at_right a) = 0" "jumpF f (at_left a) = 0"
proof -
have "isCont (inverse o inverse o f) a" using cont False unfolding comp_def
by (rule_tac continuous_at_within_inverse, auto)
then have "isCont f a" unfolding comp_def by auto
then have "(f ⤏ f a) (at_right a)" "(f ⤏ f a) (at_left a)"
unfolding continuous_at_split by (auto simp add:continuous_within)
moreover note trivial_limit_at_left_real trivial_limit_at_right_real
ultimately show "jumpF f (at_right a) = 0" "jumpF f (at_left a) = 0"
unfolding jumpF_def using filterlim_at_bot_nhds filterlim_at_top_nhds
by metis+
qed
then show ?thesis unfolding jump_def using that by auto
next
case True
then have tends0:"((λx. inverse (f x)) ⤏ 0) (at a)"
using cont unfolding isCont_def comp_def by auto
have "jump f a = 0" using that unfolding jump_def by auto
have r_lim:"if r>0 then filterlim f at_top (at_right a) else filterlim f at_bot (at_right a)"
proof (cases "r>0")
case True
then have "∀⇩F x in (at_right a). 0 < f x"
using sgnxr unfolding has_sgnx_def
by (auto elim:eventually_mono)
then have "filterlim f at_top (at_right a)"
using filterlim_inverse_at_top[of "λx. inverse (f x)", simplified] tends0
unfolding filterlim_at_split by auto
then show ?thesis using True by presburger
next
case False
then have "∀⇩F x in (at_right a). 0 > f x"
using sgnxr ‹r≠0› False unfolding has_sgnx_def
apply (elim eventually_mono)
by (meson linorder_neqE_linordered_idom sgn_less)
then have "filterlim f at_bot (at_right a)"
using filterlim_inverse_at_bot[of "λx. inverse (f x)", simplified] tends0
unfolding filterlim_at_split by auto
then show ?thesis using False by simp
qed
have l_lim:"if l>0 then filterlim f at_top (at_left a) else filterlim f at_bot (at_left a)"
proof (cases "l>0")
case True
then have "∀⇩F x in (at_left a). 0 < f x"
using sgnxl unfolding has_sgnx_def
by (auto elim:eventually_mono)
then have "filterlim f at_top (at_left a)"
using filterlim_inverse_at_top[of "λx. inverse (f x)", simplified] tends0
unfolding filterlim_at_split by auto
then show ?thesis using True by presburger
next
case False
then have "∀⇩F x in (at_left a). 0 > f x"
using sgnxl ‹l≠0› False unfolding has_sgnx_def
apply (elim eventually_mono)
by (meson linorder_neqE_linordered_idom sgn_less)
then have "filterlim f at_bot (at_left a)"
using filterlim_inverse_at_bot[of "λx. inverse (f x)", simplified] tends0
unfolding filterlim_at_split by auto
then show ?thesis using False by simp
qed
have ?thesis when "l>0" "r>0"
using that l_lim r_lim ‹jump f a=0› unfolding jumpF_def by auto
moreover have ?thesis when "¬ l>0" "¬ r>0"
proof -
have "filterlim f at_bot (at_right a)" "filterlim f at_bot (at_left a)"
using r_lim l_lim that by auto
moreover then have "¬ filterlim f at_top (at_right a)" "¬ filterlim f at_top (at_left a)"
by (auto elim: filterlim_at_top_at_bot)
ultimately have "jumpF f (at_right a) = -1/2 " "jumpF f (at_left a) = -1/2"
unfolding jumpF_def by auto
then show ?thesis using ‹jump f a=0› by auto
qed
moreover have ?thesis when "l>0" "¬ r>0"
proof -
note ‹¬ filterlim f at_top (at_left a) ∨ ¬ filterlim f at_bot (at_right a)›
moreover have "filterlim f at_bot (at_right a)" "filterlim f at_top (at_left a)"
using r_lim l_lim that by auto
ultimately have False by auto
then show ?thesis by auto
qed
moreover have ?thesis when "¬ l>0" "r>0"
proof -
note ‹¬ filterlim f at_bot (at_left a) ∨ ¬ filterlim f at_top (at_right a)›
moreover have "filterlim f at_bot (at_left a)" "filterlim f at_top (at_right a)"
using r_lim l_lim that by auto
ultimately have False by auto
then show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
lemma jump_linear_comp:
assumes "c≠0"
shows "jump (f o (λx. c*x+b)) x = (if c>0 then jump f (c*x+b) else -jump f (c*x+b))"
proof (cases "c>0")
case False
then have "c<0" using ‹c≠0› by auto
let ?g = "λx. c*x+b"
have "filtermap ?g (at_left x) = at_right (?g x)"
"filtermap ?g (at_right x) = at_left (?g x)"
using ‹c<0›
filtermap_linear_at_left[OF ‹c≠0›, of b x]
filtermap_linear_at_right[OF ‹c≠0›, of b x] by auto
then have "jump (f ∘ ?g) x = - jump f (c * x + b)"
unfolding jump_def filterlim_def comp_def
apply (auto simp add: filtermap_filtermap[of f ?g,symmetric])
apply (fold filterlim_def)
by (auto elim:filterlim_at_top_at_bot)
then show ?thesis using ‹c<0› by auto
next
case True
let ?g = "λx. c*x+b"
have "filtermap ?g (at_left x) = at_left (?g x)"
"filtermap ?g (at_right x) = at_right (?g x)"
using True
filtermap_linear_at_left[OF ‹c≠0›, of b x]
filtermap_linear_at_right[OF ‹c≠0›, of b x] by auto
then have "jump (f ∘ ?g) x = jump f (c * x + b)"
unfolding jump_def filterlim_def comp_def
by (auto simp add: filtermap_filtermap[of f ?g,symmetric])
then show ?thesis using True by auto
qed
lemma jump_divide_derivative:
assumes "isCont f x" "g x = 0" "f x≠0"
and g_deriv:"(g has_field_derivative c) (at x)" and "c≠0"
shows "jump (λt. f t/g t) x = (if sgn c = sgn ( f x) then 1 else -1)"
proof -
have g_tendsto:"(g ⤏ 0) (at_left x)" "(g ⤏ 0) (at_right x)"
by (metis DERIV_isCont Lim_at_imp_Lim_at_within assms(2) assms(4) continuous_at)+
have f_tendsto:"(f ⤏ f x) (at_left x)" "(f ⤏ f x) (at_right x)"
using Lim_at_imp_Lim_at_within assms(1) continuous_at by blast+
have ?thesis when "c>0" "f x>0"
proof -
have "(g has_sgnx - sgn (f x)) (at_left x)"
using has_sgnx_derivative_at_left[OF g_deriv ‹g x=0›] that by auto
moreover have "(g has_sgnx sgn (f x)) (at_right x)"
using has_sgnx_derivative_at_right[OF g_deriv ‹g x=0›] that by auto
ultimately have "(LIM t at_left x. f t / g t :> at_bot) ∧ (LIM t at_right x. f t / g t :> at_top)"
using filterlim_divide_at_bot_at_top_iff[OF _ ‹f x≠0›, of f]
using f_tendsto(1) f_tendsto(2) g_tendsto(1) g_tendsto(2) by blast
moreover have "sgn c = sgn (f x)" using that by auto
ultimately show ?thesis unfolding jump_def by auto
qed
moreover have ?thesis when "c>0" "f x<0"
proof -
have "(g has_sgnx sgn (f x)) (at_left x)"
using has_sgnx_derivative_at_left[OF g_deriv ‹g x=0›] that by auto
moreover have "(g has_sgnx - sgn (f x)) (at_right x)"
using has_sgnx_derivative_at_right[OF g_deriv ‹g x=0›] that by auto
ultimately have "(LIM t at_left x. f t / g t :> at_top) ∧ (LIM t at_right x. f t / g t :> at_bot)"
using filterlim_divide_at_bot_at_top_iff[OF _ ‹f x≠0›, of f]
using f_tendsto(1) f_tendsto(2) g_tendsto(1) g_tendsto(2) by blast
moreover from this have "¬ (LIM t at_left x. f t / g t :> at_bot)"
using filterlim_at_top_at_bot by fastforce
moreover have "sgn c ≠ sgn (f x)" using that by auto
ultimately show ?thesis unfolding jump_def by auto
qed
moreover have ?thesis when "c<0" "f x>0"
proof -
have "(g has_sgnx sgn (f x)) (at_left x)"
using has_sgnx_derivative_at_left[OF g_deriv ‹g x=0›] that by auto
moreover have "(g has_sgnx - sgn (f x)) (at_right x)"
using has_sgnx_derivative_at_right[OF g_deriv ‹g x=0›] that by auto
ultimately have "(LIM t at_left x. f t / g t :> at_top) ∧ (LIM t at_right x. f t / g t :> at_bot)"
using filterlim_divide_at_bot_at_top_iff[OF _ ‹f x≠0›, of f]
using f_tendsto(1) f_tendsto(2) g_tendsto(1) g_tendsto(2) by blast
moreover from this have "¬ (LIM t at_left x. f t / g t :> at_bot)"
using filterlim_at_top_at_bot by fastforce
moreover have "sgn c ≠ sgn (f x)" using that by auto
ultimately show ?thesis unfolding jump_def by auto
qed
moreover have ?thesis when "c<0" "f x<0"
proof -
have "(g has_sgnx - sgn (f x)) (at_left x)"
using has_sgnx_derivative_at_left[OF g_deriv ‹g x=0›] that by auto
moreover have "(g has_sgnx sgn (f x)) (at_right x)"
using has_sgnx_derivative_at_right[OF g_deriv ‹g x=0›] that by auto
ultimately have "(LIM t at_left x. f t / g t :> at_bot) ∧ (LIM t at_right x. f t / g t :> at_top)"
using filterlim_divide_at_bot_at_top_iff[OF _ ‹f x≠0›, of f]
using f_tendsto(1) f_tendsto(2) g_tendsto(1) g_tendsto(2) by blast
moreover have "sgn c =sgn (f x)" using that by auto
ultimately show ?thesis unfolding jump_def by auto
qed
ultimately show ?thesis using ‹c≠0› ‹f x≠0› by argo
qed
lemma jump_jump_poly: "jump (λx. poly q x / poly p x) a = jump_poly q p a"
proof (cases "p=0")
case True
then show ?thesis by auto
next
case False
obtain p' q' where p':"p= p'*gcd p q" and q':"q=q'*gcd p q"
using gcd_dvd1 gcd_dvd2 dvd_def[of "gcd p q", simplified mult.commute] by metis
then have "coprime p' q'" "p'≠0" "gcd p q≠0" using gcd_coprime ‹p≠0› by auto
define f where "f ≡ (λx. poly q' x / poly p' x)"
define g where "g ≡ (λx. if poly (gcd p q) x = 0 then 0::real else 1)"
have g_tendsto:"(g ⤏ 1) (at_left a)" "(g ⤏ 1) (at_right a)"
proof -
have
"(poly (gcd p q) has_sgnx 1) (at_left a)
∨ (poly (gcd p q) has_sgnx - 1) (at_left a)"
"(poly (gcd p q) has_sgnx 1) (at_right a)
∨ (poly (gcd p q) has_sgnx - 1) (at_right a)"
using ‹p≠0› poly_has_sgnx_values by auto
then have " ∀⇩F x in at_left a. g x = 1" " ∀⇩F x in at_right a. g x = 1"
unfolding has_sgnx_def g_def by (auto elim:eventually_mono)
then show "(g ⤏ 1) (at_left a)" "(g ⤏ 1) (at_right a)"
using tendsto_eventually by auto
qed
have "poly q x / poly p x = g x * f x" for x
unfolding f_def g_def by (subst p',subst q',auto)
then have "jump (λx. poly q x / poly p x) a = jump (λx. g x * f x) a"
by auto
also have "... = jump f a"
unfolding jump_def
apply (subst (1 2) filterlim_tendsto_pos_mult_at_top_iff)
prefer 5
apply (subst (1 2) filterlim_tendsto_pos_mult_at_bot_iff)
using g_tendsto by auto
also have "... = jump_poly q' p' a"
using jump_jump_poly_aux[OF ‹p'≠0› ‹coprime p' q'›] unfolding f_def by auto
also have "... = jump_poly q p a"
using jump_poly_mult[OF ‹gcd p q ≠ 0›, of q'] p' q'
by (metis mult.commute)
finally show ?thesis .
qed
lemma jump_Im_divide_Re_0:
assumes "path g" "Re (g x)≠0" "0<x" "x<1"
shows "jump (λt. Im (g t) / Re (g t)) x = 0"
proof -
have "isCont g x"
using ‹path g›[unfolded path_def] ‹0<x› ‹x<1›
apply (elim continuous_on_interior)
by auto
then have "isCont (λt. Im(g t)/Re(g t)) x" using ‹Re (g x)≠0›
by (auto intro:continuous_intros isCont_Re isCont_Im)
then show "jump (λt. Im(g t)/Re(g t)) x=0"
using jump_not_infinity by auto
qed
lemma jumpF_im_divide_Re_0:
assumes "path g" "Re (g x)≠0"
shows "⟦0≤x;x<1⟧ ⟹ jumpF (λt. Im (g t) / Re (g t)) (at_right x) = 0"
"⟦0<x;x≤1⟧ ⟹ jumpF (λt. Im (g t) / Re (g t)) (at_left x) = 0"
proof -
define g' where "g' = (λt. Im (g t) / Re (g t))"
show "jumpF g' (at_right x) = 0" when "0≤x" "x<1"
proof -
have "(g' ⤏ g' x) (at_right x)"
proof (cases "x=0")
case True
have "continuous (at_right 0) g"
using ‹path g› unfolding path_def
by (auto elim:continuous_on_at_right)
then have "continuous (at_right x) (λt. Im(g t))" "continuous (at_right x) (λt. Re(g t))"
using continuous_Im continuous_Re True by auto
moreover have "Re (g (netlimit (at_right x))) ≠ 0"
using assms(2) by (simp add: Lim_ident_at)
ultimately have "continuous (at_right x) (λt. Im (g t)/Re(g t))"
by (auto intro:continuous_divide)
then show ?thesis unfolding g'_def continuous_def
by (simp add: Lim_ident_at)
next
case False
have "isCont (λx. Im (g x)) x" "isCont (λx. Re (g x)) x"
using ‹path g› unfolding path_def
by (metis False atLeastAtMost_iff at_within_Icc_at continuous_Im continuous_Re
continuous_on_eq_continuous_within less_le that)+
then have "isCont g' x"
using assms(2) unfolding g'_def
by (auto intro:continuous_intros)
then show ?thesis unfolding isCont_def using filterlim_at_split by blast
qed
then have "¬ filterlim g' at_top (at_right x)" "¬ filterlim g' at_bot (at_right x)"
using filterlim_at_top_nhds[of g' "at_right x"] filterlim_at_bot_nhds[of g' "at_right x"]
by auto
then show ?thesis unfolding jumpF_def by auto
qed
show "jumpF g' (at_left x) = 0" when "0<x" "x≤1"
proof -
have "(g' ⤏ g' x) (at_left x)"
proof (cases "x=1")
case True
have "continuous (at_left 1) g"
using ‹path g› unfolding path_def
by (auto elim:continuous_on_at_left)
then have "continuous (at_left x) (λt. Im(g t))" "continuous (at_left x) (λt. Re(g t))"
using continuous_Im continuous_Re True by auto
moreover have "Re (g (netlimit (at_left x))) ≠ 0"
using assms(2) by (simp add: Lim_ident_at)
ultimately have "continuous (at_left x) (λt. Im (g t)/Re(g t))"
by (auto intro:continuous_divide)
then show ?thesis unfolding g'_def continuous_def
by (simp add: Lim_ident_at)
next
case False
have "isCont (λx. Im (g x)) x" "isCont (λx. Re (g x)) x"
using ‹path g› unfolding path_def
by (metis False atLeastAtMost_iff at_within_Icc_at continuous_Im continuous_Re
continuous_on_eq_continuous_within less_le that)+
then have "isCont g' x"
using assms(2) unfolding g'_def
by (auto)
then show ?thesis unfolding isCont_def using filterlim_at_split by blast
qed
then have "¬ filterlim g' at_top (at_left x)" "¬ filterlim g' at_bot (at_left x)"
using filterlim_at_top_nhds[of g' "at_left x"] filterlim_at_bot_nhds[of g' "at_left x"]
by auto
then show ?thesis unfolding jumpF_def by auto
qed
qed
lemma jump_cong:
assumes "x=y" and "eventually (λx. f x=g x) (at x)"
shows "jump f x = jump g y"
proof -
have left:"eventually (λx. f x=g x) (at_left x)"
and right:"eventually (λx. f x=g x) (at_right x)"
using assms(2) eventually_at_split by blast+
from filterlim_cong[OF _ _ this(1)] filterlim_cong[OF _ _ this(2)]
show ?thesis unfolding jump_def using assms(1) by fastforce
qed
lemma jumpF_cong:
assumes "F=G" and "eventually (λx. f x=g x) F"
shows "jumpF f F = jumpF g G"
proof -
have "∀⇩F r in G. f r = g r"
using assms(1) assms(2) by force
then show ?thesis
by (simp add: assms(1) filterlim_cong jumpF_def)
qed
lemma jump_at_left_at_right_eq:
assumes "isCont f x" and "f x ≠ 0" and sgnx_eq:"sgnx g (at_left x) = sgnx g (at_right x)"
shows "jump (λt. f t/g t) x = 0"
proof -
define c where "c = sgn (f x)"
then have "c≠0" using ‹f x≠0› by (simp add: sgn_zero_iff)
have f_tendsto:"(f ⤏ f x) (at_left x)" " (f ⤏ f x) (at_right x)"
using ‹isCont f x› Lim_at_imp_Lim_at_within isCont_def by blast+
have False when "(g has_sgnx - c) (at_left x)" "(g has_sgnx c) (at_right x)"
proof -
have "sgnx g (at_left x) = -c" using that(1) by auto
moreover have "sgnx g (at_right x) = c" using that(2) by auto
ultimately show False using sgnx_eq ‹c≠0› by force
qed
moreover have False when "(g has_sgnx c) (at_left x)" "(g has_sgnx - c) (at_right x)"
proof -
have "sgnx g (at_left x) = c" using that(1) by auto
moreover have "sgnx g (at_right x) = - c" using that(2) by auto
ultimately show False using sgnx_eq ‹c≠0› by force
qed
ultimately show ?thesis
unfolding jump_def
by (auto simp add:f_tendsto filterlim_divide_at_bot_at_top_iff[OF _ ‹f x ≠ 0›] c_def)
qed
lemma jumpF_pos_has_sgnx:
assumes "jumpF f F > 0"
shows "(f has_sgnx 1) F"
proof -
have "filterlim f at_top F" using assms unfolding jumpF_def by argo
then have "eventually (λx. f x>0) F" using filterlim_at_top_dense[of f F] by blast
then show ?thesis unfolding has_sgnx_def
apply (elim eventually_mono)
by auto
qed
lemma jumpF_neg_has_sgnx:
assumes "jumpF f F < 0"
shows "(f has_sgnx -1) F"
proof -
have "filterlim f at_bot F" using assms unfolding jumpF_def by argo
then have "eventually (λx. f x<0) F" using filterlim_at_bot_dense[of f F] by blast
then show ?thesis unfolding has_sgnx_def
apply (elim eventually_mono)
by auto
qed
lemma jumpF_IVT:
fixes f::"real ⇒ real" and a b::real
defines "right≡(λ(R::real ⇒ real ⇒ bool). R (jumpF f (at_right a)) 0
∨ (continuous (at_right a) f ∧ R (f a) 0))"
and
"left≡(λ(R::real ⇒ real ⇒ bool). R (jumpF f (at_left b)) 0
∨ (continuous (at_left b) f ∧ R (f b) 0))"
assumes "a<b" and cont:"continuous_on {a<..<b} f" and
right_left:"right greater ∧ left less ∨ right less ∧ left greater"
shows "∃x. a<x ∧ x<b ∧ f x =0"
proof -
have ?thesis when "right greater" "left less"
proof -
have "(f has_sgnx 1) (at_right a)"
proof -
have ?thesis when "jumpF f (at_right a)>0" using jumpF_pos_has_sgnx[OF that] .
moreover have ?thesis when "f a > 0" "continuous (at_right a) f"
proof -
have "(f ⤏ f a) (at_right a)" using that(2) by (simp add: continuous_within)
then show ?thesis
using tendsto_nonzero_has_sgnx[of f "f a" "at_right a"] that by auto
qed
ultimately show ?thesis using that(1) unfolding right_def by auto
qed
then obtain a' where "a<a'" and a'_def:"∀y. a<y ∧ y < a' ⟶ f y > 0"
unfolding has_sgnx_def eventually_at_right using sgn_1_pos by auto
have "(f has_sgnx - 1) (at_left b)"
proof -
have ?thesis when "jumpF f (at_left b)<0" using jumpF_neg_has_sgnx[OF that] .
moreover have ?thesis when "f b < 0" "continuous (at_left b) f"
proof -
have "(f ⤏ f b) (at_left b)"
using that(2) by (simp add: continuous_within)
then show ?thesis
using tendsto_nonzero_has_sgnx[of f "f b" "at_left b"] that by auto
qed
ultimately show ?thesis using that(2) unfolding left_def by auto
qed
then obtain b' where "b'<b" and b'_def:"∀y. b'<y ∧ y < b ⟶ f y < 0"
unfolding has_sgnx_def eventually_at_left using sgn_1_neg by auto
have "a' ≤ b'"
proof (rule ccontr)
assume "¬ a' ≤ b'"
then have "{a<..<a'} ∩ {b'<..<b} ≠ {}"
using ‹a<a'› ‹b'<b› ‹a<b› by auto
then obtain c where "c∈{a<..<a'}" "c∈{b'<..<b}" by blast
then have "f c>0" "f c<0"
using a'_def b'_def by auto
then show False by auto
qed
define a0 where "a0=(a+a')/2"
define b0 where "b0=(b+b')/2"
have [simp]:"a<a0" "a0<a'" "a0<b0" "b'<b0" "b0<b"
unfolding a0_def b0_def using ‹a<a'› ‹b'<b› ‹a'≤b'› by auto
have "f a0>0" "f b0<0" using a'_def[rule_format,of a0] b'_def[rule_format,of b0] by auto
moreover have "continuous_on {a0..b0} f"
using cont ‹a < a0› ‹b0 < b›
by (meson atLeastAtMost_subseteq_greaterThanLessThan_iff continuous_on_subset)
ultimately have "∃x>a0. x < b0 ∧ f x = 0"
using IVT_strict[of 0 f a0 b0] by auto
then show ?thesis using ‹a < a0› ‹b0 < b›
by (meson lessThan_strict_subset_iff psubsetE subset_psubset_trans)
qed
moreover have ?thesis when "right less" "left greater"
proof -
have "(f has_sgnx -1) (at_right a)"
proof -
have ?thesis when "jumpF f (at_right a)<0" using jumpF_neg_has_sgnx[OF that] .
moreover have ?thesis when "f a < 0" "continuous (at_right a) f"
proof -
have "(f ⤏ f a) (at_right a)"
using that(2) by (simp add: continuous_within)
then show ?thesis
using tendsto_nonzero_has_sgnx[of f "f a" "at_right a"] that by auto
qed
ultimately show ?thesis using that(1) unfolding right_def by auto
qed
then obtain a' where "a<a'" and a'_def:"∀y. a<y ∧ y < a' ⟶ f y < 0"
unfolding has_sgnx_def eventually_at_right using sgn_1_neg by auto
have "(f has_sgnx 1) (at_left b)"
proof -
have ?thesis when "jumpF f (at_left b)>0" using jumpF_pos_has_sgnx[OF that] .
moreover have ?thesis when "f b > 0" "continuous (at_left b) f"
proof -
have "(f ⤏ f b) (at_left b)"
using that(2) by (simp add: continuous_within)
then show ?thesis
using tendsto_nonzero_has_sgnx[of f "f b" "at_left b"] that by auto
qed
ultimately show ?thesis using that(2) unfolding left_def by auto
qed
then obtain b' where "b'<b" and b'_def:"∀y. b'<y ∧ y < b ⟶ f y > 0"
unfolding has_sgnx_def eventually_at_left using sgn_1_pos by auto
have "a' ≤ b'"
proof (rule ccontr)
assume "¬ a' ≤ b'"
then have "{a<..<a'} ∩ {b'<..<b} ≠ {}"
using ‹a<a'› ‹b'<b› ‹a<b› by auto
then obtain c where "c∈{a<..<a'}" "c∈{b'<..<b}" by blast
then have "f c>0" "f c<0"
using a'_def b'_def by auto
then show False by auto
qed
define a0 where "a0=(a+a')/2"
define b0 where "b0=(b+b')/2"
have [simp]:"a<a0" "a0<a'" "a0<b0" "b'<b0" "b0<b"
unfolding a0_def b0_def using ‹a<a'› ‹b'<b› ‹a'≤b'› by auto
have "f a0<0" "f b0>0" using a'_def[rule_format,of a0] b'_def[rule_format,of b0] by auto
moreover have "continuous_on {a0..b0} f"
using cont ‹a < a0› ‹b0 < b›
by (meson atLeastAtMost_subseteq_greaterThanLessThan_iff continuous_on_subset)
ultimately have "∃x>a0. x < b0 ∧ f x = 0"
using IVT_strict[of 0 f a0 b0] by auto
then show ?thesis using ‹a < a0› ‹b0 < b›
by (meson lessThan_strict_subset_iff psubsetE subset_psubset_trans)
qed
ultimately show ?thesis using right_left by auto
qed
lemma jumpF_eventually_const:
assumes "eventually (λx. f x=c) F" "F≠bot"
shows "jumpF f F = 0"
proof -
have "jumpF f F = jumpF (λ_. c) F"
apply (rule jumpF_cong)
using assms(1) by auto
also have "... = 0" using jumpF_const[OF ‹F≠bot›] by simp
finally show ?thesis .
qed
lemma jumpF_tan_comp:
"jumpF (f o tan) (at_right x) = (if cos x = 0
then jumpF f at_bot else jumpF f (at_right (tan x)))"
"jumpF (f o tan) (at_left x) = (if cos x =0
then jumpF f at_top else jumpF f (at_left (tan x)))"
proof -
have "filtermap (f ∘ tan) (at_right x) =
(if cos x = 0 then filtermap f at_bot else filtermap f (at_right (tan x)))"
unfolding comp_def
apply (subst filtermap_filtermap[of f tan,symmetric])
using filtermap_tan_at_right_inf filtermap_tan_at_right by auto
then show "jumpF (f o tan) (at_right x) = (if cos x = 0
then jumpF f at_bot else jumpF f (at_right (tan x)))"
unfolding jumpF_def filterlim_def by auto
next
have "filtermap (f ∘ tan) (at_left x) =
(if cos x = 0 then filtermap f at_top else filtermap f (at_left (tan x)))"
unfolding comp_def
apply (subst filtermap_filtermap[of f tan,symmetric])
using filtermap_tan_at_left_inf filtermap_tan_at_left by auto
then show "jumpF (f o tan) (at_left x) = (if cos x = 0
then jumpF f at_top else jumpF f (at_left (tan x)))"
unfolding jumpF_def filterlim_def by auto
qed
subsection ‹Finite jumpFs over an interval›
definition finite_jumpFs::"(real ⇒ real) ⇒ real ⇒ real ⇒ bool" where
"finite_jumpFs f a b = finite {x. (jumpF f (at_left x) ≠0 ∨ jumpF f (at_right x) ≠0) ∧ a≤x ∧ x≤b}"
lemma finite_jumpFs_linear_pos:
assumes "c>0"
shows "finite_jumpFs (f o (λx. c * x + b)) lb ub ⟷ finite_jumpFs f (c * lb +b) (c * ub + b)"
proof -
define left where "left = (λf lb ub. {x. jumpF f (at_left x) ≠ 0 ∧ lb ≤ x ∧ x ≤ ub})"
define right where "right = (λf lb ub. {x. jumpF f (at_right x) ≠ 0 ∧ lb ≤ x ∧ x ≤ ub})"
define g where "g=(λx. c*x+b)"
define gi where "gi = (λx. (x-b)/c)"
have "finite_jumpFs (f o (λx. c * x + b)) lb ub
= finite (left (f o g) lb ub ∪ right (f o g) lb ub)"
unfolding finite_jumpFs_def
apply (rule arg_cong[where f=finite])
by (auto simp add:left_def right_def g_def)
also have "... = finite (gi ` (left f (g lb) (g ub) ∪ right f (g lb) (g ub)))"
proof -
have j_rw:
"jumpF (f o g) (at_left x) = jumpF f (at_left (g x))"
"jumpF (f o g) (at_right x) = jumpF f (at_right (g x))"
for x
using jumpF_linear_comp[of c f b x] ‹c>0› unfolding g_def by auto
then have
"left (f o g) lb ub = gi ` left f (g lb) (g ub)"
"right (f o g) lb ub = gi ` right f (g lb) (g ub)"
unfolding left_def right_def gi_def
using ‹c>0› by (auto simp add:g_def field_simps)
then have "left (f o g) lb ub ∪ right (f o g) lb ub
= gi ` (left f (g lb) (g ub) ∪ right f (g lb) (g ub))"
by auto
then show ?thesis by auto
qed
also have "... = finite (left f (g lb) (g ub) ∪ right f (g lb) (g ub))"
apply (rule finite_image_iff)
unfolding gi_def using ‹c >0› inj_on_def by fastforce
also have "... = finite_jumpFs f (c * lb +b) (c * ub + b)"
unfolding finite_jumpFs_def
apply (rule arg_cong[where f=finite])
by (auto simp add:left_def right_def g_def)
finally show ?thesis .
qed
lemma finite_jumpFs_consts:
"finite_jumpFs (λ_ . c) lb ub"
unfolding finite_jumpFs_def using jumpF_const by auto
lemma finite_jumpFs_combine:
assumes "finite_jumpFs f a b" "finite_jumpFs f b c"
shows "finite_jumpFs f a c"
proof -
define P where "P=(λx. jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0)"
have "{x. P x ∧ a ≤ x ∧ x ≤ c} ⊆ {x. P x ∧ a ≤ x ∧ x≤b} ∪ {x. P x ∧ b ≤x ∧ x≤c}"
by auto
moreover have "finite ({x. P x ∧ a ≤ x ∧ x≤b} ∪ {x. P x ∧ b ≤x ∧ x≤c})"
using assms unfolding finite_jumpFs_def P_def by auto
ultimately have "finite {x. P x ∧ a ≤ x ∧ x ≤ c}"
using finite_subset by auto
then show ?thesis unfolding finite_jumpFs_def P_def by auto
qed
lemma finite_jumpFs_subE:
assumes "finite_jumpFs f a b" "a≤a'" "b'≤b"
shows "finite_jumpFs f a' b'"
using assms unfolding finite_jumpFs_def
apply (elim rev_finite_subset)
by auto
lemma finite_Psegments_Re_imp_jumpFs:
assumes "finite_Psegments (λt. Re (g t - z) = 0) a b" "continuous_on {a..b} g"
shows "finite_jumpFs (λt. Im (g t - z)/Re (g t - z)) a b"
using assms
proof (induct rule:finite_Psegments.induct)
case (emptyI a b)
then show ?case unfolding finite_jumpFs_def
by (auto intro:rev_finite_subset[of "{a}"])
next
case (insertI_1 s a b)
define f where "f=(λt. Im (g t - z) / Re (g t - z))"
have "finite_jumpFs f a s"
proof -
have "continuous_on {a..s} g" using ‹continuous_on {a..b} g› ‹s ∈ {a..<b}›
by (auto elim:continuous_on_subset)
then show ?thesis using insertI_1 unfolding f_def by auto
qed
moreover have "finite_jumpFs f s b"
proof -
have "jumpF f (at_left x) =0" "jumpF f (at_right x) = 0" when "x∈{s<..<b}" for x
proof -
show "jumpF f (at_left x) =0"
apply (rule jumpF_eventually_const[of _ 0])
unfolding eventually_at_left
apply (rule exI[where x=s])
using that insertI_1 unfolding f_def by auto
show "jumpF f (at_right x) = 0"
apply (rule jumpF_eventually_const[of _ 0])
unfolding eventually_at_right
apply (rule exI[where x=b])
using that insertI_1 unfolding f_def by auto
qed
then have "{x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ s ≤ x ∧ x ≤ b}
= {x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ (x=s ∨ x = b)}"
using ‹s∈{a..<b}› by force
then show ?thesis unfolding finite_jumpFs_def by auto
qed
ultimately show ?case using finite_jumpFs_combine[of _ a s b] unfolding f_def by auto
next
case (insertI_2 s a b)
define f where "f=(λt. Im (g t - z) / Re (g t - z))"
have "finite_jumpFs f a s"
proof -
have "continuous_on {a..s} g" using ‹continuous_on {a..b} g› ‹s ∈ {a..<b}›
by (auto elim:continuous_on_subset)
then show ?thesis using insertI_2 unfolding f_def by auto
qed
moreover have "finite_jumpFs f s b"
proof -
have "jumpF f (at_left x) =0" "jumpF f (at_right x) = 0" when "x∈{s<..<b}" for x
proof -
have "isCont f x"
unfolding f_def
apply (intro continuous_intros isCont_Im isCont_Re
continuous_on_interior[OF ‹continuous_on {a..b} g›])
using insertI_2.hyps(1) that
apply auto[2]
using insertI_2.hyps(3) that by blast
then show "jumpF f (at_left x) =0" "jumpF f (at_right x) = 0"
by (simp_all add: continuous_at_split jumpF_not_infinity)
qed
then have "{x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ s ≤ x ∧ x ≤ b}
= {x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ (x=s ∨ x = b)}"
using ‹s∈{a..<b}› by force
then show ?thesis unfolding finite_jumpFs_def by auto
qed
ultimately show ?case using finite_jumpFs_combine[of _ a s b] unfolding f_def by auto
qed
lemma finite_ReZ_segments_imp_jumpFs:
assumes "finite_ReZ_segments g z" "path g"
shows "finite_jumpFs (λt. Im (g t - z)/Re (g t - z)) 0 1"
using assms unfolding finite_ReZ_segments_def path_def
by (rule finite_Psegments_Re_imp_jumpFs)
subsection ‹@{term jumpF} at path ends›
definition jumpF_pathstart::"(real ⇒ complex) ⇒ complex ⇒ real" where
"jumpF_pathstart g z= jumpF (λt. Im(g t- z)/Re(g t - z)) (at_right 0)"
definition jumpF_pathfinish::"(real ⇒ complex) ⇒ complex ⇒ real" where
"jumpF_pathfinish g z= jumpF (λt. Im(g t - z)/Re(g t -z)) (at_left 1)"
lemma jumpF_pathstart_eq_0:
assumes "path g" "Re(pathstart g)≠Re z"
shows "jumpF_pathstart g z = 0"
unfolding jumpF_pathstart_def
apply (rule jumpF_im_divide_Re_0)
using assms[unfolded pathstart_def] by auto
lemma jumpF_pathfinish_eq_0:
assumes "path g" "Re(pathfinish g)≠Re z"
shows "jumpF_pathfinish g z = 0"
unfolding jumpF_pathfinish_def
apply (rule jumpF_im_divide_Re_0)
using assms[unfolded pathfinish_def] by auto
lemma
shows jumpF_pathfinish_reversepath: "jumpF_pathfinish (reversepath g) z = jumpF_pathstart g z"
and jumpF_pathstart_reversepath: "jumpF_pathstart (reversepath g) z = jumpF_pathfinish g z"
proof -
define f where "f=(λt. Im (g t - z) / Re (g t - z))"
define f' where "f'=(λt. Im (reversepath g t - z) / Re (reversepath g t - z))"
have "f o (λt. 1 - t) = f'"
unfolding f_def f'_def comp_def reversepath_def by auto
then show "jumpF_pathfinish (reversepath g) z = jumpF_pathstart g z"
"jumpF_pathstart (reversepath g) z = jumpF_pathfinish g z"
unfolding jumpF_pathstart_def jumpF_pathfinish_def
using jumpF_linear_comp(2)[of "-1" f 1 0,simplified] jumpF_linear_comp(1)[of "-1" f 1 1,simplified]
apply (fold f_def f'_def)
by auto
qed
lemma jumpF_pathstart_joinpaths[simp]:
"jumpF_pathstart (g1+++g2) z = jumpF_pathstart g1 z"
proof -
let ?h="(λt. Im (g1 t - z) / Re (g1 t - z))"
let ?f="λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)"
have "jumpF_pathstart g1 z = jumpF ?h (at_right 0)"
unfolding jumpF_pathstart_def by simp
also have "... = jumpF (?h o (λt. 2*t)) (at_right 0)"
using jumpF_linear_comp[of 2 ?h 0 0,simplified] by auto
also have "... = jumpF ?f (at_right 0)"
proof (rule jumpF_cong)
show " ∀⇩F x in at_right 0. (?h ∘ (*) 2) x =?f x"
unfolding eventually_at_right
apply (intro exI[where x="1/2"])
by (auto simp add:joinpaths_def)
qed simp
also have "... =jumpF_pathstart (g1+++g2) z"
unfolding jumpF_pathstart_def by simp
finally show ?thesis by simp
qed
lemma jumpF_pathfinish_joinpaths[simp]:
"jumpF_pathfinish (g1+++g2) z = jumpF_pathfinish g2 z"
proof -
let ?h="(λt. Im (g2 t - z) / Re (g2 t - z))"
let ?f="λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)"
have "jumpF_pathfinish g2 z = jumpF ?h (at_left 1)"
unfolding jumpF_pathfinish_def by simp
also have "... = jumpF (?h o (λt. 2*t-1)) (at_left 1)"
using jumpF_linear_comp[of 2 _ "-1" 1,simplified] by auto
also have "... = jumpF ?f (at_left 1)"
proof (rule jumpF_cong)
show " ∀⇩F x in at_left 1. (?h ∘ (λt. 2 * t - 1)) x =?f x"
unfolding eventually_at_left
apply (intro exI[where x="1/2"])
by (auto simp add:joinpaths_def)
qed simp
also have "... =jumpF_pathfinish (g1+++g2) z"
unfolding jumpF_pathfinish_def by simp
finally show ?thesis by simp
qed
subsection ‹Cauchy index›
definition cindex::"real ⇒ real ⇒ (real ⇒ real) ⇒ int" where
"cindex a b f = (∑x∈{x. jump f x≠0 ∧ a<x ∧ x<b}. jump f x )"
definition cindexE::"real ⇒ real ⇒ (real ⇒ real) ⇒ real" where
"cindexE a b f = (∑x∈{x. jumpF f (at_right x) ≠0 ∧ a≤x ∧ x<b}. jumpF f (at_right x))
- (∑x∈{x. jumpF f (at_left x) ≠0 ∧ a<x ∧ x≤b}. jumpF f (at_left x))"
definition cindexE_ubd::"(real ⇒ real) ⇒ real" where
"cindexE_ubd f = (∑x∈{x. jumpF f (at_right x) ≠0 }. jumpF f (at_right x))
- (∑x∈{x. jumpF f (at_left x) ≠0}. jumpF f (at_left x))"
lemma cindexE_empty:
"cindexE a a f = 0"
unfolding cindexE_def by (simp add: sum.neutral)
lemma cindex_const: "cindex a b (λ_. c) = 0"
unfolding cindex_def
apply (rule sum.neutral)
by auto
lemma cindex_eq_cindex_poly: "cindex a b (λx. poly q x/poly p x) = cindex_poly a b q p"
proof (cases "p=0")
case True
then show ?thesis using cindex_const by auto
next
case False
have "cindex_poly a b q p =
(∑x |jump_poly q p x ≠0 ∧ a < x ∧ x < b. jump_poly q p x)"
unfolding cindex_poly_def
apply (rule sum.mono_neutral_cong_right)
using jump_poly_not_root by (auto simp add: ‹p≠0› poly_roots_finite)
also have "... = cindex a b (λx. poly q x/poly p x)"
unfolding cindex_def
apply (rule sum.cong)
using jump_jump_poly[of q] by auto
finally show ?thesis by auto
qed
lemma cindex_combine:
assumes finite:"finite {x. jump f x≠0 ∧ a<x ∧ x<c}" and "a<b" "b<c"
shows "cindex a c f = cindex a b f + jump f b + cindex b c f"
proof -
define ssum where "ssum = (λs. sum (jump f) ({x. jump f x≠0 ∧ a<x ∧ x<c} ∩ s))"
have ssum_union:"ssum (A ∪ B) = ssum A + ssum B" when "A ∩ B ={}" for A B
proof -
define C where "C={x. jump f x ≠ 0 ∧ a<x ∧ x<c}"
have "finite C" using finite unfolding C_def .
then show ?thesis
unfolding ssum_def
apply (fold C_def)
using sum_Un[of "C ∩ A" "C ∩ B"] that
by (simp add: inf_assoc inf_sup_aci(3) inf_sup_distrib1 sum.union_disjoint)
qed
have "cindex a c f = ssum ({a<..<b} ∪ {b} ∪ {b<..<c})"
unfolding ssum_def cindex_def
apply (rule sum.cong[of _ _ "jump f" "jump f",simplified])
using ‹a<b› ‹b<c› by fastforce
moreover have "cindex a b f = ssum {a<..<b}"
unfolding cindex_def ssum_def using ‹a<b› ‹b<c›
by (intro sum.cong,auto)
moreover have "jump f b = ssum {b}"
unfolding ssum_def using ‹a<b› ‹b<c› by (cases "jump f b=0",auto)
moreover have "cindex b c f = ssum {b<..<c}"
unfolding cindex_def ssum_def using ‹a<b› ‹b<c› by (intro sum.cong,auto)
ultimately show ?thesis
apply (subst (asm) ssum_union,simp)
by (subst (asm) ssum_union,auto)
qed
lemma cindexE_combine:
assumes finite:"finite_jumpFs f a c" and "a≤b" "b≤c"
shows "cindexE a c f = cindexE a b f + cindexE b c f"
proof -
define S where "S={x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ a ≤ x ∧ x ≤ c}"
define A0 where "A0={x. jumpF f (at_right x) ≠ 0 ∧ a ≤ x ∧ x < c}"
define A1 where "A1={x. jumpF f (at_right x) ≠ 0 ∧ a ≤ x ∧ x < b}"
define A2 where "A2={x. jumpF f (at_right x) ≠ 0 ∧ b ≤ x ∧ x < c}"
define B0 where "B0={x. jumpF f (at_left x) ≠ 0 ∧ a < x ∧ x ≤ c}"
define B1 where "B1={x. jumpF f (at_left x) ≠ 0 ∧ a < x ∧ x ≤ b}"
define B2 where "B2={x. jumpF f (at_left x) ≠ 0 ∧ b < x ∧ x ≤ c}"
have [simp]:"finite A1" "finite A2" "finite B1" "finite B2"
proof -
have "finite S" using finite unfolding finite_jumpFs_def S_def by auto
moreover have "A1 ⊆ S" "A2 ⊆ S" "B1 ⊆ S" "B2 ⊆ S"
unfolding A1_def A2_def B1_def B2_def S_def using ‹a≤b› ‹b≤c› by auto
ultimately show "finite A1" "finite A2" "finite B1" "finite B2" by (auto elim:finite_subset)
qed
have "cindexE a c f = sum (λx. jumpF f (at_right x)) A0
- sum (λx. jumpF f (at_left x)) B0"
unfolding cindexE_def A0_def B0_def by auto
also have "... = sum (λx. jumpF f (at_right x)) (A1 ∪ A2)
- sum (λx. jumpF f (at_left x)) (B1 ∪ B2)"
proof -
have "A0=A1∪A2" unfolding A0_def A1_def A2_def using assms by auto
moreover have "B0=B1∪B2" unfolding B0_def B1_def B2_def using assms by auto
ultimately show ?thesis by auto
qed
also have "... = cindexE a b f + cindexE b c f"
proof -
have "A1 ∩ A2 = {}" unfolding A1_def A2_def by auto
moreover have "B1 ∩ B2 = {}" unfolding B1_def B2_def by auto
ultimately show ?thesis
unfolding cindexE_def
apply (fold A1_def A2_def B1_def B2_def)
by (auto simp add:sum.union_disjoint)
qed
finally show ?thesis .
qed
lemma cindex_linear_comp:
assumes "c≠0"
shows "cindex lb ub (f o (λx. c*x+b)) = (if c>0
then cindex (c*lb+b) (c*ub+b) f
else - cindex (c*ub+b) (c*lb+b) f)"
proof (cases "c>0")
case False
then have "c<0" using ‹c≠0› by auto
have "cindex lb ub (f o (λx. c*x+b)) = - cindex (c*ub+b) (c*lb+b) f"
unfolding cindex_def
apply (subst sum_negf[symmetric])
apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
subgoal by (simp add: inj_on_def)
subgoal using False
apply (subst jump_linear_comp[OF ‹c≠0›])
by (auto simp add:‹c<0› ‹c≠0› field_simps)
subgoal for x
apply (subst jump_linear_comp[OF ‹c≠0›])
by (auto simp add:‹c<0› ‹c≠0› False field_simps)
done
then show ?thesis using False by auto
next
case True
have "cindex lb ub (f o (λx. c*x+b)) = cindex (c*lb+b) (c*ub+b) f"
unfolding cindex_def
apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
subgoal by (simp add: inj_on_def)
subgoal
apply (subst jump_linear_comp[OF ‹c≠0›])
by (auto simp add: True ‹c≠0› field_simps)
subgoal for x
apply (subst jump_linear_comp[OF ‹c≠0›])
by (auto simp add: ‹c≠0› True field_simps)
done
then show ?thesis using True by auto
qed
lemma cindexE_linear_comp:
assumes "c≠0"
shows "cindexE lb ub (f o (λx. c*x+b)) = (if c>0
then cindexE (c*lb+b) (c*ub+b) f
else - cindexE (c*ub+b) (c*lb+b) f)"
proof -
define cright where "cright = (λlb ub f. (∑x | jumpF f (at_right x) ≠ 0 ∧ lb ≤ x ∧ x < ub.
jumpF f (at_right x)))"
define cleft where "cleft = (λlb ub f. (∑x | jumpF f (at_left x) ≠ 0 ∧ lb < x ∧ x ≤ ub.
jumpF f (at_left x)))"
have cindexE_unfold:"cindexE lb ub f = cright lb ub f - cleft lb ub f"
for lb ub f unfolding cindexE_def cright_def cleft_def by auto
have ?thesis when "c<0"
proof -
have "cright lb ub (f ∘ (λx. c * x + b)) = cleft (c * ub + b) (c * lb + b) f"
unfolding cright_def cleft_def
apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
subgoal by (simp add: inj_on_def)
subgoal using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add:field_simps)
subgoal for x using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add: field_simps)
done
moreover have "cleft lb ub (f ∘ (λx. c * x + b)) = cright (c*ub+b) (c*lb + b) f"
unfolding cright_def cleft_def
apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
subgoal by (simp add: inj_on_def)
subgoal using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add:field_simps)
subgoal for x using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add: field_simps)
done
ultimately show ?thesis unfolding cindexE_unfold using that by auto
qed
moreover have ?thesis when "c>0"
proof -
have "cright lb ub (f ∘ (λx. c * x + b)) = cright (c * lb + b) (c * ub + b) f"
unfolding cright_def cleft_def
apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
subgoal by (simp add: inj_on_def)
subgoal using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add:field_simps)
subgoal for x using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add: field_simps)
done
moreover have "cleft lb ub (f ∘ (λx. c * x + b)) = cleft (c*lb+b) (c*ub + b) f"
unfolding cright_def cleft_def
apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
subgoal by (simp add: inj_on_def)
subgoal using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add:field_simps)
subgoal for x using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add: field_simps)
done
ultimately show ?thesis unfolding cindexE_unfold using that by auto
qed
ultimately show ?thesis using ‹c≠0› by auto
qed
lemma cindexE_cong:
assumes "finite s" and fg_eq:"⋀x. ⟦a<x;x<b;x∉s⟧ ⟹ f x = g x"
shows "cindexE a b f = cindexE a b g"
proof -
define left where
"left=(λf. (∑x | jumpF f (at_left x) ≠ 0 ∧ a < x ∧ x ≤ b. jumpF f (at_left x)))"
define right where
"right=(λf. (∑x | jumpF f (at_right x) ≠ 0 ∧ a ≤ x ∧ x < b. jumpF f (at_right x)))"
have "left f = left g"
proof -
have "jumpF f (at_left x) = jumpF g (at_left x)" when "a<x" "x≤b" for x
proof (rule jumpF_cong)
define cs where "cs ≡ {y∈s. a<y ∧ y<x}"
define c where "c≡ (if cs = {} then (x+a)/2 else Max cs)"
have "finite cs" unfolding cs_def using assms(1) by auto
have "c<x ∧ (∀y. c<y ∧ y<x ⟶ f y=g y)"
proof (cases "cs={}")
case True
then have "∀y. c<y ∧ y<x ⟶ y ∉ s" unfolding cs_def c_def by force
moreover have "c=(x+a)/2" using True unfolding c_def by auto
ultimately show ?thesis using fg_eq using that by auto
next
case False
then have "c∈cs" unfolding c_def using False ‹finite cs› by auto
moreover have "∀y. c<y ∧ y<x ⟶ y ∉ s"
proof (rule ccontr)
assume "¬ (∀y. c < y ∧ y < x ⟶ y ∉ s) "
then obtain y' where "c<y'" "y'<x" "y'∈s" by auto
then have "y'∈cs" using ‹c∈cs› unfolding cs_def by auto
then have "y'≤c" unfolding c_def using False ‹finite cs› by auto
then show False using ‹c<y'› by auto
qed
ultimately show ?thesis unfolding cs_def using that by (auto intro!:fg_eq)
qed
then show "∀⇩F x in at_left x. f x = g x"
unfolding eventually_at_left by auto
qed simp
then show ?thesis
unfolding left_def
by (auto intro: sum.cong)
qed
moreover have "right f = right g"
proof -
have "jumpF f (at_right x) = jumpF g (at_right x)" when "a≤x" "x<b" for x
proof (rule jumpF_cong)
define cs where "cs ≡ {y∈s. x<y ∧ y<b}"
define c where "c≡ (if cs = {} then (x+b)/2 else Min cs)"
have "finite cs" unfolding cs_def using assms(1) by auto
have "x<c ∧ (∀y. x<y ∧ y<c ⟶ f y=g y)"
proof (cases "cs={}")
case True
then have "∀y. x<y ∧ y<c ⟶ y ∉ s" unfolding cs_def c_def by force
moreover have "c=(x+b)/2" using True unfolding c_def by auto
ultimately show ?thesis using fg_eq using that by auto
next
case False
then have "c∈cs" unfolding c_def using False ‹finite cs› by auto
moreover have "∀y. x<y ∧ y<c ⟶ y ∉ s"
proof (rule ccontr)
assume "¬ (∀y. x < y ∧ y < c ⟶ y ∉ s) "
then obtain y' where "x<y'" "y'<c" "y'∈s" by auto
then have "y'∈cs" using ‹c∈cs› unfolding cs_def by auto
then have "y'≥c" unfolding c_def using False ‹finite cs› by auto
then show False using ‹c>y'› by auto
qed
ultimately show ?thesis unfolding cs_def using that by (auto intro!:fg_eq)
qed
then show "∀⇩F x in at_right x. f x = g x"
unfolding eventually_at_right by auto
qed simp
then show ?thesis
unfolding right_def
by (auto intro: sum.cong)
qed
ultimately show ?thesis unfolding cindexE_def left_def right_def by presburger
qed
lemma cindexE_constI:
assumes "⋀t. ⟦a<t;t<b⟧ ⟹ f t=c"
shows "cindexE a b f = 0"
proof -
define left where
"left=(λf. (∑x | jumpF f (at_left x) ≠ 0 ∧ a < x ∧ x ≤ b. jumpF f (at_left x)))"
define right where
"right=(λf. (∑x | jumpF f (at_right x) ≠ 0 ∧ a ≤ x ∧ x < b. jumpF f (at_right x)))"
have "left f = 0"
proof -
have "jumpF f (at_left x) = 0" when "a<x" "x≤b" for x
apply (rule jumpF_eventually_const[of _ c])
unfolding eventually_at_left using assms that by auto
then show ?thesis unfolding left_def by auto
qed
moreover have "right f = 0"
proof -
have "jumpF f (at_right x) = 0" when "a≤x" "x<b" for x
apply (rule jumpF_eventually_const[of _ c])
unfolding eventually_at_right using assms that by auto
then show ?thesis unfolding right_def by auto
qed
ultimately show ?thesis unfolding cindexE_def left_def right_def by auto
qed
lemma cindex_eq_cindexE_divide:
fixes f g::"real ⇒ real"
defines "h ≡ (λx. f x/g x)"
assumes "a<b" and
finite_fg: "finite {x. (f x=0∨g x=0) ∧ a≤x∧x≤b}" and
g_imp_f:"∀x∈{a..b}. g x=0 ⟶ f x≠0" and
f_cont:"continuous_on {a..b} f" and
g_cont:"continuous_on {a..b} g"
shows "cindexE a b h = jumpF h (at_right a) + cindex a b h - jumpF h (at_left b)"
proof -
define R where "R=(λS.{x. jumpF h (at_right x) ≠ 0 ∧ x∈S})"
define L where "L=(λS.{x. jumpF h (at_left x) ≠ 0 ∧ x∈S})"
define right where "right = (λS. (∑x∈R S. jumpF h (at_right x)))"
define left where "left = (λS. (∑x∈L S. jumpF h (at_left x)))"
have jump_gnz:"jumpF h (at_left x) = 0" "jumpF h (at_right x) = 0" "jump h x=0"
when "a<x" "x<b" "g x≠0" for x
proof -
have "isCont h x" unfolding h_def using f_cont g_cont that
by (auto intro!:continuous_intros elim:continuous_on_interior)
then show "jumpF h (at_left x) = 0" "jumpF h (at_right x) = 0" "jump h x=0"
using jumpF_not_infinity jump_not_infinity unfolding continuous_at_split by auto
qed
have finite_jFs:"finite_jumpFs h a b"
proof -
define S where "S=(λs. {x. (jumpF h (at_left x) ≠ 0 ∨ jumpF h (at_right x) ≠ 0) ∧ x∈s})"
note jump_gnz
then have "S {a<..<b} ⊆ {x. (f x=0∨g x=0) ∧ a≤x∧x≤b}"
unfolding S_def by auto
then have "finite (S {a<..<b})"
using rev_finite_subset[OF finite_fg] by auto
moreover have "finite (S {a,b})" unfolding S_def by auto
moreover have "S {a..b} = S {a<..<b} ∪ S {a,b}"
unfolding S_def using ‹a<b› by auto
ultimately have "finite (S {a..b})" by auto
then show ?thesis unfolding S_def finite_jumpFs_def by auto
qed
have "cindexE a b h = right {a..<b} - left {a<..b}"
unfolding cindexE_def right_def left_def R_def L_def by auto
also have "... = jumpF h (at_right a) + right {a<..<b} - left {a<..<b} - jumpF h (at_left b)"
proof -
have "right {a..<b} = jumpF h (at_right a) + right {a<..<b}"
proof (cases "jumpF h (at_right a) =0")
case True
then have "R {a..<b} = R {a<..<b}"
unfolding R_def using less_eq_real_def by auto
then have "right {a..<b} = right {a<..<b}"
unfolding right_def by auto
then show ?thesis using True by auto
next
case False
have "finite (R {a..<b})"
using finite_jFs unfolding R_def finite_jumpFs_def
by (auto elim:rev_finite_subset)
moreover have "a ∈ R {a..<b}" using False ‹a<b› unfolding R_def by auto
moreover have "R {a..<b} - {a} = R {a<..<b}" unfolding R_def by auto
ultimately show "right {a..<b}= jumpF h (at_right a)
+ right {a<..<b}"
using sum.remove[of "R {a..<b}" a "λx. jumpF h (at_right x)"]
unfolding right_def by simp
qed
moreover have "left {a<..b} = jumpF h (at_left b) + left {a<..<b}"
proof (cases "jumpF h (at_left b) =0")
case True
then have "L {a<..b} = L {a<..<b}"
unfolding L_def using less_eq_real_def by auto
then have "left {a<..b} = left {a<..<b}"
unfolding left_def by auto
then show ?thesis using True by auto
next
case False
have "finite (L {a<..b})"
using finite_jFs unfolding L_def finite_jumpFs_def
by (auto elim:rev_finite_subset)
moreover have "b ∈ L {a<..b}" using False ‹a<b› unfolding L_def by auto
moreover have "L {a<..b} - {b} = L {a<..<b}" unfolding L_def by auto
ultimately show "left {a<..b}= jumpF h (at_left b) + left {a<..<b}"
using sum.remove[of "L {a<..b}" b "λx. jumpF h (at_left x)"]
unfolding left_def by simp
qed
ultimately show ?thesis by simp
qed
also have "... = jumpF h (at_right a) + cindex a b h - jumpF h (at_left b)"
proof -
define S where "S={x. g x=0 ∧ a < x ∧ x < b}"
have "right {a<..<b} = sum (λx. jumpF h (at_right x)) S"
unfolding right_def S_def R_def
apply (rule sum.mono_neutral_left)
subgoal using finite_fg by (auto elim:rev_finite_subset)
subgoal using jump_gnz by auto
subgoal by auto
done
moreover have "left {a<..<b} = sum (λx. jumpF h (at_left x)) S"
unfolding left_def S_def L_def
apply (rule sum.mono_neutral_left)
subgoal using finite_fg by (auto elim:rev_finite_subset)
subgoal using jump_gnz by auto
subgoal by auto
done
ultimately have "right {a<..<b} - left {a<..<b}
= sum (λx. jumpF h (at_right x) - jumpF h (at_left x)) S"
by (simp add: sum_subtractf)
also have "... = sum (λx. of_int(jump h x)) S"
proof (rule sum.cong)
fix x assume "x∈S"
define hr where "hr = sgnx h (at_right x)"
define hl where "hl = sgnx h (at_left x)"
have "h sgnx_able (at_left x)" "hr≠0" "h sgnx_able (at_right x)" "hl≠0"
proof -
have "finite {t. h t = 0 ∧ a < t ∧ t < b}"
using finite_fg unfolding h_def by (auto elim!:rev_finite_subset)
moreover have "continuous_on ({a<..<b} - {x. g x = 0 ∧ a < x ∧ x < b}) h"
unfolding h_def using f_cont g_cont
by (auto intro!: continuous_intros elim:continuous_on_subset)
moreover have "finite {x. g x = 0 ∧ a < x ∧ x < b}"
using finite_fg by (auto elim!:rev_finite_subset)
moreover have " x ∈ {a<..<b}"
using ‹x∈S› unfolding S_def by auto
ultimately show "h sgnx_able (at_left x)" "hl≠0" "h sgnx_able (at_right x)" "hr≠0"
using finite_sgnx_at_left_at_right[of h a b "{x. g x=0 ∧ a<x∧x<b}" x]
unfolding hl_def hr_def by blast+
qed
then have "(h has_sgnx hl) (at_left x)" "(h has_sgnx hr) (at_right x)"
unfolding hl_def hr_def using sgnx_able_sgnx by blast+
moreover have "isCont (inverse ∘ h) x"
proof -
have "f x≠0" using ‹x∈S› g_imp_f unfolding S_def by auto
then show ?thesis using f_cont g_cont ‹x∈S› unfolding h_def S_def
by (auto simp add:comp_def intro!:continuous_intros elim:continuous_on_interior)
qed
ultimately show "jumpF h (at_right x) - jumpF h (at_left x) = real_of_int (jump h x)"
using jump_jumpF[of x h] ‹hr≠0› ‹hl≠0› by auto
qed auto
also have "... = cindex a b h"
unfolding cindex_def of_int_sum S_def
apply (rule sum.mono_neutral_cong_right)
using jump_gnz finite_fg by (auto elim:rev_finite_subset)
finally show ?thesis by simp
qed
finally show ?thesis .
qed
subsection ‹Cauchy index along a path›
definition cindex_path::"(real ⇒ complex) ⇒ complex ⇒ int" where
"cindex_path g z = cindex 0 1 (λt. Im (g t - z) / Re (g t - z))"
definition cindex_pathE::"(real ⇒ complex) ⇒ complex ⇒ real" where
"cindex_pathE g z = cindexE 0 1 (λt. Im (g t - z) / Re (g t - z))"
lemma cindex_pathE_point: "cindex_pathE (linepath a a) b = 0"
unfolding cindex_pathE_def by (simp add:cindexE_constI)
lemma cindex_path_reversepath:
"cindex_path (reversepath g) z = - cindex_path g z"
proof -
define f where "f=(λt. Im (g t - z) / Re (g t - z))"
define f' where "f'=(λt. Im (reversepath g t - z) / Re (reversepath g t - z))"
have "f o (λt. 1 - t) = f'"
unfolding f_def f'_def comp_def reversepath_def by auto
then have "cindex 0 1 f' = - cindex 0 1 f"
using cindex_linear_comp[of "-1" 0 1 f 1,simplified] by simp
then show ?thesis
unfolding cindex_path_def
apply (fold f_def f'_def)
by simp
qed
lemma cindex_pathE_reversepath: "cindex_pathE (reversepath g) z = -cindex_pathE g z"
using cindexE_linear_comp[of "-1" 0 1 "λt. (Im (g t) - Im z) / (Re (g t) - Re z)" 1]
by (simp add: cindex_pathE_def reversepath_def o_def)
lemma cindex_pathE_reversepath': "cindex_pathE g z = -cindex_pathE (reversepath g) z"
using cindexE_linear_comp[of "-1" 0 1 "λt. (Im (g t) - Im z) / (Re (g t) - Re z)" 1]
by (simp add: cindex_pathE_def reversepath_def o_def)
lemma cindex_pathE_joinpaths:
assumes g1:"finite_ReZ_segments g1 z" and g2: "finite_ReZ_segments g2 z" and
"path g1" "path g2" "pathfinish g1 = pathstart g2"
shows "cindex_pathE (g1+++g2) z = cindex_pathE g1 z + cindex_pathE g2 z"
proof -
define f where "f = (λg (t::real). Im (g t - z) / Re (g t - z))"
have "cindex_pathE (g1 +++ g2) z = cindexE 0 1 (f (g1+++g2))"
unfolding cindex_pathE_def f_def by auto
also have "... = cindexE 0 (1/2) (f (g1+++g2)) + cindexE (1/2) 1 (f (g1+++g2))"
proof (rule cindexE_combine)
show "finite_jumpFs (f (g1 +++ g2)) 0 1"
unfolding f_def
apply (rule finite_ReZ_segments_imp_jumpFs)
subgoal using finite_ReZ_segments_joinpaths[OF g1 g2] assms(3-5) .
subgoal using path_join_imp[OF ‹path g1› ‹path g2› ‹pathfinish g1=pathstart g2›] .
done
qed auto
also have "... = cindex_pathE g1 z + cindex_pathE g2 z"
proof -
have "cindexE 0 (1/2) (f (g1+++g2)) = cindex_pathE g1 z"
proof -
have "cindexE 0 (1/2) (f (g1+++g2)) = cindexE 0 (1/2) (f g1 o ((*) 2))"
apply (rule cindexE_cong)
unfolding comp_def joinpaths_def f_def by auto
also have "... = cindexE 0 1 (f g1)"
using cindexE_linear_comp[of 2 0 "1/2" _ 0,simplified] by simp
also have "... = cindex_pathE g1 z"
unfolding cindex_pathE_def f_def by auto
finally show ?thesis .
qed
moreover have "cindexE (1/2) 1 (f (g1+++g2)) = cindex_pathE g2 z"
proof -
have "cindexE (1/2) 1 (f (g1+++g2)) = cindexE (1/2) 1 (f g2 o (λx. 2*x - 1))"
apply (rule cindexE_cong)
unfolding comp_def joinpaths_def f_def by auto
also have "... = cindexE 0 1 (f g2)"
using cindexE_linear_comp[of 2 "1/2" 1 _ "-1",simplified] by simp
also have "... = cindex_pathE g2 z"
unfolding cindex_pathE_def f_def by auto
finally show ?thesis .
qed
ultimately show ?thesis by simp
qed
finally show ?thesis .
qed
lemma cindex_pathE_constI:
assumes "⋀t. ⟦0<t;t<1⟧ ⟹ g t=c"
shows "cindex_pathE g z = 0"
unfolding cindex_pathE_def
apply (rule cindexE_constI)
using assms by auto
lemma cindex_pathE_subpath_combine:
assumes g:"finite_ReZ_segments g z"and "path g" and
"0≤a" "a≤b" "b≤c" "c≤1"
shows "cindex_pathE (subpath a b g) z + cindex_pathE (subpath b c g) z
= cindex_pathE (subpath a c g) z"
proof -
define f where "f = (λt. Im (g t - z) / Re (g t - z))"
have ?thesis when "a=b"
proof -
have "cindex_pathE (subpath a b g) z = 0"
apply (rule cindex_pathE_constI)
using that unfolding subpath_def by auto
then show ?thesis using that by auto
qed
moreover have ?thesis when "b=c"
proof -
have "cindex_pathE (subpath b c g) z = 0"
apply (rule cindex_pathE_constI)
using that unfolding subpath_def by auto
then show ?thesis using that by auto
qed
moreover have ?thesis when "a≠b" "b≠c"
proof -
have [simp]:"a<b" "b<c" "a<c"
using that ‹a≤b› ‹b≤c› by auto
have "cindex_pathE (subpath a b g) z = cindexE a b f"
proof -
have "cindex_pathE (subpath a b g) z = cindexE 0 1 (f ∘ (λx. (b - a) * x + a))"
unfolding cindex_pathE_def f_def comp_def subpath_def by auto
also have "... = cindexE a b f"
using cindexE_linear_comp[of "b-a" 0 1 f a,simplified] that(1) by auto
finally show ?thesis .
qed
moreover have "cindex_pathE (subpath b c g) z = cindexE b c f"
proof -
have "cindex_pathE (subpath b c g) z = cindexE 0 1 (f ∘ (λx. (c - b) * x + b))"
unfolding cindex_pathE_def f_def comp_def subpath_def by auto
also have "... = cindexE b c f"
using cindexE_linear_comp[of "c-b" 0 1 f b,simplified] that(2) by auto
finally show ?thesis .
qed
moreover have "cindex_pathE (subpath a c g) z = cindexE a c f"
proof -
have "cindex_pathE (subpath a c g) z = cindexE 0 1 (f ∘ (λx. (c - a) * x + a))"
unfolding cindex_pathE_def f_def comp_def subpath_def by auto
also have "... = cindexE a c f"
using cindexE_linear_comp[of "c-a" 0 1 f a,simplified] ‹a<c› by auto
finally show ?thesis .
qed
moreover have "cindexE a b f + cindexE b c f = cindexE a c f "
proof -
have "finite_jumpFs f a c"
using finite_ReZ_segments_imp_jumpFs[OF g ‹path g›] ‹0≤a› ‹c≤1› unfolding f_def
by (elim finite_jumpFs_subE,auto)
then show ?thesis using cindexE_linear_comp cindexE_combine[OF _ ‹a≤b› ‹b≤c›] by auto
qed
ultimately show ?thesis by auto
qed
ultimately show ?thesis by blast
qed
lemma cindex_pathE_shiftpath:
assumes "finite_ReZ_segments g z" "s∈{0..1}" "path g" and loop:"pathfinish g = pathstart g"
shows "cindex_pathE (shiftpath s g) z = cindex_pathE g z"
proof -
define f where "f=(λg t. Im (g (t::real) - z) / Re (g t - z))"
have "cindex_pathE (shiftpath s g) z = cindexE 0 1 (f (shiftpath s g))"
unfolding cindex_pathE_def f_def by simp
also have "... = cindexE 0 (1-s) (f (shiftpath s g)) + cindexE (1-s) 1 (f (shiftpath s g))"
proof (rule cindexE_combine)
have "finite_ReZ_segments (shiftpath s g) z"
using finite_ReZ_segments_shiftpah[OF assms] .
from finite_ReZ_segments_imp_jumpFs[OF this] path_shiftpath[OF ‹path g› loop ‹s∈{0..1}›]
show "finite_jumpFs (f (shiftpath s g)) 0 1" unfolding f_def by simp
show "0 ≤ 1 - s" "1 - s ≤ 1" using ‹s∈{0..1}› by auto
qed
also have "... = cindexE 0 s (f g) + cindexE s 1 (f g)"
proof -
have "cindexE 0 (1-s) (f (shiftpath s g)) = cindexE s 1 (f g)"
proof -
have "cindexE 0 (1-s) (f (shiftpath s g)) = cindexE 0 (1-s) ((f g) o (λt. t+s))"
apply (rule cindexE_cong)
unfolding shiftpath_def f_def using ‹s∈{0..1}› by (auto simp add:algebra_simps)
also have "...= cindexE s 1 (f g)"
using cindexE_linear_comp[of 1 0 "1-s" "f g" s,simplified] .
finally show ?thesis .
qed
moreover have "cindexE (1 - s) 1 (f (shiftpath s g)) = cindexE 0 s (f g)"
proof -
have "cindexE (1 - s) 1 (f (shiftpath s g)) = cindexE (1-s) 1 ((f g) o (λt. t+s-1))"
apply (rule cindexE_cong)
unfolding shiftpath_def f_def using ‹s∈{0..1}› by (auto simp add:algebra_simps)
also have "... = cindexE 0 s (f g)"
using cindexE_linear_comp[of 1 "1-s" 1 "f g" "s-1",simplified]
by (simp add:algebra_simps)
finally show ?thesis .
qed
ultimately show ?thesis by auto
qed
also have "... = cindexE 0 1 (f g)"
proof (rule cindexE_combine[symmetric])
show "finite_jumpFs (f g) 0 1"
using finite_ReZ_segments_imp_jumpFs[OF assms(1,3)] unfolding f_def by simp
show "0 ≤ s" "s≤1" using ‹s∈{0..1}› by auto
qed
also have "... = cindex_pathE g z"
unfolding cindex_pathE_def f_def by simp
finally show ?thesis .
qed
subsection ‹Cauchy's Index Theorem›
theorem winding_number_cindex_pathE_aux:
fixes g::"real ⇒ complex"
assumes "finite_ReZ_segments g z" and "valid_path g" "z ∉ path_image g" and
Re_ends:"Re (g 1) = Re z" "Re (g 0) = Re z"
shows "2 * Re(winding_number g z) = - cindex_pathE g z"
using assms
proof (induct rule:finite_ReZ_segments_induct)
case (sub0 g z)
have "winding_number (subpath 0 0 g) z = 0"
using ‹z ∉ path_image (subpath 0 0 g)› unfolding subpath_refl
by (auto intro!: winding_number_trivial)
moreover have "cindex_pathE (subpath 0 0 g) z = 0"
unfolding subpath_def by (auto intro:cindex_pathE_constI)
ultimately show ?case by auto
next
case (subEq s g z)
have Re_winding_0:"Re(winding_number h z) = 0"
when Re_const:"∀t∈{0..1}. Re (h t) = Re z" and "valid_path h" "z∉path_image h" for h
proof -
have "Re (winding_number (λt. h t - z) 0) = (Im (Ln (pathfinish (λt. h t - z)))
- Im (Ln (pathstart (λt. h t - z)))) / (2 * pi)"
apply (rule Re_winding_number_half_right[of _ 0,simplified])
using Re_const ‹valid_path h› ‹z ∉ path_image h›
apply auto
by (metis (no_types, opaque_lifting) add.commute imageE le_add_same_cancel1 order_refl
path_image_def plus_complex.simps(1))
moreover have "Im (Ln (h 1 - z)) = Im (Ln (h 0 - z))"
proof -
define z0 where "z0 = h 0 - z"
define z1 where "z1 = h 1 - z"
have [simp]: "z0≠0" "z1≠0" "Re z0=0" "Re z1=0"
using ‹z ∉ path_image h› that(1) unfolding z1_def z0_def path_image_def by auto
have ?thesis when [simp]: "Im z0>0" "Im z1>0"
apply (fold z1_def z0_def)
using Im_Ln_eq_pi_half[of z1] Im_Ln_eq_pi_half[of z0] by auto
moreover have ?thesis when [simp]: "Im z0<0" "Im z1<0"
apply (fold z1_def z0_def)
using Im_Ln_eq_pi_half[of z1] Im_Ln_eq_pi_half[of z0] by auto
moreover have False when "Im z0≥0" "Im z1≤0"
proof -
define f where "f=(λt. Im (h t - z))"
have "∃x≥0. x ≤ 1 ∧ f x = 0"
apply (rule IVT2'[of f 1 0 0])
using that valid_path_imp_path[OF ‹valid_path h›]
unfolding f_def z0_def z1_def path_def
by (auto intro:continuous_intros)
then show False using Re_const ‹z ∉ path_image h› unfolding f_def
by (metis atLeastAtMost_iff complex_surj image_eqI minus_complex.simps(2)
path_defs(4) right_minus_eq)
qed
moreover have False when "Im z0≤0" "Im z1≥0"
proof -
define f where "f=(λt. Im (h t - z))"
have "∃x≥0. x ≤ 1 ∧ f x = 0"
apply (rule IVT')
using that valid_path_imp_path[OF ‹valid_path h›]
unfolding f_def z0_def z1_def path_def
by (auto intro:continuous_intros)
then show False using Re_const ‹z ∉ path_image h› unfolding f_def
by (metis atLeastAtMost_iff complex_surj image_eqI minus_complex.simps(2)
path_defs(4) right_minus_eq)
qed
ultimately show ?thesis by argo
qed
ultimately have "Re (winding_number (λt. h t - z) 0) = 0"
unfolding pathfinish_def pathstart_def by auto
then show ?thesis using winding_number_offset by auto
qed
have ?case when "s = 0"
proof -
have *: "∀t∈{0..1}. Re (g t) = Re z"
using ‹∀t∈{s<..<1}. Re (g t) = Re z› ‹Re (g 1) = Re z› ‹Re (g 0) = Re z› ‹s=0›
by force
have "Re(winding_number g z) = 0"
by (rule Re_winding_0[OF * ‹valid_path g› ‹z ∉ path_image g›])
moreover have "cindex_pathE g z = 0"
unfolding cindex_pathE_def
apply (rule cindexE_constI)
using * by auto
ultimately show ?thesis by auto
qed
moreover have ?case when "s≠0"
proof -
define g1 where "g1 = subpath 0 s g"
define g2 where "g2 = subpath s 1 g"
have "path g" "s>0"
using valid_path_imp_path[OF ‹valid_path g›] that ‹s∈{0..<1}› by auto
have "2 * Re (winding_number g z) = 2*Re (winding_number g1 z) + 2*Re (winding_number g2 z)"
apply (subst winding_number_subpath_combine[OF ‹path g› ‹z∉path_image g›,of 0 s 1
,simplified,symmetric])
using ‹s∈{0..<1}› unfolding g1_def g2_def by auto
also have "... = - cindex_pathE g1 z - cindex_pathE g2 z"
proof -
have "2*Re (winding_number g1 z) = - cindex_pathE g1 z"
unfolding g1_def
apply (rule subEq.hyps(5))
subgoal using subEq.hyps(1) subEq.prems(1) valid_path_subpath by fastforce
subgoal by (meson Path_Connected.path_image_subpath_subset atLeastAtMost_iff
atLeastLessThan_iff less_eq_real_def subEq(7) subEq.hyps(1) subEq.prems(1)
subsetCE valid_path_imp_path zero_le_one)
subgoal by (metis Groups.add_ac(2) add_0_left diff_zero mult.right_neutral subEq(2)
subEq(9) subpath_def)
subgoal by (simp add: subEq.prems(4) subpath_def)
done
moreover have "2*Re (winding_number g2 z) = - cindex_pathE g2 z"
proof -
have *: "∀t∈{0..1}. Re (g2 t) = Re z"
proof
fix t::real assume "t∈{0..1}"
have "Re (g2 t) = Re z" when "t=0 ∨ t=1"
using that unfolding g2_def
by (metis ‹s ≠ 0› add.left_neutral diff_add_cancel mult.commute mult.left_neutral
mult_zero_left subEq.hyps(2) subEq.prems(3) subpath_def)
moreover have "Re (g2 t) = Re z" when "t∈{0<..<1}"
proof -
define t' where "t'=(1 - s) * t + s"
then have "t'∈{s<..<1}"
using that ‹s∈{0..<1}› unfolding t'_def
apply auto
by (sos "((((A<0 * (A<1 * A<2)) * R<1) + ((A<=1 * (A<0 * R<1)) * (R<1 * [1]^2))))")
then have "Re (g t') = Re z"
using ‹∀t∈{s<..<1}. Re (g t) = Re z› by auto
then show ?thesis
unfolding g2_def subpath_def t'_def .
qed
ultimately show "Re (g2 t) = Re z" using ‹t∈{0..1}› by fastforce
qed
have "Re(winding_number g2 z) = 0"
apply (rule Re_winding_0[OF *])
subgoal using g2_def subEq.hyps(1) subEq.prems(1) valid_path_subpath by fastforce
subgoal by (metis (no_types, opaque_lifting) Path_Connected.path_image_subpath_subset
atLeastAtMost_iff atLeastLessThan_iff g2_def less_eq_real_def subEq.hyps(1)
subEq.prems(1) subEq.prems(2) subsetCE valid_path_imp_path zero_le_one)
done
moreover have "cindex_pathE g2 z = 0"
unfolding cindex_pathE_def
apply (rule cindexE_constI)
using * by auto
ultimately show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
also have "... = - cindex_pathE g z"
proof -
have "finite_ReZ_segments g z"
unfolding finite_ReZ_segments_def
apply (rule finite_Psegments.insertI_1[of s])
subgoal using ‹s ∈ {0..<1}› by auto
subgoal using ‹s = 0 ∨ Re (g s) = Re z› by auto
subgoal using ‹∀t∈{s<..<1}. Re (g t) = Re z› by auto
subgoal
proof -
have "finite_Psegments (λt. Re (g (s * t)) = Re z) 0 1"
using ‹finite_ReZ_segments (subpath 0 s g) z›
unfolding subpath_def finite_ReZ_segments_def by auto
from finite_Psegments_pos_linear[of _ "1/s" 0 0 s,simplified,OF this]
show "finite_Psegments (λt. Re (g t - z) = 0) 0 s"
using ‹s>0› unfolding comp_def by auto
qed
done
then show ?thesis
using cindex_pathE_subpath_combine[OF _ ‹path g›,of z 0 s 1,folded g1_def g2_def,simplified]
‹s∈{0..<1}› by auto
qed
finally show ?thesis .
qed
ultimately show ?case by auto
next
case (subNEq s g z)
have Re_winding:"2*Re(winding_number h z) = jumpF_pathfinish h z - jumpF_pathstart h z"
when Re_neq:"∀t∈{0<..<1}. Re (h t) ≠ Re z" and "Re (h 0) = Re z" "Re (h 1) = Re z"
and "valid_path h" "z∉path_image h" for h
proof -
have Re_winding_pos:
"2*Re(winding_number h0 0) = jumpF_pathfinish h0 0 - jumpF_pathstart h0 0"
when Re_gt:"∀t∈{0<..<1}. Re (h0 t) > 0" and "Re (h0 0) = 0" "Re (h0 1) = 0"
and "valid_path h0" "0∉path_image h0" for h0
proof -
define f where "f ≡ (λ(t::real). Im(h0 t) / Re (h0 t))"
define ln0 where "ln0 = Im (Ln (h0 0)) / pi"
define ln1 where "ln1 = Im (Ln (h0 1)) / pi"
have "path h0" using ‹valid_path h0› valid_path_imp_path by auto
have "h0 0≠0" "h0 1≠0"
using path_defs(4) that(5) by fastforce+
have "ln1 = jumpF_pathfinish h0 0"
proof -
have sgnx_at_left:"((λx. Re (h0 x)) has_sgnx 1) (at_left 1)"
unfolding has_sgnx_def eventually_at_left using ‹∀p∈{0<..<1}. Re (h0 p) > 0›
by (intro exI[where x=0],auto)
have cont:"continuous (at_left 1) (λt. Im (h0 t))"
"continuous (at_left 1) (λt. Re (h0 t))"
using ‹path h0› unfolding path_def
by (auto intro:continuous_on_at_left[of 0 1] continuous_intros)
have ?thesis when "Im (h0 1) > 0"
proof -
have "ln1 = 1/2"
using Im_Ln_eq_pi_half[OF ‹h0 1≠0›] that ‹Re (h0 1) = 0› unfolding ln1_def by auto
moreover have "jumpF_pathfinish h0 0 = 1/2"
proof -
have "filterlim f at_top (at_left 1)" unfolding f_def
apply (subst filterlim_divide_at_bot_at_top_iff[of _ " Im (h0 1)"])
using ‹Re(h0 1) = 0› sgnx_at_left cont that unfolding continuous_within by auto
then show ?thesis unfolding jumpF_pathfinish_def jumpF_def f_def by auto
qed
ultimately show ?thesis by auto
qed
moreover have ?thesis when "Im (h0 1) < 0"
proof -
have "ln1 = - 1/2"
using Im_Ln_eq_pi_half[OF ‹h0 1≠0›] that ‹Re (h0 1) = 0› unfolding ln1_def by auto
moreover have "jumpF_pathfinish h0 0 = - 1/2"
proof -
have "((λx. Re (h0 x)) has_sgnx - sgn (Im (h0 1))) (at_left 1)"
using sgnx_at_left that by auto
then have "filterlim f at_bot (at_left 1)"
unfolding f_def using cont that
apply (subst filterlim_divide_at_bot_at_top_iff[of _ " Im (h0 1)"])
unfolding continuous_within using ‹Re(h0 1) = 0› by auto
then show ?thesis unfolding jumpF_pathfinish_def jumpF_def f_def by auto
qed
ultimately show ?thesis by auto
qed
moreover have "Im (h0 1)≠0" using ‹h0 1≠0› ‹Re (h0 1) = 0›
using complex.expand by auto
ultimately show ?thesis by linarith
qed
moreover have "ln0 = jumpF_pathstart h0 0"
proof -
have sgnx_at_right:"((λx. Re (h0 x)) has_sgnx 1) (at_right 0)"
unfolding has_sgnx_def eventually_at_right using ‹∀p∈{0<..<1}. Re (h0 p) > 0›
by (intro exI[where x=1],auto)
have cont:"continuous (at_right 0) (λt. Im (h0 t))"
"continuous (at_right 0) (λt. Re (h0 t))"
using ‹path h0› unfolding path_def
by (auto intro:continuous_on_at_right[of 0 1] continuous_intros)
have ?thesis when "Im (h0 0) > 0"
proof -
have "ln0 = 1/2"
using Im_Ln_eq_pi_half[OF ‹h0 0≠0›] that ‹Re (h0 0) = 0› unfolding ln0_def by auto
moreover have "jumpF_pathstart h0 0 = 1/2"
proof -
have "filterlim f at_top (at_right 0)" unfolding f_def
apply (subst filterlim_divide_at_bot_at_top_iff[of _ " Im (h0 0)"])
using ‹Re(h0 0) = 0› sgnx_at_right cont that unfolding continuous_within by auto
then show ?thesis unfolding jumpF_pathstart_def jumpF_def f_def by auto
qed
ultimately show ?thesis by auto
qed
moreover have ?thesis when "Im (h0 0) < 0"
proof -
have "ln0 = - 1/2"
using Im_Ln_eq_pi_half[OF ‹h0 0≠0›] that ‹Re (h0 0) = 0› unfolding ln0_def by auto
moreover have "jumpF_pathstart h0 0 = - 1/2"
proof -
have "filterlim f at_bot (at_right 0)" unfolding f_def
apply (subst filterlim_divide_at_bot_at_top_iff[of _ " Im (h0 0)"])
using ‹Re(h0 0) = 0› sgnx_at_right cont that unfolding continuous_within by auto
then show ?thesis unfolding jumpF_pathstart_def jumpF_def f_def by auto
qed
ultimately show ?thesis by auto
qed
moreover have "Im (h0 0)≠0" using ‹h0 0≠0› ‹Re (h0 0) = 0›
using complex.expand by auto
ultimately show ?thesis by linarith
qed
moreover have "2*Re(winding_number h0 0) = ln1 - ln0"
proof -
have "∀p∈path_image h0. 0 ≤ Re p"
proof
fix p assume "p ∈ path_image h0"
then obtain t where t:"t∈{0..1}" "p = h0 t" unfolding path_image_def by auto
have "0 ≤ Re p" when "t=0 ∨ t=1"
using that t ‹Re (h0 0) = 0› ‹Re (h0 1) = 0› by auto
moreover have "0 ≤ Re p" when "t∈{0<..<1}"
using that t Re_gt[rule_format, of t] by fastforce
ultimately show "0 ≤ Re p" using t(1) by fastforce
qed
from Re_winding_number_half_right[of _ 0,simplified,OF this ‹valid_path h0› ‹0 ∉ path_image h0›]
show ?thesis unfolding ln1_def ln0_def pathfinish_def pathstart_def
by (auto simp add:field_simps)
qed
ultimately show ?thesis by auto
qed
have ?thesis when "∀t∈{0<..<1}. Re (h t) < Re z"
proof -
let ?hu= "λt. z - h t"
have "2*Re(winding_number ?hu 0) = jumpF_pathfinish ?hu 0 - jumpF_pathstart ?hu 0"
apply(rule Re_winding_pos)
subgoal using that by auto
subgoal using ‹Re (h 0) = Re z› by auto
subgoal using ‹Re (h 1) = Re z› by auto
subgoal using ‹valid_path h› valid_path_offset valid_path_uminus_comp
unfolding comp_def by fastforce
subgoal using ‹z∉path_image h› by (simp add: image_iff path_defs(4))
done
moreover have "winding_number ?hu 0 = winding_number h z"
using winding_number_offset[of h z]
winding_number_uminus_comp[of "λt. h t- z" 0,unfolded comp_def,simplified]
‹valid_path h› ‹z∉path_image h› by auto
moreover have "jumpF_pathfinish ?hu 0 = jumpF_pathfinish h z"
unfolding jumpF_pathfinish_def
apply (auto intro!:jumpF_cong eventuallyI)
by (auto simp add:divide_simps algebra_simps)
moreover have "jumpF_pathstart ?hu 0 = jumpF_pathstart h z"
unfolding jumpF_pathstart_def
apply (auto intro!:jumpF_cong eventuallyI)
by (auto simp add:divide_simps algebra_simps)
ultimately show ?thesis by auto
qed
moreover have ?thesis when "∀t∈{0<..<1}. Re (h t) > Re z"
proof -
let ?hu= "λt. h t - z"
have "2*Re(winding_number ?hu 0) = jumpF_pathfinish ?hu 0 - jumpF_pathstart ?hu 0"
apply(rule Re_winding_pos)
subgoal using that by auto
subgoal using ‹Re (h 0) = Re z› by auto
subgoal using ‹Re (h 1) = Re z› by auto
subgoal using ‹valid_path h› valid_path_offset valid_path_uminus_comp
unfolding comp_def by fastforce
subgoal using ‹z∉path_image h› by simp
done
moreover have "winding_number ?hu 0 = winding_number h z"
using winding_number_offset[of h z] ‹valid_path h› ‹z∉path_image h› by auto
moreover have "jumpF_pathfinish ?hu 0 = jumpF_pathfinish h z"
unfolding jumpF_pathfinish_def by auto
moreover have "jumpF_pathstart ?hu 0 = jumpF_pathstart h z"
unfolding jumpF_pathstart_def by auto
ultimately show ?thesis by auto
qed
moreover have "(∀t∈{0<..<1}. Re (h t) > Re z) ∨ (∀t∈{0<..<1}. Re (h t) < Re z)"
proof (rule ccontr)
assume " ¬ ((∀t∈{0<..<1}. Re z < Re (h t)) ∨ (∀t∈{0<..<1}. Re (h t) < Re z))"
then obtain t1 t2 where t:"t1∈{0<..<1}" "t2∈{0<..<1}" "Re (h t1)≤Re z" "Re (h t2)≥Re z"
unfolding path_image_def by auto
have False when "t1≤t2"
proof -
have "continuous_on {t1..t2} (λt. Re (h t))"
using valid_path_imp_path[OF ‹valid_path h›] t unfolding path_def
by (metis (full_types) atLeastatMost_subset_iff continuous_on_Re continuous_on_subset
eucl_less_le_not_le greaterThanLessThan_iff)
then obtain t' where t':"t'≥t1" "t'≤t2" "Re (h t') = Re z"
using IVT'[of "λt. Re (h t)" t1 _ t2] t ‹t1≤t2› by auto
then have "t'∈{0<..<1}" using t by auto
then have "Re (h t') ≠ Re z" using Re_neq by auto
then show False using ‹Re (h t') = Re z› by simp
qed
moreover have False when "t1≥t2"
proof -
have "continuous_on {t2..t1} (λt. Re (h t))"
using valid_path_imp_path[OF ‹valid_path h›] t unfolding path_def
by (metis (full_types) atLeastatMost_subset_iff continuous_on_Re continuous_on_subset
eucl_less_le_not_le greaterThanLessThan_iff)
then obtain t' where t':"t'≤t1" "t'≥t2" "Re (h t') = Re z"
using IVT2'[of "λt. Re (h t)" t1 _ t2] t ‹t1≥t2› by auto
then have "t'∈{0<..<1}" using t by auto
then have "Re (h t') ≠ Re z" using Re_neq by auto
then show False using ‹Re (h t') = Re z› by simp
qed
ultimately show False by linarith
qed
ultimately show ?thesis by blast
qed
have index_ends:"cindex_pathE h z = jumpF_pathstart h z - jumpF_pathfinish h z"
when Re_neq:"∀t∈{0<..<1}. Re (h t) ≠ Re z" and "valid_path h" for h
proof -
define f where "f = (λt. Im (h t - z) / Re (h t - z))"
define Ri where "Ri = {x. jumpF f (at_right x) ≠ 0 ∧ 0 ≤ x ∧ x < 1}"
define Le where "Le = {x. jumpF f (at_left x) ≠ 0 ∧ 0 < x ∧ x ≤ 1}"
have "path h" using ‹valid_path h› valid_path_imp_path by auto
have jumpF_eq0: "jumpF f (at_left x) = 0" "jumpF f (at_right x) = 0" when "x∈{0<..<1}" for x
proof -
have "Re (h x) ≠ Re z"
using ‹∀t∈{0<..<1}. Re (h t) ≠ Re z› that by blast
then have "isCont f x"
unfolding f_def using continuous_on_interior[OF ‹path h›[unfolded path_def]] that
by (auto intro!: continuous_intros isCont_Im isCont_Re)
then show "jumpF f (at_left x) = 0" "jumpF f (at_right x) = 0"
unfolding continuous_at_split by (auto intro: jumpF_not_infinity)
qed
have "cindex_pathE h z = cindexE 0 1 f"
unfolding cindex_pathE_def f_def by simp
also have "... = sum (λx. jumpF f (at_right x)) Ri - sum (λx. jumpF f (at_left x)) Le"
unfolding cindexE_def Ri_def Le_def by auto
also have "... = jumpF f (at_right 0) - jumpF f (at_left 1)"
proof -
have "sum (λx. jumpF f (at_right x)) Ri = jumpF f (at_right 0)"
proof (cases "jumpF f (at_right 0) = 0")
case True
hence False if "x ∈ Ri" for x using that
by (cases "x = 0") (auto simp: jumpF_eq0 Ri_def)
hence "Ri = {}" by blast
then show ?thesis using True by auto
next
case False
hence "x ∈ Ri ⟷ x = 0" for x using that
by (cases "x = 0") (auto simp: jumpF_eq0 Ri_def)
hence "Ri = {0}" by blast
then show ?thesis by auto
qed
moreover have "sum (λx. jumpF f (at_left x)) Le = jumpF f (at_left 1)"
proof (cases "jumpF f (at_left 1) = 0")
case True
then have "Le = {}"
unfolding Le_def using jumpF_eq0(1) greaterThanLessThan_iff by fastforce
then show ?thesis using True by auto
next
case False
then have "Le = {1}"
unfolding Le_def using jumpF_eq0(1) greaterThanLessThan_iff by fastforce
then show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
also have "... = jumpF_pathstart h z - jumpF_pathfinish h z"
unfolding jumpF_pathstart_def jumpF_pathfinish_def f_def by simp
finally show ?thesis .
qed
have ?case when "s=0"
proof -
have "2 * Re (winding_number g z) = jumpF_pathfinish g z - jumpF_pathstart g z"
apply (rule Re_winding)
using subNEq that by auto
moreover have "cindex_pathE g z = jumpF_pathstart g z - jumpF_pathfinish g z"
apply (rule index_ends)
using subNEq that by auto
ultimately show ?thesis by auto
qed
moreover have ?case when "s≠0"
proof -
define g1 where "g1 = subpath 0 s g"
define g2 where "g2 = subpath s 1 g"
have "path g" "s>0"
using valid_path_imp_path[OF ‹valid_path g›] that ‹s∈{0..<1}› by auto
have "2 * Re (winding_number g z) = 2*Re (winding_number g1 z) + 2*Re (winding_number g2 z)"
apply (subst winding_number_subpath_combine[OF ‹path g› ‹z∉path_image g›,of 0 s 1
,simplified,symmetric])
using ‹s∈{0..<1}› unfolding g1_def g2_def by auto
also have "... = - cindex_pathE g1 z - cindex_pathE g2 z"
proof -
have "2*Re (winding_number g1 z) = - cindex_pathE g1 z"
unfolding g1_def
apply (rule subNEq.hyps(5))
subgoal using subNEq.hyps(1) subNEq.prems(1) valid_path_subpath by fastforce
subgoal by (meson Path_Connected.path_image_subpath_subset atLeastAtMost_iff
atLeastLessThan_iff less_eq_real_def subNEq(7) subNEq.hyps(1) subNEq.prems(1)
subsetCE valid_path_imp_path zero_le_one)
subgoal by (metis Groups.add_ac(2) add_0_left diff_zero mult.right_neutral subNEq(2)
subNEq(9) subpath_def)
subgoal by (simp add: subNEq.prems(4) subpath_def)
done
moreover have "2*Re (winding_number g2 z) = - cindex_pathE g2 z"
proof -
have *:"∀t∈{0<..<1}. Re (g2 t) ≠ Re z"
proof
fix t::real assume "t ∈ {0<..<1}"
define t' where "t'=(1 - s) * t + s"
have "t'∈{s<..<1}" unfolding t'_def using ‹s∈{0..<1}› ‹t ∈ {0<..<1}›
apply (auto simp add:algebra_simps)
by (sos "((((A<0 * (A<1 * A<2)) * R<1) + ((A<=1 * (A<1 * R<1)) * (R<1 * [1]^2))))")
then have "Re (g t') ≠ Re z" using ‹∀t∈{s<..<1}. Re (g t) ≠ Re z› by auto
then show "Re (g2 t) ≠ Re z" unfolding g2_def subpath_def t'_def by auto
qed
have "2*Re (winding_number g2 z) = jumpF_pathfinish g2 z - jumpF_pathstart g2 z"
apply (rule Re_winding[OF *])
subgoal by (metis add.commute add.right_neutral g2_def mult_zero_right subNEq.hyps(2)
subpath_def that)
subgoal by (simp add: ‹g2 ≡ subpath s 1 g› subNEq.prems(3) subpath_def)
subgoal using g2_def subNEq.hyps(1) subNEq.prems(1) valid_path_subpath by fastforce
subgoal by (metis (no_types, opaque_lifting) Path_Connected.path_image_subpath_subset
‹path g› atLeastAtMost_iff atLeastLessThan_iff g2_def less_eq_real_def subNEq.hyps(1)
subNEq.prems(2) subsetCE zero_le_one)
done
moreover have "cindex_pathE g2 z = jumpF_pathstart g2 z - jumpF_pathfinish g2 z"
apply (rule index_ends[OF *])
using g2_def subNEq.hyps(1) subNEq.prems(1) valid_path_subpath by fastforce
ultimately show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
also have "... = - cindex_pathE g z"
proof -
have "finite_ReZ_segments g z"
unfolding finite_ReZ_segments_def
apply (rule finite_Psegments.insertI_2[of s])
subgoal using ‹s ∈ {0..<1}› by auto
subgoal using ‹s = 0 ∨ Re (g s) = Re z› by auto
subgoal using ‹∀t∈{s<..<1}. Re (g t) ≠ Re z› by auto
subgoal
proof -
have "finite_Psegments (λt. Re (g (s * t)) = Re z) 0 1"
using ‹finite_ReZ_segments (subpath 0 s g) z›
unfolding subpath_def finite_ReZ_segments_def by auto
from finite_Psegments_pos_linear[of _ "1/s" 0 0 s,simplified,OF this]
show "finite_Psegments (λt. Re (g t - z) = 0) 0 s"
using ‹s>0› unfolding comp_def by auto
qed
done
then show ?thesis
using cindex_pathE_subpath_combine[OF _ ‹path g›,of z 0 s 1,folded g1_def g2_def,simplified]
‹s∈{0..<1}› by auto
qed
finally show ?thesis .
qed
ultimately show ?case by auto
qed
theorem winding_number_cindex_pathE:
fixes g::"real ⇒ complex"
assumes "finite_ReZ_segments g z" and "valid_path g" "z ∉ path_image g" and
loop: "pathfinish g = pathstart g"
shows "winding_number g z = - cindex_pathE g z / 2"
proof (rule finite_ReZ_segment_cases[OF assms(1)])
fix s assume "s ∈ {0..<1}" "s = 0 ∨ Re (g s) = Re z"
and const:"∀t∈{s<..<1}. Re (g t) = Re z"
and finite:"finite_ReZ_segments (subpath 0 s g) z"
have "Re (g 1) = Re z"
apply(rule continuous_constant_on_closure[of "{s<..<1}" "λt. Re(g t)"])
subgoal using valid_path_imp_path[OF ‹valid_path g›,unfolded path_def] ‹s∈{0..<1}›
by (auto intro!:continuous_intros continuous_Re elim:continuous_on_subset)
subgoal using const by auto
subgoal using ‹s∈{0..<1}› by auto
done
moreover then have "Re (g 0) = Re z" using loop unfolding path_defs by auto
ultimately have "2 * Re (winding_number g z) = - cindex_pathE g z"
using winding_number_cindex_pathE_aux[of g z] assms(1-3) by auto
moreover have "winding_number g z ∈ ℤ"
using integer_winding_number[OF _ loop ‹z∉path_image g›] valid_path_imp_path[OF ‹valid_path g›]
by auto
ultimately show "winding_number g z = - cindex_pathE g z / 2"
by (metis add.right_neutral complex_eq complex_is_Int_iff mult_zero_right
nonzero_mult_div_cancel_left of_real_0 zero_neq_numeral)
next
fix s assume "s ∈ {0..<1}" "s = 0 ∨ Re (g s) = Re z"
and Re_neq:"∀t∈{s<..<1}. Re (g t) ≠ Re z"
and finite:"finite_ReZ_segments (subpath 0 s g) z"
have "path g" using ‹valid_path g› valid_path_imp_path by auto
let ?goal = "2 * Re (winding_number g z) = - cindex_pathE g z"
have ?goal when "s=0"
proof -
have index_ends:"cindex_pathE h z = jumpF_pathstart h z - jumpF_pathfinish h z"
when Re_neq:"∀t∈{0<..<1}. Re (h t) ≠ Re z" and "valid_path h" for h
proof -
define f where "f = (λt. Im (h t - z) / Re (h t - z))"
define Ri where "Ri = {x. jumpF f (at_right x) ≠ 0 ∧ 0 ≤ x ∧ x < 1}"
define Le where "Le = {x. jumpF f (at_left x) ≠ 0 ∧ 0 < x ∧ x ≤ 1}"
have "path h" using ‹valid_path h› valid_path_imp_path by auto
have jumpF_eq0: "jumpF f (at_left x) = 0" "jumpF f (at_right x) = 0" when "x∈{0<..<1}" for x
proof -
have "Re (h x) ≠ Re z"
using ‹∀t∈{0<..<1}. Re (h t) ≠ Re z› that by blast
then have "isCont f x"
unfolding f_def using continuous_on_interior[OF ‹path h›[unfolded path_def]] that
by (auto intro!: continuous_intros isCont_Im isCont_Re)
then show "jumpF f (at_left x) = 0" "jumpF f (at_right x) = 0"
unfolding continuous_at_split by (auto intro: jumpF_not_infinity)
qed
have "cindex_pathE h z = cindexE 0 1 f"
unfolding cindex_pathE_def f_def by simp
also have "... = sum (λx. jumpF f (at_right x)) Ri - sum (λx. jumpF f (at_left x)) Le"
unfolding cindexE_def Ri_def Le_def by auto
also have "... = jumpF f (at_right 0) - jumpF f (at_left 1)"
proof -
have "sum (λx. jumpF f (at_right x)) Ri = jumpF f (at_right 0)"
proof (cases "jumpF f (at_right 0) = 0")
case True
hence False if "x ∈ Ri" for x using that
by (cases "x = 0") (auto simp: jumpF_eq0 Ri_def)
hence "Ri = {}" by blast
then show ?thesis using True by auto
next
case False
hence "x ∈ Ri ⟷ x = 0" for x using that
by (cases "x = 0") (auto simp: jumpF_eq0 Ri_def)
then have "Ri = {0}" by blast
then show ?thesis by auto
qed
moreover have "sum (λx. jumpF f (at_left x)) Le = jumpF f (at_left 1)"
proof (cases "jumpF f (at_left 1) = 0")
case True
then have "Le = {}"
unfolding Le_def using jumpF_eq0(1) greaterThanLessThan_iff by fastforce
then show ?thesis using True by auto
next
case False
then have "Le = {1}"
unfolding Le_def using jumpF_eq0(1) greaterThanLessThan_iff by fastforce
then show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
also have "... = jumpF_pathstart h z - jumpF_pathfinish h z"
unfolding jumpF_pathstart_def jumpF_pathfinish_def f_def by simp
finally show ?thesis .
qed
define fI where "fI=(λt. Im (g t - z))"
define fR where "fR=(λt. Re (g t - z))"
have fI: "(fI ⤏ fI 0) (at_right 0)" "(fI ⤏ fI 1) (at_left 1)"
proof -
have "continuous (at_right 0) fI"
apply (rule continuous_on_at_right[of _ 1])
using ‹path g› unfolding fI_def path_def by (auto intro:continuous_intros)
then show "(fI ⤏ fI 0) (at_right 0)" by (simp add: continuous_within)
next
have "continuous (at_left 1) fI"
apply (rule continuous_on_at_left[of 0])
using ‹path g› unfolding fI_def path_def by (auto intro:continuous_intros)
then show "(fI ⤏ fI 1) (at_left 1)" by (simp add: continuous_within)
qed
have fR: "(fR ⤏ 0) (at_right 0)" "(fR ⤏ 0) (at_left 1)" when "Re (g 0) = Re z"
proof -
have "continuous (at_right 0) fR"
apply (rule continuous_on_at_right[of _ 1])
using ‹path g› unfolding fR_def path_def by (auto intro:continuous_intros)
then show "(fR ⤏ 0) (at_right 0)" using that unfolding fR_def by (simp add: continuous_within)
next
have "continuous (at_left 1) fR"
apply (rule continuous_on_at_left[of 0])
using ‹path g› unfolding fR_def path_def by (auto intro:continuous_intros)
then show "(fR ⤏ 0) (at_left 1)"
using that loop unfolding fR_def path_defs by (simp add: continuous_within)
qed
have "(∀t∈{0<..<1}. Re (g t) > Re z) ∨ (∀t∈{0<..<1}. Re (g t) < Re z)"
proof (rule ccontr)
assume " ¬ ((∀t∈{0<..<1}. Re z < Re (g t)) ∨ (∀t∈{0<..<1}. Re (g t) < Re z))"
then obtain t1 t2 where t:"t1∈{0<..<1}" "t2∈{0<..<1}" "Re (g t1)≤Re z" "Re (g t2)≥Re z"
unfolding path_image_def by auto
have False when "t1≤t2"
proof -
have "continuous_on {t1..t2} (λt. Re (g t))"
using valid_path_imp_path[OF ‹valid_path g›] t unfolding path_def
by (metis (full_types) atLeastatMost_subset_iff continuous_on_Re continuous_on_subset
eucl_less_le_not_le greaterThanLessThan_iff)
then obtain t' where t':"t'≥t1" "t'≤t2" "Re (g t') = Re z"
using IVT'[of "λt. Re (g t)" t1 _ t2] t ‹t1≤t2› by auto
then have "t'∈{0<..<1}" using t by auto
then have "Re (g t') ≠ Re z" using Re_neq ‹s=0› by auto
then show False using ‹Re (g t') = Re z› by simp
qed
moreover have False when "t1≥t2"
proof -
have "continuous_on {t2..t1} (λt. Re (g t))"
using valid_path_imp_path[OF ‹valid_path g›] t unfolding path_def
by (metis (full_types) atLeastatMost_subset_iff continuous_on_Re continuous_on_subset
eucl_less_le_not_le greaterThanLessThan_iff)
then obtain t' where t':"t'≤t1" "t'≥t2" "Re (g t') = Re z"
using IVT2'[of "λt. Re (g t)" t1 _ t2] t ‹t1≥t2› by auto
then have "t'∈{0<..<1}" using t by auto
then have "Re (g t') ≠ Re z" using Re_neq ‹s=0› by auto
then show False using ‹Re (g t') = Re z› by simp
qed
ultimately show False by linarith
qed
moreover have ?thesis when Re_pos:"∀t∈{0<..<1}. Re (g t) > Re z"
proof -
have "Re (winding_number g z) = 0"
proof -
have "∀p∈path_image g. Re z ≤ Re p"
proof
fix p assume "p ∈ path_image g"
then obtain t where "0≤t" "t≤1" "p = g t" unfolding path_image_def by auto
have "Re z ≤ Re (g t)"
apply (rule continuous_ge_on_closure[of "{0<..<1}" "λt. Re (g t)" t "Re z",simplified])
subgoal using valid_path_imp_path[OF ‹valid_path g›,unfolded path_def]
by (auto intro:continuous_intros)
subgoal using ‹0≤t› ‹t≤1› by auto
subgoal for x using that[rule_format,of x] by auto
done
then show "Re z ≤ Re p" using ‹p = g t› by auto
qed
from Re_winding_number_half_right[OF this ‹valid_path g› ‹z∉path_image g›] loop
show ?thesis by auto
qed
moreover have "cindex_pathE g z = 0"
proof -
have "cindex_pathE g z = jumpF_pathstart g z - jumpF_pathfinish g z"
using index_ends[OF _ ‹valid_path g›] Re_neq ‹s=0› by auto
moreover have "jumpF_pathstart g z = jumpF_pathfinish g z" when "Re (g 0) ≠ Re z"
proof -
have "jumpF_pathstart g z = 0"
using jumpF_pathstart_eq_0[OF ‹path g›] that unfolding path_defs by auto
moreover have "jumpF_pathfinish g z=0"
using jumpF_pathfinish_eq_0[OF ‹path g›] that loop unfolding path_defs by auto
ultimately show ?thesis by auto
qed
moreover have "jumpF_pathstart g z = jumpF_pathfinish g z" when "Re (g 0) = Re z"
proof -
have [simp]:"(fR has_sgnx 1) (at_right 0)"
unfolding fR_def has_sgnx_def eventually_at_right
apply (rule exI[where x=1])
using Re_pos by auto
have [simp]:"(fR has_sgnx 1) (at_left 1)"
unfolding fR_def has_sgnx_def eventually_at_left
apply (rule exI[where x=0])
using Re_pos by auto
have "fI 0≠0"
proof (rule ccontr)
assume "¬ fI 0 ≠ 0"
then have "g 0 =z" using ‹Re (g 0) = Re z›
unfolding fI_def by (simp add: complex.expand)
then show False using ‹z ∉ path_image g› unfolding path_image_def by auto
qed
moreover have ?thesis when "fI 0>0"
proof -
have "jumpF_pathstart g z = 1/2"
proof -
have "(LIM x at_right 0. fI x / fR x :> at_top)"
apply (subst filterlim_divide_at_bot_at_top_iff[of _ "fI 0"])
using that fI fR[OF ‹Re (g 0) = Re z›] by simp_all
then show ?thesis unfolding jumpF_pathstart_def fI_def fR_def jumpF_def by auto
qed
moreover have "jumpF_pathfinish g z = 1/2"
proof -
have "fI 1>0" using loop that unfolding path_defs fI_def by auto
then have "(LIM x at_left 1. fI x / fR x :> at_top)"
apply (subst filterlim_divide_at_bot_at_top_iff[of _ "fI 1"])
using that fI fR[OF ‹Re (g 0) = Re z›] by simp_all
then show ?thesis unfolding jumpF_pathfinish_def fI_def fR_def jumpF_def by auto
qed
ultimately show ?thesis by simp
qed
moreover have ?thesis when "fI 0<0"
proof -
have "jumpF_pathstart g z = - 1/2"
proof -
have "(LIM x at_right 0. fI x / fR x :> at_bot)"
apply (subst filterlim_divide_at_bot_at_top_iff[of _ "fI 0"])
using that fI fR[OF ‹Re (g 0) = Re z›] by simp_all
then show ?thesis unfolding jumpF_pathstart_def fI_def fR_def jumpF_def by auto
qed
moreover have "jumpF_pathfinish g z = - 1/2"
proof -
have "fI 1<0" using loop that unfolding path_defs fI_def by auto
then have "(LIM x at_left 1. fI x / fR x :> at_bot)"
apply (subst filterlim_divide_at_bot_at_top_iff[of _ "fI 1"])
using that fI fR[OF ‹Re (g 0) = Re z›] by simp_all
then show ?thesis unfolding jumpF_pathfinish_def fI_def fR_def jumpF_def by auto
qed
ultimately show ?thesis by simp
qed
ultimately show ?thesis by linarith
qed
ultimately show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
moreover have ?thesis when Re_neg:"∀t∈{0<..<1}. Re (g t) < Re z"
proof -
have "Re (winding_number g z) = 0"
proof -
have "∀p∈path_image g. Re z ≥ Re p"
proof
fix p assume "p ∈ path_image g"
then obtain t where "0≤t" "t≤1" "p = g t" unfolding path_image_def by auto
have "Re z ≥ Re (g t)"
apply (rule continuous_le_on_closure[of "{0<..<1}" "λt. Re (g t)" t "Re z",simplified])
subgoal using valid_path_imp_path[OF ‹valid_path g›,unfolded path_def]
by (auto intro:continuous_intros)
subgoal using ‹0≤t› ‹t≤1› by auto
subgoal for x using that[rule_format,of x] by auto
done
then show "Re z ≥ Re p" using ‹p = g t› by auto
qed
from Re_winding_number_half_left[OF this ‹valid_path g› ‹z∉path_image g›] loop
show ?thesis by auto
qed
moreover have "cindex_pathE g z = 0"
proof -
have "cindex_pathE g z = jumpF_pathstart g z - jumpF_pathfinish g z"
using index_ends[OF _ ‹valid_path g›] Re_neq ‹s=0› by auto
moreover have "jumpF_pathstart g z = jumpF_pathfinish g z" when "Re (g 0) ≠ Re z"
proof -
have "jumpF_pathstart g z = 0"
using jumpF_pathstart_eq_0[OF ‹path g›] that unfolding path_defs by auto
moreover have "jumpF_pathfinish g z=0"
using jumpF_pathfinish_eq_0[OF ‹path g›] that loop unfolding path_defs by auto
ultimately show ?thesis by auto
qed
moreover have "jumpF_pathstart g z = jumpF_pathfinish g z" when "Re (g 0) = Re z"
proof -
have [simp]:"(fR has_sgnx - 1) (at_right 0)"
unfolding fR_def has_sgnx_def eventually_at_right
apply (rule exI[where x=1])
using Re_neg by auto
have [simp]:"(fR has_sgnx - 1) (at_left 1)"
unfolding fR_def has_sgnx_def eventually_at_left
apply (rule exI[where x=0])
using Re_neg by auto
have "fI 0≠0"
proof (rule ccontr)
assume "¬ fI 0 ≠ 0"
then have "g 0 =z" using ‹Re (g 0) = Re z›
unfolding fI_def by (simp add: complex.expand)
then show False using ‹z ∉ path_image g› unfolding path_image_def by auto
qed
moreover have ?thesis when "fI 0>0"
proof -
have "jumpF_pathstart g z = - 1/2"
proof -
have "(LIM x at_right 0. fI x / fR x :> at_bot)"
apply (subst filterlim_divide_at_bot_at_top_iff[of _ "fI 0"])
using that fI fR[OF ‹Re (g 0) = Re z›] by simp_all
then show ?thesis unfolding jumpF_pathstart_def fI_def fR_def jumpF_def by auto
qed
moreover have "jumpF_pathfinish g z = - 1/2"
proof -
have "fI 1>0" using loop that unfolding path_defs fI_def by auto
then have "(LIM x at_left 1. fI x / fR x :> at_bot)"
apply (subst filterlim_divide_at_bot_at_top_iff[of _ "fI 1"])
using that fI fR[OF ‹Re (g 0) = Re z›] by simp_all
then show ?thesis unfolding jumpF_pathfinish_def fI_def fR_def jumpF_def by auto
qed
ultimately show ?thesis by simp
qed
moreover have ?thesis when "fI 0<0"
proof -
have "jumpF_pathstart g z = 1/2"
proof -
have "(LIM x at_right 0. fI x / fR x :> at_top)"
apply (subst filterlim_divide_at_bot_at_top_iff[of _ "fI 0"])
using that fI fR[OF ‹Re (g 0) = Re z›] by simp_all
then show ?thesis unfolding jumpF_pathstart_def fI_def fR_def jumpF_def by auto
qed
moreover have "jumpF_pathfinish g z = 1/2"
proof -
have "fI 1<0" using loop that unfolding path_defs fI_def by auto
then have "(LIM x at_left 1. fI x / fR x :> at_top)"
apply (subst filterlim_divide_at_bot_at_top_iff[of _ "fI 1"])
using that fI fR[OF ‹Re (g 0) = Re z›] by simp_all
then show ?thesis unfolding jumpF_pathfinish_def fI_def fR_def jumpF_def by auto
qed
ultimately show ?thesis by simp
qed
ultimately show ?thesis by linarith
qed
ultimately show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
moreover have ?goal when "s≠0"
proof -
have "Re (g s) = Re z" using ‹s = 0 ∨ Re (g s) = Re z› that by auto
define g' where "g' = shiftpath s g"
have "2 * Re (winding_number g' z) = - cindex_pathE g' z"
proof (rule winding_number_cindex_pathE_aux)
show "Re (g' 1) = Re z" "Re (g' 0) = Re z"
using ‹Re (g s) = Re z› ‹s∈{0..<1}› ‹s≠0›
unfolding g'_def shiftpath_def by simp_all
show "valid_path g'"
using valid_path_shiftpath[OF ‹valid_path g› loop,of s,folded g'_def] ‹s∈{0..<1}›
by auto
show "z ∉ path_image g'"
using ‹s ∈ {0..<1}› assms(3) g'_def loop path_image_shiftpath by fastforce
show "finite_ReZ_segments g' z"
using finite_ReZ_segments_shiftpah[OF ‹finite_ReZ_segments g z› _ ‹path g› loop] ‹s∈{0..<1}›
unfolding g'_def by auto
qed
moreover have "winding_number g' z = winding_number g z"
unfolding g'_def
apply (rule winding_number_shiftpath[OF ‹path g› ‹z ∉ path_image g› loop])
using ‹s∈{0..<1}› by auto
moreover have "cindex_pathE g' z = cindex_pathE g z"
unfolding g'_def
apply (rule cindex_pathE_shiftpath[OF ‹finite_ReZ_segments g z› _ ‹path g› loop])
using ‹s∈{0..<1}› by auto
ultimately show ?thesis by auto
qed
ultimately have ?goal by auto
moreover have "winding_number g z ∈ ℤ"
using integer_winding_number[OF _ loop ‹z∉path_image g›] valid_path_imp_path[OF ‹valid_path g›]
by auto
ultimately show "winding_number g z = - cindex_pathE g z / 2"
by (metis add.right_neutral complex_eq complex_is_Int_iff mult_zero_right
nonzero_mult_div_cancel_left of_real_0 zero_neq_numeral)
qed
text ‹REMARK: The usual statement of Cauchy's Index theorem (i.e. Analytic Theory of Polynomials
(2002): Theorem 11.1.3) is about the equality between the number of polynomial roots and
the Cauchy index, which is the joint application of @{thm winding_number_cindex_pathE} and
@{thm argument_principle}.›
end