# HG changeset patch # User paulson # Date 1744834413 -3600 # Node ID 819688d4cc45a741107aa920aa496784bec210ae # Parent 2886a76359f3af38543855ea74b7bb429e450056# Parent 1b17f0a41aa3b84e305a3a11b2db0dcbf9922f8a merged diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Analysis/Change_Of_Vars.thy --- a/src/HOL/Analysis/Change_Of_Vars.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Analysis/Change_Of_Vars.thy Wed Apr 16 21:13:33 2025 +0100 @@ -3425,4 +3425,23 @@ using measurable_differentiable_image_eq [OF S der_f inj] assms has_measure_differentiable_image by blast +lemma has_absolute_integral_reflect_real: + fixes f :: "real \ real" + assumes "uminus ` A \ B" "uminus ` B \ A" "A \ sets lebesgue" + shows "(\x. f (-x)) absolutely_integrable_on A \ integral A (\x. f (-x)) = b \ + f absolutely_integrable_on B \ integral B f = b" +proof - + have bij: "bij_betw uminus A B" + by (rule bij_betwI[of _ _ _ uminus]) (use assms(1,2) in auto) + have "((\x. \-1\ *\<^sub>R f (-x)) absolutely_integrable_on A \ + integral A (\x. \-1\ *\<^sub>R f (-x)) = b) \ + (f absolutely_integrable_on uminus ` A \ + integral (uminus ` A) f = b)" using assms + by (intro has_absolute_integral_change_of_variables_1') (auto intro!: derivative_eq_intros) + also have "uminus ` A = B" + using bij by (simp add: bij_betw_def) + finally show ?thesis + by simp +qed + end diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Analysis/Complex_Transcendental.thy --- a/src/HOL/Analysis/Complex_Transcendental.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Wed Apr 16 21:13:33 2025 +0100 @@ -1107,6 +1107,7 @@ using assms mpi_less_Im_Ln [of "exp z"] Im_Ln_le_pi [of "exp z"] by auto qed auto + subsection\<^marker>\tag unimportant\\Relation to Real Logarithm\ lemma Ln_of_real: @@ -2014,6 +2015,12 @@ lemma Arg_eq_0: "Arg z = 0 \ z \ \ \ 0 \ Re z" using Arg_def Im_Ln_eq_0 complex_eq_iff complex_is_Real_iff by auto +lemma Arg_neg_iff: "Arg x < 0 \ Im x < 0" + using Arg_less_0 linorder_not_le by blast + +lemma Arg_pos_iff: "Arg x > 0 \ Im x > 0 \ (Im x = 0 \ Re x < 0)" + by (metis Arg_eq_pi Arg_le_pi Arg_lt_pi order_less_le pi_gt_zero) + corollary\<^marker>\tag unimportant\ Arg_ne_0: assumes "z \ \\<^sub>\\<^sub>0" shows "Arg z \ 0" using assms by (auto simp: nonneg_Reals_def Arg_eq_0) @@ -2065,6 +2072,11 @@ lemma Ln_Arg: "z\0 \ Ln(z) = ln(norm z) + \ * Arg(z)" by (metis Arg_def Re_Ln complex_eq) +lemma Ln_of_real': + assumes "x \ 0" + shows "Ln (of_real x) = of_real (ln \x\) + (if x < 0 then pi else 0) * \" + by (subst Ln_Arg) (use assms in auto) + lemma continuous_at_Arg: assumes "z \ \\<^sub>\\<^sub>0" shows "continuous (at z) Arg" @@ -2079,6 +2091,20 @@ lemma continuous_within_Arg: "z \ \\<^sub>\\<^sub>0 \ continuous (at z within S) Arg" using continuous_at_Arg continuous_at_imp_continuous_within by blast + +lemma continuous_on_Arg: "continuous_on (-\\<^sub>\\<^sub>0) Arg" + using continuous_at_Arg by (simp add: continuous_at_imp_continuous_on) + +lemma continuous_on_Arg' [continuous_intros]: + assumes "continuous_on A f" "\z. z \ A \ f z \ \\<^sub>\\<^sub>0" + shows "continuous_on A (\x. Arg (f x))" + by (rule continuous_on_compose2[OF continuous_on_Arg assms(1)]) (use assms(2) in auto) + +lemma tendsto_Arg [tendsto_intros]: + assumes "(f \ z) F" "z \ \\<^sub>\\<^sub>0" + shows "((\x. Arg (f x)) \ Arg z) F" + by (rule isCont_tendsto_compose[OF continuous_at_Arg]) (use assms in auto) + lemma Arg_Re_pos: "\Arg z\ < pi / 2 \ Re z > 0 \ z = 0" using Arg_def Re_Ln_pos_lt by auto @@ -2089,6 +2115,37 @@ assumes "Arg z + Arg w \ {-pi<..pi}" "z \ 0" "w \ 0" shows "Arg (z * w) = Arg z + Arg w" using Arg_eq_Im_Ln Ln_times_simple assms by auto + +lemma Arg_unique': "r > 0 \ \ \ {-pi<..pi} \ x = rcis r \ \ Arg x = \" + by (rule Arg_unique[of r]) (auto simp: rcis_def cis_conv_exp) + +lemma Arg_times': + assumes "w \ 0" "z \ 0" + defines "x \ Arg w + Arg z" + shows "Arg (w * z) = x + (if x \ {-pi<..pi} then 0 else if x > pi then -2*pi else 2*pi)" +proof (rule Arg_unique'[of "norm w * norm z"]) + show "w * z = rcis (cmod w * cmod z) + (x + (if x \ {- pi<..pi} then 0 else if x > pi then -2*pi else 2*pi))" + by (subst (1 3) rcis_cmod_Arg [symmetric]) + (use assms in \auto simp: rcis_def simp flip: cis_mult cis_divide cis_inverse\) + show "x + (if x \ {- pi<..pi} then 0 else if pi < x then - 2 * pi else 2 * pi) \ {- pi<..pi}" + using Arg_bounded[of w] Arg_bounded[of z] by (auto simp: x_def) +qed (use assms in auto) + +lemma Arg_divide': + assumes [simp]: "z \ 0" "w \ 0" + shows "Arg (z / w) = Arg z - Arg w + + (if Arg z - Arg w > pi then -2 * pi else if Arg z - Arg w \ -pi then 2 * pi else 0)" + (is "_ = ?rhs") +proof - + have "Arg (z * inverse w) = ?rhs" + by (subst Arg_times') + (use Arg_bounded[of w] Arg_bounded[of z] + in \auto simp: Arg_inverse elim!: Reals_cases split: if_splits\)+ + also have "z * inverse w = z / w" + by (simp add: field_simps) + finally show ?thesis . +qed subsection\The Unwinding Number and the Ln product Formula\ @@ -2860,6 +2917,31 @@ by simp qed +lemma csqrt_in_nonpos_Reals_iff [simp]: "csqrt z \ \\<^sub>\\<^sub>0 \ z = 0" +proof + assume "csqrt z \ \\<^sub>\\<^sub>0" + hence "csqrt z = 0" + unfolding complex_eq_iff using csqrt_principal[of z] + by (auto simp: complex_nonpos_Reals_iff sgn_if simp del: csqrt.sel split: if_splits) + thus "z = 0" + by simp +qed auto + +lemma Im_csqrt_eq_0_iff: "Im (csqrt z) = 0 \ z \ \\<^sub>\\<^sub>0" +proof + assume *: "Im (csqrt z) = 0" + define x where "x = Re (csqrt z)" + have "z = csqrt z ^ 2" + by simp + also have "csqrt z = of_real x" + by (simp add: complex_eq_iff x_def * del: csqrt.sel) + also have "\ ^ 2 = of_real (x ^ 2)" + by simp + also have "\ \ \\<^sub>\\<^sub>0" + unfolding nonneg_Reals_of_real_iff by auto + finally show "z \ \\<^sub>\\<^sub>0" . +qed (auto elim!: nonneg_Reals_cases) + lemma csqrt_conv_powr: "csqrt z = z powr (1/2)" by (auto simp: csqrt_exp_Ln powr_def) @@ -3965,4 +4047,618 @@ apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler) done + +subsection \Normalisation of angles\ + +text \ + The following operation normalises an angle $\varphi$, i.e.\ returns the unique + $\psi$ in the range $(-\pi, \pi]$ such that + $\varphi\equiv\psi\hskip.5em(\text{mod}\ 2\pi)$. + This is the same convention used by the \<^const>\Arg\ function. +\ +definition normalize_angle :: "real \ real" where + "normalize_angle x = x - \x / (2 * pi) - 1 / 2\ * (2 * pi)" + +lemma normalize_angle_id [simp]: + assumes "x \ {-pi<..pi}" + shows "normalize_angle x = x" +proof - + have "-1 < x / (2 * pi) - 1 / 2" "x / (2 * pi) - 1 / 2 \ 0" + using assms pi_gt3 by (auto simp: field_simps) + hence "ceiling (x / (2 * pi) - 1 / 2) = 0" + by linarith + thus ?thesis + by (simp add: normalize_angle_def) +qed + +lemma normalize_angle_normalized: "normalize_angle x \ {-pi<..pi}" +proof - + have "-1 < x / (2 * pi) - 1 / 2 - ceiling (x / (2 * pi) - 1 / 2)" + by linarith + moreover have "x / (2 * pi) - 1 / 2 - ceiling (x / (2 * pi) - 1 / 2) \ 0" + by linarith + ultimately show ?thesis + using pi_gt3 by (auto simp: field_simps normalize_angle_def) +qed + +lemma cis_normalize_angle [simp]: "cis (normalize_angle x) = cis x" +proof - + have "cis (normalize_angle x) = cis x / cis (real_of_int \x / (2 * pi) - 1 / 2\ * (2 * pi))" + by (simp add: normalize_angle_def flip: cis_divide) + also have "real_of_int \x / (2 * pi) - 1 / 2\ * (2 * pi) = + 2 * pi * real_of_int \x / (2 * pi) - 1 / 2\" + by (simp add: algebra_simps) + also have "cis \ = 1" + by (rule cis_multiple_2pi) auto + finally show ?thesis + by simp +qed + +lemma rcis_normalize_angle [simp]: "rcis r (normalize_angle x) = rcis r x" + by (simp add: rcis_def) + +lemma normalize_angle_lbound [intro]: "normalize_angle x > -pi" + and normalize_angle_ubound [intro]: "normalize_angle x \ pi" + using normalize_angle_normalized[of x] by auto + +lemma normalize_angle_idem [simp]: "normalize_angle (normalize_angle x) = normalize_angle x" + by (rule normalize_angle_id) (use normalize_angle_normalized[of x] in auto) + +lemma Arg_rcis': "r > 0 \ Arg (rcis r \) = normalize_angle \" + by (rule Arg_unique'[of r]) auto + + +subsection \Convexity of circular sectors in the complex plane\ + +text \ + In this section we will show that if we have two non-zero points $w$ and $z$ in the complex plane + whose arguments differ by less than $\pi$, then the argument of any point on the line connecting + $w$ and $z$ lies between the arguments of $w$ and $z$. Moreover, the norm of any such point is + no greater than the norms of $w$ and $z$. + + Geometrically, this means that if we have a sector around the origin with a central angle + less than $\pi$ (minus the origin itself) then that region is convex. +\ + +lemma Arg_closed_segment_aux1: + assumes "x \ 0" "y \ 0" "Re x > 0" "Re x = Re y" + assumes "z \ closed_segment x y" + shows "Arg z \ closed_segment (Arg x) (Arg y)" + using assms +proof (induction "Arg x" "Arg y" arbitrary: x y rule: linorder_wlog) + case (le x y) + from le have "Re z = Re x" "Im z \ closed_segment (Im x) (Im y)" + by (auto simp: closed_segment_same_Re) + then obtain t where t: "t \ {0..1}" "Im z = linepath (Im x) (Im y) t" + by (metis image_iff linepath_image_01) + have *: "Im x \ Im y" + using le by (auto simp: arg_conv_arctan arctan_le_iff field_simps) + have "Im x / Re x \ linepath (Im x) (Im y) t / Re x" + using le t * by (intro divide_right_mono linepath_real_ge_left) auto + hence "Arg x \ Arg z" + using t le \Re z = Re x\ by (auto simp: arg_conv_arctan arctan_le_iff) + moreover have "Im y / Re x \ linepath (Im x) (Im y) t / Re x" + using le t * by (intro divide_right_mono linepath_real_le_right) auto + hence "Arg y \ Arg z" + using t le \Re z = Re x\ by (auto simp: arg_conv_arctan arctan_le_iff) + ultimately show ?case + using le by (auto simp: closed_segment_same_Re closed_segment_eq_real_ivl) +next + case (sym x y) + have "Arg z \ closed_segment (Arg y) (Arg x)" + by (rule sym(1)) + (use sym(2-) in \simp_all add: dist_commute closed_segment_commute\) + thus ?case + by (simp add: closed_segment_commute) +qed + +lemma Arg_closed_segment_aux1': + fixes r1 r2 \1 \2 :: real + defines "x \ rcis r1 \1" and "y \ rcis r2 \2" + assumes "z \ closed_segment x y" + assumes "r1 > 0" "r2 > 0" "Re x = Re y" "Re x \ 0" "Re x = 0 \ Im x * Im y > 0" + assumes "dist \1 \2 < pi" + obtains r \ where "r \ {0<..max r1 r2}" "\ \ closed_segment \1 \2" "z = rcis r \" +proof (cases "Re x = 0") + case True + have [simp]: "cos \1 = 0" "cos \2 = 0" + using assms True by auto + have "sin \1 = 1 \ sin \2 = 1 \ sin \1 = -1 \ sin \2 = -1" + using sin_cos_squared_add[of \1] sin_cos_squared_add[of \2] assms + by (auto simp: zero_less_mult_iff power2_eq_1_iff) + thus ?thesis + proof (elim disjE conjE) + assume [simp]: "sin \1 = 1" "sin \2 = 1" + have xy_eq: "x = of_real r1 * \" "y = of_real r2 * \" + by (auto simp: complex_eq_iff x_def y_def) + hence z: "Re z = 0" "Im z \ closed_segment r1 r2" + using \z \ closed_segment x y \ by (auto simp: xy_eq closed_segment_same_Re) + have "closed_segment r1 r2 \ {0<..max r1 r2}" + by (rule closed_segment_subset) (use assms in auto) + with z have "Im z \ {0<..max r1 r2}" + by blast + show ?thesis + by (rule that[of "Im z" \1]) + (use z \Im z \ {0<..max r1 r2}\ in \auto simp: complex_eq_iff\) + next + assume [simp]: "sin \1 = -1" "sin \2 = -1" + have xy_eq: "x = -of_real r1 * \" "y = -of_real r2 * \" + by (auto simp: complex_eq_iff x_def y_def) + hence z: "Re z = 0" "Im z \ closed_segment (-r1) (-r2)" + using \z \ closed_segment x y \ by (auto simp: xy_eq closed_segment_same_Re) + have "closed_segment (-r1) (-r2) \ {-max r1 r2..<0}" + by (rule closed_segment_subset) (use assms in auto) + with z have "-Im z \ {0<..max r1 r2}" + by auto + show ?thesis + by (rule that[of "-Im z" \1]) + (use z \-Im z \ {0<..max r1 r2}\ in \auto simp: complex_eq_iff\) + qed +next + case False + hence Re_pos: "Re x > 0" + using \Re x \ 0\ by linarith + define n :: int where "n = \\1 / (2 * pi) - 1 / 2\" + define n' :: int where "n' = \\2 / (2 * pi) - 1 / 2\" + + have "Re z = Re x" + using assms by (auto simp: closed_segment_same_Re) + + have Arg_z: "Arg z \ closed_segment (Arg x) (Arg y)" + by (rule Arg_closed_segment_aux1) (use assms Re_pos in \simp_all add: dist_norm\) + + have "z \ closed_segment x y" + by fact + also have "\ \ cball 0 (max r1 r2)" + using _ _ convex_cball by (rule closed_segment_subset) (use assms in auto) + finally have "norm z \ max r1 r2" + by auto + moreover have "z \ 0" + by (intro notI) (use \Re x > 0\ \Re z = Re x\ in auto) + ultimately have norm_z: "norm z \ {0<..max r1 r2}" + by simp + + have Arg_x: "Arg x = \1 - 2 * pi * of_int n" + using assms by (simp add: x_def Arg_rcis' normalize_angle_def n_def) + have Arg_y: "Arg y = \2 - 2 * pi * of_int n'" + using assms by (simp add: x_def Arg_rcis' normalize_angle_def n'_def) + have Arg_bounds: "\Arg x\ \ pi/2" "\Arg y\ \ pi/2" + by (subst Arg_Re_nonneg; use assms in simp)+ + + have "pi * of_int (2 * \n - n'\ - 1) = 2 * pi * of_int (\n - n'\) - pi" + by (simp add: algebra_simps) + also have "\ = \2 * pi * of_int (n - n')\ - pi / 2 - pi / 2" + by (simp add: abs_mult) + also have "\ \ \2 * pi * of_int (n - n') + Arg x - Arg y\" + using Arg_bounds pi_gt_zero by linarith + also have "\ \ dist \1 \2" + using Arg_x Arg_y unfolding dist_norm real_norm_def by (simp add: algebra_simps) + also have "\ < pi * 1" + using assms by simp + finally have "2 * \n - n'\ - 1 < 1" + by (subst (asm) mult_less_cancel_left_pos) auto + hence [simp]: "n' = n" + by presburger + + show ?thesis + using norm_z + proof (rule that[of "norm z" "Arg z + 2 * pi * of_int n"]) + have "2 * pi * of_int n + Arg z \ ((+) (2 * pi * of_int n)) ` closed_segment (Arg x) (Arg y)" + using Arg_z by blast + also have "\ = closed_segment (2 * pi * real_of_int n + Arg x) (2 * pi * real_of_int n + Arg y)" + by (rule closed_segment_translation [symmetric]) + also have "2 * pi * real_of_int n + Arg x = \1" + by (simp add: Arg_x) + also have "2 * pi * real_of_int n + Arg y = \2" + by (simp add: Arg_y) + finally show "Arg z + 2 * pi * real_of_int n \ closed_segment \1 \2" + by (simp add: add_ac) + next + have "z = rcis (norm z) (Arg z)" + by (simp add: rcis_cmod_Arg) + also have "\ = rcis (cmod z) (Arg z + 2 * pi * real_of_int n)" + by (simp add: rcis_def flip: cis_mult) + finally show "z = \" . + qed +qed + +lemma Arg_closed_segment': + fixes r1 r2 \1 \2 :: real + defines "x \ rcis r1 \1" and "y \ rcis r2 \2" + assumes "r1 > 0" "r2 > 0" "dist \1 \2 < pi" "z \ closed_segment x y" + obtains r \ where "r \ {0<..max r1 r2}" "\ \ closed_segment \1 \2" "z = rcis r \" +proof - + define u_aux :: real where + "u_aux = (if Im x = Im y then pi/2 else arctan (Re (x-y) / Im (x-y)))" + define u :: real where + "u = (if Re (x * cis u_aux) < 0 then if u_aux \ 0 then u_aux + pi else u_aux - pi else u_aux)" + + have "u_aux \ {-pi/2<..pi/2}" + using arctan_lbound[of "Re (x-y) / Im (x-y)"] arctan_ubound[of "Re (x-y) / Im (x-y)"] + by (auto simp: u_aux_def) + have u_bounds: "u \ {-pi<..pi}" + using \u_aux \ _\ by (auto simp: u_def) + + have u_aux: "(Re x - Re y) * cos u_aux = (Im x - Im y) * sin u_aux" + proof (cases "Im x = Im y") + case False + hence "tan u_aux = (Re x - Re y) / (Im x - Im y)" and "cos u_aux \ 0" + by (auto simp: u_aux_def tan_arctan) + thus ?thesis using False + by (simp add: tan_def divide_simps mult_ac split: if_splits) + qed (auto simp: u_aux_def) + hence "Re (x * cis u_aux) = Re (y * cis u_aux)" + by (auto simp: algebra_simps) + hence same_Re: "Re (x * cis u) = Re (y * cis u)" + by (auto simp: u_def) + + have Re_nonneg: "Re (x * cis u) \ 0" + by (auto simp: u_def) + + have "linear (\w. w * cis u)" + by (intro linearI) (auto simp: algebra_simps) + hence "closed_segment (x * cis u) (y * cis u) = (\w. w * cis u) ` closed_segment x y" + by (intro closed_segment_linear_image) + hence z'_in: "z * cis u \ closed_segment (x * cis u) (y * cis u)" + using assms by blast + + obtain r \ where r\: + "r \ {0<..max r1 r2}" "\ \ closed_segment (\1 + u) (\2 + u)" "z * cis u = rcis r \" + proof (rule Arg_closed_segment_aux1'[of "z * cis u" r1 "\1 + u" r2 "\2 + u"]) + show "z * cis u \ closed_segment (rcis r1 (\1 + u)) (rcis r2 (\2 + u))" + using z'_in by (simp add: x_def y_def rcis_def mult.assoc flip: cis_mult) + next + show "r1 > 0" "r2 > 0" + by fact+ + next + show "Re (rcis r1 (\1 + u)) = Re (rcis r2 (\2 + u))" + using same_Re by (simp add: x_def y_def cos_add field_simps) + next + show "Re (rcis r1 (\1 + u)) \ 0" + using \r1 > 0\ Re_nonneg by (auto intro!: mult_nonneg_nonneg simp: cos_add x_def) + next + show "dist (\1 + u) (\2 + u) < pi" + using assms by (simp add: dist_norm) + next + show "Re (rcis r1 (\1 + u)) = 0 \ 0 < Im (rcis r1 (\1 + u)) * Im (rcis r2 (\2 + u))" + proof + assume *: "Re (rcis r1 (\1 + u)) = 0" + hence "cos (\1 + u) = 0" + using assms by simp + then obtain n1 where "\1 + u = real_of_int n1 * pi + pi / 2" + by (subst (asm) cos_zero_iff_int2) auto + hence n1: "\1 = real_of_int n1 * pi + pi / 2 - u" + by linarith + + have "Re (rcis r1 (\1 + u)) = 0" + by fact + also have "rcis r1 (\1 + u) = x * cis u" + by (simp add: x_def rcis_def cis_mult) + also have "Re (x * cis u) = Re (y * cis u)" + by (fact same_Re) + also have "y * cis u = rcis r2 (\2 + u)" + by (simp add: y_def rcis_def cis_mult) + finally have "cos (\2 + u) = 0" + using assms by simp + then obtain n2 where "\2 + u = real_of_int n2 * pi + pi / 2" + by (subst (asm) cos_zero_iff_int2) auto + hence n2: "\2 = real_of_int n2 * pi + pi / 2 - u" + by linarith + + have "pi * real_of_int \n2 - n1\ = \real_of_int (n2 - n1) * pi\" + by (simp add: abs_mult) + also have "\ = dist \1 \2" + by (simp add: n1 n2 dist_norm ring_distribs) + also have "\ < pi * 1" + using \dist \1 \2 < pi\ by simp + finally have "real_of_int \n2 - n1\ < 1" + by (subst (asm) mult_less_cancel_left_pos) auto + hence "n1 = n2" + by linarith + + have "Im (rcis r1 (\1 + u)) * Im (rcis r2 (\2 + u)) = r1 * r2 * cos (real_of_int n2 * pi) ^ 2" + by (simp add: n1 n2 sin_add \n1 = n2\ power2_eq_square) + also have "cos (real_of_int n2 * pi) ^ 2 = (cos (2 * (real_of_int n2 * pi)) + 1) / 2" + by (subst cos_double_cos) auto + also have "2 * (real_of_int n2 * pi) = 2 * pi * real_of_int n2" + by (simp add: mult_ac) + also have "(cos \ + 1) / 2 = 1" + by (subst cos_int_2pin) auto + also have "r1 * r2 * 1 > 0" + using assms by simp + finally show "Im (rcis r1 (\1 + u)) * Im (rcis r2 (\2 + u)) > 0" . + qed + qed + + show ?thesis + proof (rule that[of r "\ - u"]) + show "r \ {0<..max r1 r2}" + by fact + next + have "u + (\ - u) \ closed_segment (\1 + u) (\2 + u)" + using r\ by simp + also have "\ = (+) u ` closed_segment \1 \2" + by (subst (1 2) add.commute, rule closed_segment_translation) + finally show "\ - u \ closed_segment \1 \2" + by (subst (asm) inj_image_mem_iff) auto + next + show "z = rcis r (\ - u)" + using r\ by (simp add: rcis_def field_simps flip: cis_divide) + qed +qed + +lemma Arg_closed_segment: + assumes "x \ 0" "y \ 0" "dist (Arg x) (Arg y) < pi" "z \ closed_segment x y" + shows "Arg z \ closed_segment (Arg x) (Arg y)" +proof - + define r1 \1 where "r1 = norm x" and "\1 = Arg x" + define r2 \2 where "r2 = norm y" and "\2 = Arg y" + note defs = r1_def r2_def \1_def \2_def + obtain r \ where *: "r \ {0<..max r1 r2}" "\ \ closed_segment \1 \2" "z = rcis r \" + by (rule Arg_closed_segment'[of r1 r2 \1 \2 z]) + (use assms in \auto simp: defs rcis_cmod_Arg\) + have "Arg z = \" + proof (rule Arg_unique') + show "z = rcis r \" "r > 0" + using * by auto + next + have "\ \ closed_segment \1 \2" + by (fact *) + also have "\ \ {-pi<..pi}" + by (rule closed_segment_subset) + (use assms * Arg_bounded[of x] Arg_bounded[of y] in \auto simp: defs\) + finally show "\ \ {-pi<..pi}" + by auto + qed + with * show ?thesis + by (simp add: defs) +qed + + +subsection \Complex cones\ + +text \ + We introduce the following notation to describe the set of all complex numbers of the form + $c e^{ix}$ where $c\geq 0$ and $x\in [a, b]$. +\ +definition complex_cone :: "real \ real \ complex set" where + "complex_cone a b = (\(r,a). rcis r a) ` ({0..} \ closed_segment a b)" + +lemma in_complex_cone_iff: "z \ complex_cone a b \ (\x\closed_segment a b. z = rcis (norm z) x)" + by (auto simp: complex_cone_def image_iff) + +lemma zero_in_complex_cone [simp, intro]: "0 \ complex_cone a b" + by (auto simp: in_complex_cone_iff) + +lemma in_complex_cone_iff_Arg: + assumes "a \ {-pi<..pi}" "b \ {-pi<..pi}" + shows "z \ complex_cone a b \ z = 0 \ Arg z \ closed_segment a b" +proof + assume "z \ complex_cone a b" + then obtain r x where *: "x \ closed_segment a b" "z = rcis r x" "r \ 0" + by (auto simp: complex_cone_def) + have "closed_segment a b \ {-pi<..pi}" + by (rule closed_segment_subset) (use assms in auto) + with * have **: "x \ {-pi<..pi}" + by auto + show "z = 0 \ Arg z \ closed_segment a b" + proof (cases "z = 0") + case False + with * have "r \ 0" + by auto + with * have [simp]: "r > 0" + by simp + show ?thesis + by (use * ** in \auto simp: Arg_rcis\) + qed auto +next + assume "z = 0 \ Arg z \ closed_segment a b" + thus "z \ complex_cone a b" + proof + assume *: "Arg z \ closed_segment a b" + have "z = rcis (norm z) (Arg z)" + by (simp_all add: rcis_cmod_Arg) + thus ?thesis using * + unfolding in_complex_cone_iff by blast + qed auto +qed + +lemma complex_cone_rotate: "complex_cone (c + a) (c + b) = (*) (cis c) ` complex_cone a b" +proof - + have *: "(*) (cis c) ` complex_cone a b \ complex_cone (c + a) (c + b)" for c a b + by (auto simp: closed_segment_translation in_complex_cone_iff norm_mult rcis_def simp flip: cis_mult) + + have "complex_cone (c + a) (c + b) = (*) (cis c) ` (*) (cis (-c)) ` complex_cone (c + a) (c + b)" + by (simp add: image_image field_simps flip: cis_inverse) + also have "\ \ (*) (cis c) ` complex_cone ((-c) + (c + a)) ((-c) + (c + b))" + by (intro image_mono *) + also have "\ = (*) (cis c) ` complex_cone a b" + by simp + finally show ?thesis + using *[of c a b] by blast +qed + +lemma complex_cone_subset: + "a \ closed_segment a' b' \ b \ closed_segment a' b' \ complex_cone a b \ complex_cone a' b'" + unfolding complex_cone_def + by (intro image_mono Sigma_mono order.refl, unfold subset_closed_segment) auto + +lemma complex_cone_commute: "complex_cone a b = complex_cone b a" + by (simp add: complex_cone_def closed_segment_commute) + +lemma complex_cone_eq_UNIV: + assumes "dist a b \ 2*pi" + shows "complex_cone a b = UNIV" + using assms +proof (induction a b rule: linorder_wlog) + case (le a b) + have "bij ((*) (cis (a+pi)))" + by (rule bij_betwI[of _ _ _ "(*) (cis (-a-pi))"]) + (auto simp: field_simps simp flip: cis_inverse cis_divide cis_mult) + hence "UNIV = (*) (cis (a+pi)) ` UNIV" + unfolding bij_betw_def by blast + also have "UNIV \ complex_cone (-pi) pi" + proof safe + fix z :: complex + have "z = rcis (norm z) (Arg z)" "norm z \ 0" "Arg z \ closed_segment (-pi) pi" + using Arg_bounded[of z] by (auto simp: closed_segment_eq_real_ivl rcis_cmod_Arg) + thus "z \ complex_cone (-pi) pi" + unfolding in_complex_cone_iff by blast + qed + also have "(*) (cis (a + pi)) ` complex_cone (- pi) pi = complex_cone a (a + 2 * pi)" + using complex_cone_rotate[of "a+pi" "-pi" pi] by (simp add: add_ac) + also have "\ \ complex_cone a b" + by (rule complex_cone_subset) (use le in \auto simp: closed_segment_eq_real_ivl1 dist_norm\) + finally show ?case by blast +qed (simp_all add: complex_cone_commute dist_commute) + + +text \ + A surprisingly tough argument: cones in the complex plane are closed. +\ +lemma closed_complex_cone [continuous_intros, intro]: "closed (complex_cone a b)" +proof (induction a b rule: linorder_wlog) + case (sym a b) + thus ?case + by (simp add: complex_cone_commute) +next + case (le a b) + show ?case + proof (cases "b - a < 2 * pi") + case False + hence "complex_cone a b = UNIV" + by (intro complex_cone_eq_UNIV) (auto simp: dist_norm) + thus ?thesis + by simp + next + case True + define c where "c = (b - a) / 2" + define d where "d = (b + a) / 2" + have ab_eq: "a = d - c" "b = c + d" + by (simp_all add: c_def d_def field_simps) + have "c \ 0" "c < pi" + using True le by (simp_all add: c_def) + + define e where "e = (if c \ pi / 2 then 1 else sin c)" + have "e > 0" + proof (cases "c \ pi / 2") + case False + have "0 < pi / 2" + by simp + also have "pi / 2 < c" + using False by simp + finally have "c > 0" . + moreover have "c < pi" + using True by (simp add: c_def) + ultimately show ?thesis + using False by (auto simp: e_def intro!: sin_gt_zero) + qed (auto simp: e_def) + + define A where "A = -ball 0 1 - {z. Re z < 0} \ ({z. Im z < e} \ {z. Im z > -e})" + + have "closed (A \ (Arg -` {-c..c}))" + proof (intro continuous_closed_preimage) + show "closed A" unfolding A_def + by (intro closed_Diff closed_Compl open_Int open_halfspace_Re_lt + open_halfspace_Im_lt open_halfspace_Im_gt open_ball) + show "continuous_on A Arg" + unfolding A_def using \e > 0\ + by (intro continuous_intros) (auto elim!: nonpos_Reals_cases) + qed auto + + also have "A \ (Arg -` {-c..c}) = + (Arg -` {-c..c} - {z. Re z < 0} \ ({z. Im z < e} \ {z. Im z > -e})) - ball 0 1" + by (auto simp: A_def) + + also have "\ = Arg -` {-c..c} - ball 0 1" + proof (intro equalityI subsetI) + fix z assume z: "z \ Arg -` {-c..c} - ball 0 1" + define r where "r = norm z" + define x where "x = Arg z" + have "\x\ \ c" + using z by (auto simp: x_def) + also note \c < pi\ + finally have "\x\ < pi" . + + have False if *: "Re z < 0" "Im z < e" "Im z > -e" + proof - + have "r \ 1" + using z by (auto simp: r_def) + have z_eq: "z = rcis r x" + by (simp add: r_def x_def rcis_cmod_Arg) + from * and \r \ 1\ have "cos x < 0" + by (simp add: z_eq mult_less_0_iff) + with \\x\ < pi\ have "\x\ > pi / 2" + using cos_ge_zero[of x] by linarith + hence "c > pi / 2" + using \\x\ \ c\ by linarith + + have "sin c \ sin \x\" + proof - + have "sin (pi - c) \ sin (pi - \x\)" + by (rule sin_monotone_2pi_le) + (use \\x\ \ c\ \\x\ < pi\ \\x\ > pi / 2\ \c < pi\ in \auto simp: field_simps\) + thus ?thesis + by simp + qed + also have "sin \x\ \ 1 * \sin x\" + by (auto simp: abs_if) + also have "1 * \sin x\ \ r * \sin x\" + by (rule mult_right_mono) (use \r \ 1\ in auto) + also have "r * \sin x\ = \Im z\" + using \r \ 1\ by (simp add: z_eq abs_mult) + also have "\Im z\ < e" + using * by linarith + finally show False + using \c > pi / 2\ by (auto simp: e_def split: if_splits) + + qed + thus "z \ Arg -` {-c..c} - {z. Re z < 0} \ ({z. Im z < e} \ {z. Im z > -e}) - ball 0 1" + using z by blast + qed auto + + also have "Arg -` {-c..c} - ball 0 1 = complex_cone (-c) c - ball 0 1" + using \c < pi\ \c \ 0\ + by (auto simp: in_complex_cone_iff_Arg closed_segment_eq_real_ivl1) + + finally have "closed (complex_cone (-c) c - ball 0 1)" . + + moreover have "closed (complex_cone (-c) c \ cball 0 1)" + proof - + have "compact ((\(r,x). rcis r x) ` ({0..1} \ closed_segment (-c) c))" + by (intro compact_continuous_image) + (auto intro!: continuous_intros compact_Times simp: case_prod_unfold) + also have "((\(r,x). rcis r x) ` ({0..1} \ closed_segment (-c) c)) = complex_cone (-c) c \ cball 0 1" + by (auto simp: in_complex_cone_iff image_def) + finally show ?thesis + by (rule compact_imp_closed) + qed + + ultimately have "closed (complex_cone (-c) c - ball 0 1 \ complex_cone (-c) c \ cball 0 1)" + by (intro closed_Un) + also have "\ = complex_cone (-c) c" + by auto + finally have "closed (complex_cone (-c) c)" . + + hence "closed ((*) (cis d) ` complex_cone (-c) c)" + by (intro closed_injective_linear_image) auto + also have "\ = complex_cone a b" + using complex_cone_rotate[of d "-c" c] by (simp add: ab_eq add_ac) + finally show ?thesis . + qed +qed + +lemma norm_eq_Re_iff: "norm z = Re z \ z \ \\<^sub>\\<^sub>0" +proof + assume "norm z = Re z" + hence "norm z ^ 2 = Re z ^ 2" + by simp + hence "Im z = 0" + by (auto simp: cmod_def) + moreover have "Re z \ 0" + by (subst \norm z = Re z\ [symmetric]) auto + ultimately show "z \ \\<^sub>\\<^sub>0" + by (auto simp: complex_nonneg_Reals_iff) +qed (auto elim!: nonneg_Reals_cases) + end diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Analysis/Elementary_Metric_Spaces.thy --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Apr 16 21:13:33 2025 +0100 @@ -366,6 +366,12 @@ for x :: "'a::{perfect_space,metric_space}" using islimpt_UNIV [of x] by (simp add: islimpt_approachable) + +lemma pointed_ball_nonempty: + assumes "r > 0" + shows "ball x r - {x :: 'a :: {perfect_space, metric_space}} \ {}" + using perfect_choose_dist[of r x] assms by (auto simp: ball_def dist_commute) + lemma cball_eq_sing: fixes x :: "'a::{metric_space,perfect_space}" shows "cball x e = {x} \ e = 0" diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Analysis/Gamma_Function.thy --- a/src/HOL/Analysis/Gamma_Function.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Analysis/Gamma_Function.thy Wed Apr 16 21:13:33 2025 +0100 @@ -2096,7 +2096,7 @@ } note lim = this from assms double_in_nonpos_Ints_imp[of z] have z': "2 * z \ \\<^sub>\\<^sub>0" by auto - from fraction_not_in_ints[of 2 1] have "(1/2 :: 'a) \ \\<^sub>\\<^sub>0" + from fraction_not_in_Ints[of 2 1] have "(1/2 :: 'a) \ \\<^sub>\\<^sub>0" by (intro not_in_Ints_imp_not_in_nonpos_Ints) simp_all with lim[of "1/2 :: 'a"] have "?h \ 2 * Gamma (1/2 :: 'a)" by (simp add: exp_of_real) from LIMSEQ_unique[OF this lim[OF assms]] z' show ?thesis @@ -2388,18 +2388,22 @@ case True with that have "z = 0 \ z = 1" by (force elim!: Ints_cases) moreover have "g 0 * g (1/2) = Gamma (1/2)^2 * g 0" - using fraction_not_in_ints[where 'a = complex, of 2 1] by (simp add: g_def power2_eq_square) + using fraction_not_in_Ints[where 'a = complex, of 2 1] by (simp add: g_def power2_eq_square) moreover have "g (1/2) * g 1 = Gamma (1/2)^2 * g 1" - using fraction_not_in_ints[where 'a = complex, of 2 1] + using fraction_not_in_Ints[where 'a = complex, of 2 1] by (simp add: g_def power2_eq_square Beta_def algebra_simps) ultimately show ?thesis by force next case False - hence z: "z/2 \ \" "(z+1)/2 \ \" using Ints_diff[of "z+1" 1] by (auto elim!: Ints_cases) + hence z: "z/2 \ \ \ (z+1)/2 \ \" + by (metis Ints_1 Ints_cases Ints_of_int add.commute + add_in_Ints_iff_left divide_eq_eq_numeral1(1) + of_int_mult one_add_one zero_neq_numeral) hence z': "z/2 \ \\<^sub>\\<^sub>0" "(z+1)/2 \ \\<^sub>\\<^sub>0" by (auto elim!: nonpos_Ints_cases) from z have "1-z/2 \ \" "1-((z+1)/2) \ \" using Ints_diff[of 1 "1-z/2"] Ints_diff[of 1 "1-((z+1)/2)"] by auto - hence z'': "1-z/2 \ \\<^sub>\\<^sub>0" "1-((z+1)/2) \ \\<^sub>\\<^sub>0" by (auto elim!: nonpos_Ints_cases) + hence z'': "1-z/2 \ \\<^sub>\\<^sub>0 \ 1-((z+1)/2) \ \\<^sub>\\<^sub>0" + by blast from z have "g (z/2) * g ((z+1)/2) = (Gamma (z/2) * Gamma ((z+1)/2)) * (Gamma (1-z/2) * Gamma (1-((z+1)/2))) * (sin (of_real pi * z/2) * sin (of_real pi * (z+1)/2))" @@ -2453,7 +2457,7 @@ by (subst (1 2) g_eq[symmetric]) simp from DERIV_cmult[OF this, of "inverse ((Gamma (1/2))^2)"] have "(g has_field_derivative (g z * ((h (z/2) + h ((z+1)/2))/2))) (at z)" - using fraction_not_in_ints[where 'a = complex, of 2 1] + using fraction_not_in_Ints[where 'a = complex, of 2 1] by (simp add: divide_simps Gamma_eq_zero_iff not_in_Ints_imp_not_in_nonpos_Ints) moreover have "(g has_field_derivative (g z * h z)) (at z)" using g_g'[of z] by (simp add: ac_simps) @@ -2592,7 +2596,7 @@ lemma Gamma_one_half_real: "Gamma (1/2 :: real) = sqrt pi" proof - - from Gamma_reflection_complex[of "1/2"] fraction_not_in_ints[where 'a = complex, of 2 1] + from Gamma_reflection_complex[of "1/2"] fraction_not_in_Ints[where 'a = complex, of 2 1] have "Gamma (1/2 :: complex)^2 = of_real pi" by (simp add: power2_eq_square) hence "of_real pi = Gamma (complex_of_real (1/2))^2" by simp also have "\ = of_real ((Gamma (1/2))^2)" by (subst Gamma_complex_of_real) simp_all diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Analysis/Homeomorphism.thy --- a/src/HOL/Analysis/Homeomorphism.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Analysis/Homeomorphism.thy Wed Apr 16 21:13:33 2025 +0100 @@ -2259,4 +2259,69 @@ finally show ?thesis . qed +lemma closure_bij_homeomorphic_image_eq: + assumes bij: "bij_betw f A B" + assumes homo: "homeomorphism A B f g" + assumes cont: "continuous_on A' f" "continuous_on B' g" + assumes inv: "\x. x \ B' \ f (g x) = x" + assumes cl: "closed A'" "closed B'" and X: "X \ A" "A \ A'" "B \ B'" + shows "closure (f ` X) = f ` closure X" +proof - + have "f ` X \ f ` A" + using \X \ A\ by blast + also have "f ` A = B" + using \bij_betw f A B\ by (simp add: bij_betw_def) + finally have *: "closure (f ` X) \ closure B" + by (intro closure_mono) + + show ?thesis + proof (rule antisym) + have "g ` closure (f ` X) \ closure (g ` f ` X)" + proof (rule continuous_image_closure_subset[OF _ *]) + have "closure B \ B'" + using X cl by (simp add: closure_minimal) + thus "continuous_on (closure B) g" + by (rule continuous_on_subset[OF cont(2)]) + qed + also have "g ` f ` X = (g \ f) ` X" + by (simp add: image_image) + also have "\ = id ` X" + using homo X by (intro image_cong) (auto simp: homeomorphism_def) + finally have "g ` closure (f ` X) \ closure X" + by simp + hence "f ` g ` closure (f ` X) \ f ` closure X" + by (intro image_mono) + also have "f ` g ` closure (f ` X) = (f \ g) ` closure (f ` X)" + by (simp add: image_image) + also have "\ = id ` closure (f ` X)" + proof (rule image_cong) + fix x assume "x \ closure (f ` X)" + also have "closure (f ` X) \ closure B'" + proof (rule closure_mono) + have "f ` X \ f ` A" + using X by (intro image_mono) auto + also have "\ = B" + using bij by (simp add: bij_betw_def) + also have "\ \ B'" + by fact + finally show "f ` X \ B'" . + qed + finally have "x \ B'" + using cl by simp + thus "(f \ g) x = id x" + by (auto simp: homeomorphism_def inv) + qed auto + finally show "closure (f ` X) \ f ` closure X" + by simp + next + show "f ` closure X \ closure (f ` X)" + proof (rule continuous_image_closure_subset) + show "continuous_on A' f" + by fact + show "closure X \ A'" + using assms by (simp add: closure_minimal) + qed + qed +qed + end diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Analysis/Linear_Algebra.thy --- a/src/HOL/Analysis/Linear_Algebra.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Analysis/Linear_Algebra.thy Wed Apr 16 21:13:33 2025 +0100 @@ -586,6 +586,18 @@ lemma of_real_differentiable [simp,derivative_intros]: "of_real differentiable F" by (simp add: bounded_linear_imp_differentiable bounded_linear_of_real) +lemma bounded_linear_representation: + fixes B :: "'a :: euclidean_space set" + assumes "independent B" "span B = UNIV" + shows "bounded_linear (\v. representation B v b)" +proof - + have "Vector_Spaces.linear (*\<^sub>R) (*) (\v. representation B v b)" + by (rule real_vector.linear_representation) fact+ + then have "linear (\v. representation B v b)" + unfolding linear_def real_scaleR_def [abs_def] . + thus ?thesis + by (simp add: linear_conv_bounded_linear) +qed subsection\<^marker>\tag unimportant\ \We continue\ diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Analysis/Ordered_Euclidean_Space.thy --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Wed Apr 16 21:13:33 2025 +0100 @@ -266,6 +266,11 @@ using convex_box[of a b] by (metis interval_cbox) +lemma bounded_Ico [simp]: "bounded {a..x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} = (if {a .. b} = {} then {} else if 0 \ m then {m *\<^sub>R a .. m *\<^sub>R b} else {m *\<^sub>R b .. m *\<^sub>R a})" using image_smult_cbox[of m a b] diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Analysis/Path_Connected.thy Wed Apr 16 21:13:33 2025 +0100 @@ -1329,6 +1329,33 @@ "(linepath a b has_vector_derivative (b - a)) (at x within S)" by (force intro: derivative_eq_intros simp add: linepath_def has_vector_derivative_def algebra_simps) +lemma linepath_real_ge_left: + fixes x y :: real + assumes "x \ y" "t \ 0" + shows "linepath x y t \ x" +proof - + have "x + 0 \ x + t *\<^sub>R (y - x)" + using assms by (intro add_left_mono) auto + also have "\ = linepath x y t" + by (simp add: linepath_def algebra_simps) + finally show ?thesis by simp +qed + +lemma linepath_real_le_right: + fixes x y :: real + assumes "x \ y" "t \ 1" + shows "linepath x y t \ y" +proof - + have "y + 0 \ y + (1 - t) *\<^sub>R (x - y)" + using assms by (intro add_left_mono) (auto intro: mult_nonneg_nonpos) + also have "y + (1 - t) *\<^sub>R (x - y) = linepath x y t" + by (simp add: linepath_def algebra_simps) + finally show ?thesis by simp +qed + +lemma linepath_translate: "(+) c \ linepath a b = linepath (a + c) (b + c)" + by (auto simp: linepath_def algebra_simps) + subsection\<^marker>\tag unimportant\\Segments via convex hulls\ diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Analysis/Sparse_In.thy --- a/src/HOL/Analysis/Sparse_In.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Analysis/Sparse_In.thy Wed Apr 16 21:13:33 2025 +0100 @@ -71,6 +71,19 @@ using assms unfolding sparse_in_def islimpt_Un by (metis Int_iff open_Int) +lemma sparse_in_union': "A sparse_in C \ B sparse_in C \ A \ B sparse_in C" + using sparse_in_union[of A C B C] by simp + +lemma sparse_in_Union_finite: + assumes "(\A'. A' \ A \ A' sparse_in B)" "finite A" + shows "\A sparse_in B" + using assms(2,1) by (induction rule: finite_induct) (auto intro!: sparse_in_union') + +lemma sparse_in_UN_finite: + assumes "(\x. x \ A \ f x sparse_in B)" "finite A" + shows "(\x\A. f x) sparse_in B" + by (rule sparse_in_Union_finite) (use assms in auto) + lemma sparse_in_compact_finite: assumes "pts sparse_in A" "compact A" shows "finite (A \ pts)" @@ -144,6 +157,44 @@ eventually_at_topological by blast +lemma sparse_in_translate: + fixes A B :: "'a :: real_normed_vector set" + assumes "A sparse_in B" + shows "(+) c ` A sparse_in (+) c ` B" + unfolding sparse_in_def +proof safe + fix x assume "x \ B" + from get_sparse_in_cover[OF assms] obtain B' where B': "open B'" "B \ B'" "\y\B'. \y islimpt A" + by blast + have "c + x \ (+) c ` B'" "open ((+) c ` B')" + using B' \x \ B\ by (auto intro: open_translation) + moreover have "\y\(+) c ` B'. \y islimpt ((+) c ` A)" + proof safe + fix y assume y: "y \ B'" "c + y islimpt (+) c ` A" + have "(-c) + (c + y) islimpt (+) (-c) ` (+) c ` A" + by (intro islimpt_isCont_image[OF y(2)] continuous_intros) + (auto simp: algebra_simps eventually_at_topological) + hence "y islimpt A" + by (simp add: image_image) + with y(1) B' show False + by blast + qed + ultimately show "\B. c + x \ B \ open B \ (\y\B. \ y islimpt (+) c ` A)" + by metis +qed + +lemma sparse_in_translate': + fixes A B :: "'a :: real_normed_vector set" + assumes "A sparse_in B" "C \ (+) c ` B" + shows "(+) c ` A sparse_in C" + using sparse_in_translate[OF assms(1)] assms(2) by (rule sparse_in_subset) + +lemma sparse_in_translate_UNIV: + fixes A B :: "'a :: real_normed_vector set" + assumes "A sparse_in UNIV" + shows "(+) c ` A sparse_in UNIV" + using assms by (rule sparse_in_translate') auto + subsection \Co-sparseness filter\ @@ -176,6 +227,13 @@ "\\<^sub>\x\A. P" == "CONST eventually (\x. P) (CONST cosparse A)" syntax + "_eventually_cosparse_UNIV" :: "pttrn => bool => bool" (\(\indent=3 notation=\binder \\\\\\<^sub>\_./ _)\ [0, 10] 10) +syntax_consts + "_eventually_cosparse_UNIV" == eventually +translations + "\\<^sub>\x. P" == "CONST eventually (\x. P) (CONST cosparse CONST UNIV)" + +syntax "_qeventually_cosparse" :: "pttrn \ bool \ 'a \ 'a" (\(\indent=3 notation=\binder \\\\\\<^sub>\_ | (_)./ _)\ [0, 0, 10] 10) syntax_consts "_qeventually_cosparse" == eventually diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Apr 16 21:13:33 2025 +0100 @@ -363,6 +363,12 @@ box (\i\Basis. max (a\i) (c\i) *\<^sub>R i) (\i\Basis. min (b\i) (d\i) *\<^sub>R i)" unfolding set_eq_iff and Int_iff and mem_box by auto +lemma cbox_prod: "cbox a b = cbox (fst a) (fst b) \ cbox (snd a) (snd b)" + by (cases a; cases b) auto + +lemma box_prod: "box a b = box (fst a) (fst b) \ box (snd a) (snd b)" + by (cases a; cases b) (force simp: box_def Basis_prod_def) + lemma rational_boxes: fixes x :: "'a::euclidean_space" assumes "e > 0" @@ -722,6 +728,12 @@ lemma box_complex_of_real [simp]: "box (complex_of_real x) (complex_of_real y) = {}" by (auto simp: in_box_complex_iff) +lemma cbox_complex_eq: "cbox a b = {x. Re x \ {Re a..Re b} \ Im x \ {Im a..Im b}}" + by (auto simp: in_cbox_complex_iff) + +lemma box_complex_eq: "box a b = {x. Re x \ {Re a<.. Im x \ {Im a<.. cbox c d = diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Archimedean_Field.thy Wed Apr 16 21:13:33 2025 +0100 @@ -775,6 +775,55 @@ lemma frac_neg_eq_iff: "frac (-x) = frac (-y) \ frac x = frac y" using add.inverse_inverse frac_neg_frac by metis +lemma frac_eqE: + assumes "frac x = frac y" + obtains n where "x = y + of_int n" + by (rule that[of "floor x - floor y"]) (use assms in \auto simp: frac_def\) + +lemma frac_add_of_int_right [simp]: "frac (x + of_int n) = frac x" + by (auto simp: frac_def) + +lemma frac_add_of_int_left [simp]: "frac (of_int n + x) = frac x" + by (auto simp: frac_def) + +lemma frac_add_int_right: "y \ \ \ frac (x + y) = frac x" + by (elim Ints_cases) auto + +lemma frac_add_int_left: "x \ \ \ frac (x + y) = frac y" + by (elim Ints_cases) auto + +lemma bij_betw_frac: "bij_betw frac {x.. {x.. {x..of_int n\ = \a - b\" + using n by (simp add: algebra_simps) + also have "\ < 1" + using * by auto + finally have "n = 0" + by (simp flip: of_int_abs) + with n show "a = b" + by auto + qed +next + show "frac ` {x.. {0..<1}" + have "t = frac (if t \ frac x then x + t - frac x else x + t - frac x + 1)" + using frac_eq[of t] t by (auto simp: frac_def) + moreover have "(if t \ frac x then x + t - frac x else x + t - frac x + 1) \ {x.. frac ` {x..Rounding to the nearest integer\ definition round :: "'a::floor_ceiling \ int" diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Code_Numeral.thy Wed Apr 16 21:13:33 2025 +0100 @@ -642,7 +642,7 @@ by (transfer; simp)+ lemma or_integer_code [code]: - \Pos Num.One AND Pos Num.One = Pos Num.One\ + \Pos Num.One OR Pos Num.One = Pos Num.One\ \Pos Num.One OR Pos (Num.Bit0 n) = Pos (Num.Bit1 n)\ \Pos (Num.Bit0 m) OR Pos Num.One = Pos (Num.Bit1 m)\ \Pos Num.One OR Pos (Num.Bit1 n) = Pos (Num.Bit1 n)\ @@ -1018,7 +1018,7 @@ val word_max_index = word_of_int max_index; fun words_of_int k = case divMod (k, max_index) - of (b, s) => word_of_int s :: (replicate b word_max_index); + of (b, s) => word_of_int s :: replicate b word_max_index; fun push' i k = << (k, i); @@ -1046,7 +1046,7 @@ let max_index = Z.of_int max_int;; let splitIndex i = let (b, s) = Z.div_rem i max_index - in Z.to_int s :: (replicate b max_int);; + in Z.to_int s :: replicate b max_int;; let push' i k = Z.shift_left k i;; diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Codegenerator_Test/Basic_Setup.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Basic_Setup.thy Wed Apr 16 21:13:33 2025 +0100 @@ -0,0 +1,33 @@ +(* Author: Florian Haftmann, TU Muenchen *) + +section \Basic setup\ + +theory Basic_Setup +imports + Complex_Main +begin + +text \Drop technical stuff from \<^theory>\HOL.Quickcheck_Narrowing\ which is tailored towards Haskell\ + +ML \ +structure Codegenerator_Test = +struct + +fun drop_partial_term_of thy = + let + val tycos = Sign.logical_types thy; + val consts = map_filter (try (curry (Axclass.param_of_inst thy) + \<^const_name>\Quickcheck_Narrowing.partial_term_of\)) tycos; + in + thy + |> fold Code.declare_unimplemented_global consts + end; + +end; +\ + +text \Avoid popular infix.\ + +code_reserved (SML) upto + +end diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Codegenerator_Test/Candidates.thy --- a/src/HOL/Codegenerator_Test/Candidates.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Codegenerator_Test/Candidates.thy Wed Apr 16 21:13:33 2025 +0100 @@ -5,7 +5,7 @@ theory Candidates imports - Complex_Main + Basic_Setup "HOL-Library.Library" "HOL-Library.Sorting_Algorithms" "HOL-Library.Subseq_Order" @@ -19,16 +19,7 @@ "HOL-Examples.Gauss_Numbers" begin -text \Drop technical stuff from \<^theory>\HOL.Quickcheck_Narrowing\ which is tailored towards Haskell\ - -setup \ -fn thy => -let - val tycos = Sign.logical_types thy; - val consts = map_filter (try (curry (Axclass.param_of_inst thy) - \<^const_name>\Quickcheck_Narrowing.partial_term_of\)) tycos; -in fold Code.declare_unimplemented_global consts thy end -\ +setup \Codegenerator_Test.drop_partial_term_of\ text \Simple example for the predicate compiler.\ @@ -40,10 +31,6 @@ code_pred sublist . -text \Avoid popular infix.\ - -code_reserved (SML) upto - text \Explicit check in \OCaml\ for correct precedence of let expressions in list expressions\ definition funny_list :: "bool list" diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Codegenerator_Test/Generate_Target_Rewrites_To_Bit_Operations.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Generate_Target_Rewrites_To_Bit_Operations.thy Wed Apr 16 21:13:33 2025 +0100 @@ -0,0 +1,21 @@ +(* Author: Florian Haftmann, TU Muenchen *) + +section \Test of arithmetic using target-language bit operations\ + +theory Generate_Target_Rewrites_To_Bit_Operations +imports + Basic_Setup + "HOL-Library.Code_Bit_Shifts_for_Arithmetic" + "HOL-Library.Code_Test" +begin + +setup \Codegenerator_Test.drop_partial_term_of\ + +text \ + If any of the checks fails, inspect the code generated + by a corresponding \export_code\ command. +\ + +export_code _ checking SML OCaml? Haskell? Scala + +end diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Complex.thy Wed Apr 16 21:13:33 2025 +0100 @@ -1032,6 +1032,32 @@ using filterlim_norm_at_top_imp_at_infinity by blast qed +lemma tendsto_cis [tendsto_intros]: + assumes "(f \ x) F" + shows "((\u. cis (f u)) \ cis x) F" + unfolding cis_conv_exp by (intro tendsto_intros assms) + +lemma tendsto_rcis [tendsto_intros]: + assumes "(f \ r) F" "(g \ x) F" + shows "((\u. rcis (f u) (g u)) \ rcis r x) F" + unfolding rcis_def by (intro tendsto_intros assms) + +lemma continuous_on_rcis [continuous_intros]: + "continuous_on A f \ continuous_on A g \ continuous_on A (\x. rcis (f x) (g x))" + unfolding rcis_def by (intro continuous_intros) + +lemma has_derivative_cis [derivative_intros]: + assumes "(f has_derivative d) (at x within A)" + shows "((\x. cis (f x)) has_derivative (\t. d t *\<^sub>R (\ * cis (f x)))) (at x within A)" +proof (rule has_derivative_compose[OF assms]) + have cis_eq: "cis = (\x. cos x + \ * sin x)" + by (auto simp: complex_eq_iff cos_of_real sin_of_real) + have "(cis has_vector_derivative (\ * cis (f x))) (at (f x))" + unfolding cis_eq by (auto intro!: derivative_eq_intros simp: cos_of_real sin_of_real algebra_simps) + thus "(cis has_derivative (\a. a *\<^sub>R (\ * cis (f x)))) (at (f x))" + by (simp add: has_vector_derivative_def) +qed + subsubsection \Complex argument\ definition Arg :: "complex \ real" @@ -1126,6 +1152,7 @@ lemma sin_Arg: "z \ 0 \ sin (Arg z) = Im z / norm z" by (metis Im_sgn cis.sel(2) cis_Arg) + subsection \Complex n-th roots\ lemma bij_betw_roots_unity: @@ -1365,7 +1392,7 @@ lemma csqrt_minus [simp]: assumes "Im x < 0 \ (Im x = 0 \ 0 \ Re x)" - shows "csqrt (- x) = \ * csqrt x" + shows "csqrt (-x) = \ * csqrt x" proof - have "csqrt ((\ * csqrt x)^2) = \ * csqrt x" proof (rule csqrt_square) @@ -1379,6 +1406,17 @@ finally show ?thesis . qed +lemma csqrt_neq_neg_real: + assumes "Im x = 0" "Re x < 0" + shows "csqrt z \ x" + using csqrt_principal[of z] assms by auto + +lemma csqrt_of_real: "x \ 0 \ csqrt (of_real x) = of_real (sqrt x)" + by (rule csqrt_unique) (auto simp flip: of_real_power) + +lemma csqrt_of_real': "csqrt (of_real x) = of_real (sqrt \x\) * (if x \ 0 then 1 else \)" + by (rule csqrt_unique) (auto simp flip: of_real_power simp: power_mult_distrib) + text \Legacy theorem names\ diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy --- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Wed Apr 16 21:13:33 2025 +0100 @@ -468,7 +468,7 @@ thus ?thesis by (simp add: o_def) qed - + lemma contour_integral_comp_analyticW: assumes "f analytic_on s" "valid_path \" "path_image \ \ s" shows "contour_integral (f \ \) g = contour_integral \ (\w. deriv f w * g (f w))" diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Complex_Analysis/Complex_Singularities.thy --- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Wed Apr 16 21:13:33 2025 +0100 @@ -4,6 +4,22 @@ subsection \Non-essential singular points\ +lemma at_to_0': "NO_MATCH 0 z \ at z = filtermap (\x. x + z) (at 0)" + for z :: "'a::real_normed_vector" + by (rule at_to_0) + +lemma nhds_to_0: "nhds (x :: 'a :: real_normed_vector) = filtermap ((+) x) (nhds 0)" +proof - + have "(\xa. xa - - x) = (+) x" + by auto + thus ?thesis + using filtermap_nhds_shift[of "-x" 0] by simp +qed + +lemma nhds_to_0': "NO_MATCH 0 x \ nhds (x :: 'a :: real_normed_vector) = filtermap ((+) x) (nhds 0)" + by (rule nhds_to_0) + + definition\<^marker>\tag important\ is_pole :: "('a::topological_space \ 'b::real_normed_vector) \ 'a \ bool" where "is_pole f a = (LIM x (at a). f x :> at_infinity)" @@ -2455,7 +2471,7 @@ assumes f_iso: "isolated_singularity_at f z" and f_ness: "not_essential f z" and fg_nconst: "\\<^sub>Fw in (at z). deriv f w * f w \ 0" - and f_ord: "zorder f z \0" + and f_ord: "zorder f z \ 0" shows "is_pole (\z. deriv f z / f z) z" proof (rule neg_zorder_imp_is_pole) define ff where "ff=(\w. deriv f w / f w)" @@ -2490,106 +2506,6 @@ using isolated_pole_imp_neg_zorder assms by fastforce qed -subsection \Isolated zeroes\ - -definition isolated_zero :: "(complex \ complex) \ complex \ bool" where - "isolated_zero f z \ f z = 0 \ eventually (\z. f z \ 0) (at z)" - -lemma isolated_zero_altdef: "isolated_zero f z \ f z = 0 \ \z islimpt {z. f z = 0}" - unfolding isolated_zero_def eventually_at_filter eventually_nhds islimpt_def by blast - -lemma isolated_zero_mult1: - assumes "isolated_zero f x" "isolated_zero g x" - shows "isolated_zero (\x. f x * g x) x" -proof - - have "\\<^sub>F x in at x. f x \ 0" "\\<^sub>F x in at x. g x \ 0" - using assms unfolding isolated_zero_def by auto - hence "eventually (\x. f x * g x \ 0) (at x)" - by eventually_elim auto - with assms show ?thesis - by (auto simp: isolated_zero_def) -qed - -lemma isolated_zero_mult2: - assumes "isolated_zero f x" "g x \ 0" "g analytic_on {x}" - shows "isolated_zero (\x. f x * g x) x" -proof - - have "eventually (\x. f x \ 0) (at x)" - using assms unfolding isolated_zero_def by auto - moreover have "eventually (\x. g x \ 0) (at x)" - using analytic_at_neq_imp_eventually_neq[of g x 0] assms by auto - ultimately have "eventually (\x. f x * g x \ 0) (at x)" - by eventually_elim auto - thus ?thesis - using assms(1) by (auto simp: isolated_zero_def) -qed - -lemma isolated_zero_mult3: - assumes "isolated_zero f x" "g x \ 0" "g analytic_on {x}" - shows "isolated_zero (\x. g x * f x) x" - using isolated_zero_mult2[OF assms] by (simp add: mult_ac) - -lemma isolated_zero_prod: - assumes "\x. x \ I \ isolated_zero (f x) z" "I \ {}" "finite I" - shows "isolated_zero (\y. \x\I. f x y) z" - using assms(3,2,1) by (induction rule: finite_ne_induct) (auto intro: isolated_zero_mult1) - -lemma non_isolated_zero': - assumes "isolated_singularity_at f z" "not_essential f z" "f z = 0" "\isolated_zero f z" - shows "eventually (\z. f z = 0) (at z)" - by (metis assms isolated_zero_def non_zero_neighbour not_eventually) - -lemma non_isolated_zero: - assumes "\isolated_zero f z" "f analytic_on {z}" "f z = 0" - shows "eventually (\z. f z = 0) (nhds z)" -proof - - have "eventually (\z. f z = 0) (at z)" - by (rule non_isolated_zero') - (use assms in \auto intro: not_essential_analytic isolated_singularity_at_analytic\) - with \f z = 0\ show ?thesis - unfolding eventually_at_filter by (auto elim!: eventually_mono) -qed - -lemma not_essential_compose: - assumes "not_essential f (g z)" "g analytic_on {z}" - shows "not_essential (\x. f (g x)) z" -proof (cases "isolated_zero (\w. g w - g z) z") - case False - hence "eventually (\w. g w - g z = 0) (nhds z)" - by (rule non_isolated_zero) (use assms in \auto intro!: analytic_intros\) - hence "not_essential (\x. f (g x)) z \ not_essential (\_. f (g z)) z" - by (intro not_essential_cong refl) - (auto elim!: eventually_mono simp: eventually_at_filter) - thus ?thesis - by (simp add: not_essential_const) -next - case True - hence ev: "eventually (\w. g w \ g z) (at z)" - by (auto simp: isolated_zero_def) - from assms consider c where "f \g z\ c" | "is_pole f (g z)" - by (auto simp: not_essential_def) - have "isCont g z" - by (rule analytic_at_imp_isCont) fact - hence lim: "g \z\ g z" - using isContD by blast - - from assms(1) consider c where "f \g z\ c" | "is_pole f (g z)" - unfolding not_essential_def by blast - thus ?thesis - proof cases - fix c assume "f \g z\ c" - hence "(\x. f (g x)) \z\ c" - by (rule filterlim_compose) (use lim ev in \auto simp: filterlim_at\) - thus ?thesis - by (auto simp: not_essential_def) - next - assume "is_pole f (g z)" - hence "is_pole (\x. f (g x)) z" - by (rule is_pole_compose) fact+ - thus ?thesis - by (auto simp: not_essential_def) - qed -qed subsection \Isolated points\ @@ -2618,85 +2534,143 @@ lemmas uniform_discreteI1 = uniformI1 lemmas uniform_discreteI2 = uniformI2 -lemma isolated_singularity_at_compose: - assumes "isolated_singularity_at f (g z)" "g analytic_on {z}" - shows "isolated_singularity_at (\x. f (g x)) z" -proof (cases "isolated_zero (\w. g w - g z) z") - case False - hence "eventually (\w. g w - g z = 0) (nhds z)" - by (rule non_isolated_zero) (use assms in \auto intro!: analytic_intros\) - hence "isolated_singularity_at (\x. f (g x)) z \ isolated_singularity_at (\_. f (g z)) z" - by (intro isolated_singularity_at_cong refl) - (auto elim!: eventually_mono simp: eventually_at_filter) +lemma zorder_zero_eqI': + assumes "f analytic_on {z}" + assumes "\i. i < nat n \ (deriv ^^ i) f z = 0" + assumes "(deriv ^^ nat n) f z \ 0" and "n \ 0" + shows "zorder f z = n" +proof - + from assms(1) obtain A where "open A" "z \ A" "f holomorphic_on A" + using analytic_at by blast thus ?thesis - by (simp add: isolated_singularity_at_const) -next - case True - from assms(1) obtain r where r: "r > 0" "f analytic_on ball (g z) r - {g z}" - by (auto simp: isolated_singularity_at_def) - hence holo_f: "f holomorphic_on ball (g z) r - {g z}" - by (subst (asm) analytic_on_open) auto - from assms(2) obtain r' where r': "r' > 0" "g holomorphic_on ball z r'" - by (auto simp: analytic_on_def) + using zorder_zero_eqI[of f A z n] assms by blast +qed + + +subsection \Isolated zeros\ + +definition isolated_zero :: "('a::topological_space \ 'b::real_normed_div_algebra) \ 'a \ bool" where + "isolated_zero f a \ f \a\ 0 \ eventually (\x. f x \ 0) (at a)" + +lemma isolated_zero_shift: + fixes z :: "'a :: real_normed_vector" + shows "isolated_zero f z \ isolated_zero (\w. f (z + w)) 0" + unfolding isolated_zero_def + by (simp add: at_to_0' eventually_filtermap filterlim_filtermap add_ac) + +lemma isolated_zero_shift': + fixes z :: "'a :: real_normed_vector" + assumes "NO_MATCH 0 z" + shows "isolated_zero f z \ isolated_zero (\w. f (z + w)) 0" + by (rule isolated_zero_shift) - have "continuous_on (ball z r') g" - using holomorphic_on_imp_continuous_on r' by blast - hence "isCont g z" - using r' by (subst (asm) continuous_on_eq_continuous_at) auto - hence "g \z\ g z" - using isContD by blast - hence "eventually (\w. g w \ ball (g z) r) (at z)" - using \r > 0\ unfolding tendsto_def by force - moreover have "eventually (\w. g w \ g z) (at z)" using True - by (auto simp: isolated_zero_def elim!: eventually_mono) - ultimately have "eventually (\w. g w \ ball (g z) r - {g z}) (at z)" - by eventually_elim auto - then obtain r'' where r'': "r'' > 0" "\w\ball z r''-{z}. g w \ ball (g z) r - {g z}" - unfolding eventually_at_filter eventually_nhds_metric ball_def - by (auto simp: dist_commute) - have "f \ g holomorphic_on ball z (min r' r'') - {z}" - proof (rule holomorphic_on_compose_gen) - show "g holomorphic_on ball z (min r' r'') - {z}" - by (rule holomorphic_on_subset[OF r'(2)]) auto - show "f holomorphic_on ball (g z) r - {g z}" - by fact - show "g ` (ball z (min r' r'') - {z}) \ ball (g z) r - {g z}" - using r'' by force - qed - hence "f \ g analytic_on ball z (min r' r'') - {z}" - by (subst analytic_on_open) auto - thus ?thesis using \r' > 0\ \r'' > 0\ - by (auto simp: isolated_singularity_at_def o_def intro!: exI[of _ "min r' r''"]) +lemma isolated_zero_imp_not_essential [intro]: + "isolated_zero f z \ not_essential f z" + unfolding isolated_zero_def not_essential_def + using tendsto_nhds_iff by blast + +lemma pole_is_not_zero: + fixes f:: "'a::perfect_space \ 'b::real_normed_field" + assumes "is_pole f z" + shows "\isolated_zero f z" +proof + assume "isolated_zero f z" + then have "filterlim f (nhds 0) (at z)" + unfolding isolated_zero_def using tendsto_nhds_iff by blast + moreover have "filterlim f at_infinity (at z)" + using \is_pole f z\ unfolding is_pole_def . + ultimately show False + using not_tendsto_and_filterlim_at_infinity[OF at_neq_bot] + by auto +qed + +lemma isolated_zero_imp_pole_inverse: + fixes f :: "_ \ 'b::{real_normed_div_algebra, division_ring}" + assumes "isolated_zero f z" + shows "is_pole (\z. inverse (f z)) z" +proof - + from assms have ev: "eventually (\z. f z \ 0) (at z)" + by (auto simp: isolated_zero_def) + have "filterlim f (nhds 0) (at z)" + using assms by (simp add: isolated_zero_def) + with ev have "filterlim f (at 0) (at z)" + using filterlim_atI by blast + also have "?this \ filterlim (\z. inverse (inverse (f z))) (at 0) (at z)" + by (rule filterlim_cong) (use ev in \auto elim!: eventually_mono\) + finally have "filterlim (\z. inverse (f z)) at_infinity (at z)" + by (subst filterlim_inverse_at_iff [symmetric]) + thus ?thesis + by (simp add: is_pole_def) qed -lemma is_pole_power_int_0: - assumes "f analytic_on {x}" "isolated_zero f x" "n < 0" - shows "is_pole (\x. f x powi n) x" +lemma is_pole_imp_isolated_zero_inverse: + fixes f :: "_ \ 'b::{real_normed_div_algebra, division_ring}" + assumes "is_pole f z" + shows "isolated_zero (\z. inverse (f z)) z" proof - - have "f \x\ f x" - using assms(1) by (simp add: analytic_at_imp_isCont isContD) - with assms show ?thesis - unfolding is_pole_def - by (intro filterlim_power_int_neg_at_infinity) (auto simp: isolated_zero_def) + from assms have ev: "eventually (\z. f z \ 0) (at z)" + by (simp add: non_zero_neighbour_pole) + have "filterlim f at_infinity (at z)" + using assms by (simp add: is_pole_def) + also have "?this \ filterlim (\z. inverse (inverse (f z))) at_infinity (at z)" + by (rule filterlim_cong) (use ev in \auto elim!: eventually_mono\) + finally have "filterlim (\z. inverse (f z)) (at 0) (at z)" + by (subst (asm) filterlim_inverse_at_iff [symmetric]) auto + hence "filterlim (\z. inverse (f z)) (nhds 0) (at z)" + using filterlim_at by blast + moreover have "eventually (\z. inverse (f z) \ 0) (at z)" + using ev by eventually_elim auto + ultimately show ?thesis + by (simp add: isolated_zero_def) qed -lemma isolated_zero_imp_not_constant_on: - assumes "isolated_zero f x" "x \ A" "open A" - shows "\f constant_on A" -proof - assume "f constant_on A" - then obtain c where c: "\x. x \ A \ f x = c" - by (auto simp: constant_on_def) - from assms and c[of x] have [simp]: "c = 0" - by (auto simp: isolated_zero_def) - have "eventually (\x. f x \ 0) (at x)" - using assms by (auto simp: isolated_zero_def) - moreover have "eventually (\x. x \ A) (at x)" - using assms by (intro eventually_at_in_open') auto - ultimately have "eventually (\x. False) (at x)" - by eventually_elim (use c in auto) - thus False - by simp +lemma is_pole_inverse_iff: "is_pole (\z. inverse (f z)) z \ isolated_zero f z" + using is_pole_imp_isolated_zero_inverse isolated_zero_imp_pole_inverse by fastforce + +lemma isolated_zero_inverse_iff: "isolated_zero (\z. inverse (f z)) z \ is_pole f z" + using is_pole_imp_isolated_zero_inverse isolated_zero_imp_pole_inverse by fastforce + +lemma zero_isolated_zero: + fixes f :: "'a :: {t2_space, perfect_space} \ _" + assumes "isolated_zero f z" "isCont f z" + shows "f z = 0" +proof (rule tendsto_unique) + show "f \z\ f z" + using assms(2) by (rule isContD) + show "f \z\ 0" + using assms(1) by (simp add: isolated_zero_def) +qed auto + +lemma zero_isolated_zero_analytic: + assumes "isolated_zero f z" "f analytic_on {z}" + shows "f z = 0" + using assms(1) analytic_at_imp_isCont[OF assms(2)] by (rule zero_isolated_zero) + +lemma isolated_zero_analytic_iff: + assumes "f analytic_on {z}" + shows "isolated_zero f z \ f z = 0 \ eventually (\z. f z \ 0) (at z)" +proof safe + assume "f z = 0" "eventually (\z. f z \ 0) (at z)" + with assms show "isolated_zero f z" + unfolding isolated_zero_def by (metis analytic_at_imp_isCont isCont_def) +qed (use zero_isolated_zero_analytic[OF _ assms] in \auto simp: isolated_zero_def\) + +lemma non_isolated_zero_imp_eventually_zero: + assumes "f analytic_on {z}" "f z = 0" "\isolated_zero f z" + shows "eventually (\z. f z = 0) (at z)" +proof (rule not_essential_frequently_0_imp_eventually_0) + from assms(1) show "isolated_singularity_at f z" "not_essential f z" + by (simp_all add: isolated_singularity_at_analytic not_essential_analytic) + from assms(1,2) have "f \z\ 0" + by (metis analytic_at_imp_isCont continuous_within) + thus "frequently (\z. f z = 0) (at z)" + using assms(2,3) by (auto simp: isolated_zero_def frequently_def) qed +lemma non_isolated_zero_imp_eventually_zero': + assumes "f analytic_on {z}" "f z = 0" "\isolated_zero f z" + shows "eventually (\z. f z = 0) (nhds z)" + using non_isolated_zero_imp_eventually_zero[OF assms] assms(2) + using eventually_nhds_conv_at by blast + end diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Complex_Analysis/Contour_Integration.thy --- a/src/HOL/Complex_Analysis/Contour_Integration.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Complex_Analysis/Contour_Integration.thy Wed Apr 16 21:13:33 2025 +0100 @@ -47,6 +47,12 @@ unfolding contour_integral_def has_contour_integral_def contour_integrable_on_def using has_integral_unique by blast +lemma has_contour_integral_cong: + assumes "\z. z \ path_image g \ f z = f' z" "g = g'" "c = c'" + shows "(f has_contour_integral c) g \ (f' has_contour_integral c') g'" + unfolding has_contour_integral_def assms(2,3) + by (intro has_integral_cong) (auto simp: assms path_image_def intro!: assms(1)) + lemma has_contour_integral_eqpath: "\(f has_contour_integral y) p; f contour_integrable_on \; contour_integral p f = contour_integral \ f\ diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Complex_Analysis/Laurent_Convergence.thy --- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy Wed Apr 16 21:13:33 2025 +0100 @@ -78,21 +78,6 @@ by (auto simp: fls_subdegree_ge0I) qed -lemma at_to_0': "NO_MATCH 0 z \ at z = filtermap (\x. x + z) (at 0)" - for z :: "'a::real_normed_vector" - by (rule at_to_0) - -lemma nhds_to_0: "nhds (x :: 'a :: real_normed_vector) = filtermap ((+) x) (nhds 0)" -proof - - have "(\xa. xa - - x) = (+) x" - by auto - thus ?thesis - using filtermap_nhds_shift[of "-x" 0] by simp -qed - -lemma nhds_to_0': "NO_MATCH 0 x \ nhds (x :: 'a :: real_normed_vector) = filtermap ((+) x) (nhds 0)" - by (rule nhds_to_0) - definition%important fls_conv_radius :: "complex fls \ ereal" where "fls_conv_radius f = fps_conv_radius (fls_regpart f)" diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Complex_Analysis/Meromorphic.thy --- a/src/HOL/Complex_Analysis/Meromorphic.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Complex_Analysis/Meromorphic.thy Wed Apr 16 21:13:33 2025 +0100 @@ -242,6 +242,94 @@ using False remove_sings_eqI by auto qed simp +lemma remove_sings_analytic_on: + assumes "isolated_singularity_at f z" "f \z\ c" + shows "remove_sings f analytic_on {z}" +proof - + from assms(1) obtain A where A: "open A" "z \ A" "f holomorphic_on (A - {z})" + using analytic_imp_holomorphic isolated_singularity_at_iff_analytic_nhd by auto + have ana: "f analytic_on (A - {z})" + by (subst analytic_on_open) (use A in auto) + + have "remove_sings f holomorphic_on A" + proof (rule no_isolated_singularity) + have "f holomorphic_on (A - {z})" + by fact + moreover have "remove_sings f holomorphic_on (A - {z}) \ f holomorphic_on (A - {z})" + by (intro holomorphic_cong remove_sings_at_analytic) (auto intro!: analytic_on_subset[OF ana]) + ultimately show "remove_sings f holomorphic_on (A - {z})" + by blast + hence "continuous_on (A-{z}) (remove_sings f)" + by (intro holomorphic_on_imp_continuous_on) + moreover have "isCont (remove_sings f) z" + using assms isCont_def remove_sings_eqI tendsto_remove_sings_iff by blast + ultimately show "continuous_on A (remove_sings f)" + by (metis A(1) DiffI closed_singleton continuous_on_eq_continuous_at open_Diff singletonD) + qed (use A(1) in auto) + thus ?thesis + using A(1,2) analytic_at by blast +qed + +lemma residue_remove_sings [simp]: + assumes "isolated_singularity_at f z" + shows "residue (remove_sings f) z = residue f z" +proof - + from assms have "eventually (\w. remove_sings f w = f w) (at z)" + using eventually_remove_sings_eq_at by blast + then obtain A where A: "open A" "z \ A" "\w. w \ A - {z} \ remove_sings f w = f w" + by (subst (asm) eventually_at_topological) blast + from A(1,2) obtain \ where \: "\ > 0" "cball z \ \ A" + using open_contains_cball_eq by blast + hence eq: "remove_sings f w = f w" if "w \ cball z \ - {z}" for w + using that A \ by blast + + define P where "P = (\f c \. (f has_contour_integral of_real (2 * pi) * \ * c) (circlepath z \))" + have "P (remove_sings f) c \ \ P f c \" if "0 < \" "\ < \" for c \ + unfolding P_def using \\ > 0\ that by (intro has_contour_integral_cong) (auto simp: eq) + hence *: "(\\>0. \ < e \ P (remove_sings f) c \) \ (\\>0. \ < e \ P f c \)" if "e \ \" for c e + using that by force + have **: "(\e>0. \\>0. \ < e \ P (remove_sings f) c \) \ (\e>0. \\>0. \ < e \ P f c \)" for c + proof + assume "(\e>0. \\>0. \ < e \ P (remove_sings f) c \)" + then obtain e where "e > 0" "\\>0. \ < e \ P (remove_sings f) c \" + by blast + thus "(\e>0. \\>0. \ < e \ P f c \)" + by (intro exI[of _ "min e \"]) (use *[of "min e \" c] \(1) in auto) + next + assume "(\e>0. \\>0. \ < e \ P f c \)" + then obtain e where "e > 0" "\\>0. \ < e \ P f c \" + by blast + thus "(\e>0. \\>0. \ < e \ P (remove_sings f) c \)" + by (intro exI[of _ "min e \"]) (use *[of "min e \" c] \(1) in auto) + qed + show ?thesis + unfolding residue_def by (intro arg_cong[of _ _ Eps] ext **[unfolded P_def]) +qed + +lemma remove_sings_shift_0: + "remove_sings f z = remove_sings (\w. f (z + w)) 0" +proof (cases "\c. f \z\ c") + case True + then obtain c where c: "f \z\ c" + by blast + from c have "remove_sings f z = c" + by (rule remove_sings_eqI) + moreover have "remove_sings (\w. f (z + w)) 0 = c" + by (rule remove_sings_eqI) (use c in \simp_all add: at_to_0' filterlim_filtermap add_ac\) + ultimately show ?thesis + by simp +next + case False + hence "\(\c. (\w. f (z + w)) \0\ c)" + by (simp add: at_to_0' filterlim_filtermap add_ac) + with False show ?thesis + by (simp add: remove_sings_def) +qed + +lemma remove_sings_shift_0': + "NO_MATCH 0 z \ remove_sings f z = remove_sings (\w. f (z + w)) 0" + by (rule remove_sings_shift_0) + subsection \Meromorphicity\ @@ -735,6 +823,37 @@ using eq[OF w not_pole[OF w]] . qed +lemma nicely_meromorphic_on_unop: + assumes "f nicely_meromorphic_on A" + assumes "f meromorphic_on A \ (\z. h (f z)) meromorphic_on A" + assumes "\z. z \ A \ is_pole f z \ is_pole (\z. h (f z)) z" + assumes "\z. z \ f ` A \ isCont h z" + assumes "h 0 = 0" + shows "(\z. h (f z)) nicely_meromorphic_on A" + unfolding nicely_meromorphic_on_def +proof (intro conjI ballI) + show "(\z. h (f z)) meromorphic_on A" + using assms(1,2) by (auto simp: nicely_meromorphic_on_def) +next + fix z assume z: "z \ A" + hence "is_pole f z \ f z = 0 \ f \z\ f z" + using assms by (auto simp: nicely_meromorphic_on_def) + thus "is_pole (\z. h (f z)) z \ h (f z) = 0 \ (\z. h (f z)) \z\ h (f z)" + proof (rule disj_forward) + assume "is_pole f z \ f z = 0" + thus "is_pole (\z. h (f z)) z \ h (f z) = 0" + using assms z by auto + next + assume *: "f \z\ f z" + from z assms have "isCont h (f z)" + by auto + with * show "(\z. h (f z)) \z\ h (f z)" + using continuous_within continuous_within_compose3 by blast + qed +qed + + + subsection \Closure properties and proofs for individual functions\ lemma meromorphic_on_const [intro, meromorphic_intros]: "(\_. c) meromorphic_on A" @@ -848,6 +967,33 @@ by (rule laurent_expansion_intros exI ballI assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+ +lemma nicely_meromorphic_on_const [intro]: "(\_. c) nicely_meromorphic_on A" + unfolding nicely_meromorphic_on_def by auto + +lemma nicely_meromorphic_on_cmult_left [intro]: + assumes "f nicely_meromorphic_on A" + shows "(\z. c * f z) nicely_meromorphic_on A" +proof (cases "c = 0") + case [simp]: False + show ?thesis + using assms by (rule nicely_meromorphic_on_unop) (auto intro!: meromorphic_intros) +qed (auto intro!: nicely_meromorphic_on_const) + +lemma nicely_meromorphic_on_cmult_right [intro]: + assumes "f nicely_meromorphic_on A" + shows "(\z. f z * c) nicely_meromorphic_on A" + using nicely_meromorphic_on_cmult_left[OF assms, of c] by (simp add: mult.commute) + +lemma nicely_meromorphic_on_scaleR [intro]: + assumes "f nicely_meromorphic_on A" + shows "(\z. c *\<^sub>R f z) nicely_meromorphic_on A" + using assms by (auto simp: scaleR_conv_of_real) + +lemma nicely_meromorphic_on_uminus [intro]: + assumes "f nicely_meromorphic_on A" + shows "(\z. -f z) nicely_meromorphic_on A" + using nicely_meromorphic_on_cmult_left[OF assms, of "-1"] by simp + lemma meromorphic_on_If [meromorphic_intros]: assumes "f meromorphic_on A" "g meromorphic_on B" assumes "\z. z \ A \ z \ B \ f z = g z" "open A" "open B" "C \ A \ B" @@ -954,6 +1100,31 @@ by eventually_elim auto qed +lemma remove_sings_constant_on_open_iff: + assumes "f meromorphic_on A" "open A" + shows "remove_sings f constant_on A \ (\c. \\<^sub>\x\A. f x = c)" +proof + assume "remove_sings f constant_on A" + then obtain c where c: "remove_sings f z = c" if "z \ A" for z + using that by (auto simp: constant_on_def) + have "\\<^sub>\x\A. x \ A" + using \open A\ by (simp add: eventually_in_cosparse) + hence "\\<^sub>\x\A. f x = c" + using eventually_remove_sings_eq[OF assms(1)] by eventually_elim (use c in auto) + thus "\c. \\<^sub>\x\A. f x = c" + by blast +next + assume "\c. \\<^sub>\x\A. f x = c" + then obtain c where c: "\\<^sub>\x\A. f x = c" + by blast + have "\\<^sub>\x\A. remove_sings f x = c" + using eventually_remove_sings_eq[OF assms(1)] c by eventually_elim auto + hence "remove_sings f z = c" if "z \ A" for z using that + by (meson assms(2) c eventually_cosparse_open_eq remove_sings_eqI tendsto_eventually) + thus "remove_sings f constant_on A" + unfolding constant_on_def by blast +qed + text \ A meromorphic function on a connected domain takes any given value either almost everywhere @@ -1274,4 +1445,418 @@ by (auto simp: constant_on_def) qed + +subsection \More on poles and zeros\ + +lemma zorder_prod: + assumes "\x. x \ A \ f x meromorphic_on {z}" + assumes "eventually (\z. (\x\A. f x z) \ 0) (at z)" + shows "zorder (\z. \x\A. f x z) z = (\x\A. zorder (f x) z)" + using assms +proof (induction A rule: infinite_finite_induct) + case (insert a A) + have "zorder (\z. \x\insert a A. f x z) z = zorder (\z. f a z * (\x\A. f x z)) z" + using insert.hyps by simp + also have "\ = zorder (f a) z + zorder (\z. \x\A. f x z) z" + proof (subst zorder_mult) + have "\\<^sub>F z in at z. f a z \ 0" + using insert.prems(2) by eventually_elim (use insert.hyps in auto) + thus "\\<^sub>F z in at z. f a z \ 0" + using eventually_frequently at_neq_bot by blast + next + have "\\<^sub>F z in at z. (\x\A. f x z) \ 0" + using insert.prems(2) by eventually_elim (use insert.hyps in auto) + thus "\\<^sub>F z in at z. (\x\A. f x z) \ 0" + using eventually_frequently at_neq_bot by blast + qed (use insert.prems in \auto intro!: meromorphic_intros\) + also have "zorder (\z. \x\A. f x z) z = (\x\A. zorder (f x) z)" + by (intro insert.IH) (use insert.prems insert.hyps in \auto elim!: eventually_mono\) + also have "zorder (f a) z + \ = (\x\insert a A. zorder (f x) z)" + using insert.hyps by simp + finally show ?case . +qed auto + +lemma zorder_scale: + assumes "f meromorphic_on {a * z}" "a \ 0" + shows "zorder (\w. f (a * w)) z = zorder f (a * z)" +proof (cases "eventually (\z. f z = 0) (at (a * z))") + case True + hence ev: "eventually (\z. f (a * z) = 0) (at z)" + proof (rule eventually_compose_filterlim) + show "filterlim ((*) a) (at (a * z)) (at z)" + proof (rule filterlim_atI) + show "\\<^sub>F x in at z. a * x \ a * z" + using eventually_neq_at_within[of z z] by eventually_elim (use \a \ 0\ in auto) + qed (auto intro!: tendsto_intros) + qed + + have "zorder (\w. f (a * w)) z = zorder (\_. 0) z" + by (rule zorder_cong) (use ev in auto) + also have "\ = zorder (\_. 0) (a * z)" + by (simp add: zorder_shift') + also have "\ = zorder f (a * z)" + by (rule zorder_cong) (use True in auto) + finally show ?thesis . +next + case False + define G where "G = fps_const a * fps_X" + have "zorder (f \ (\z. a * z)) z = zorder f (a * z) * int (subdegree G)" + proof (rule zorder_compose) + show "isolated_singularity_at f (a * z)" "not_essential f (a * z)" + using assms(1) by (auto simp: meromorphic_on_altdef) + next + have "(\x. a * x) has_fps_expansion G" + unfolding G_def by (intro fps_expansion_intros) + thus "(\x. a * (z + x) - a * z) has_fps_expansion G" + by (simp add: algebra_simps) + next + show "\\<^sub>F w in at (a * z). f w \ 0" using False + by (metis assms(1) has_laurent_expansion_isolated has_laurent_expansion_not_essential + meromorphic_on_def non_zero_neighbour not_eventually singletonI) + qed (use \a \ 0\ in \auto simp: G_def\) + also have "subdegree G = 1" + using \a \ 0\ by (simp add: G_def) + finally show ?thesis + by (simp add: o_def) +qed + +lemma zorder_uminus: + assumes "f meromorphic_on {-z}" + shows "zorder (\w. f (-w)) z = zorder f (-z)" + using assms zorder_scale[of f "-1" z] by simp + +lemma is_pole_deriv_iff: + assumes "f meromorphic_on {z}" + shows "is_pole (deriv f) z \ is_pole f z" +proof - + from assms obtain F where F: "(\w. f (z + w)) has_laurent_expansion F" + by (auto simp: meromorphic_on_def) + have "deriv (\w. f (z + w)) has_laurent_expansion fls_deriv F" + using F by (rule has_laurent_expansion_deriv) + also have "deriv (\w. f (z + w)) = (\w. deriv f (z + w))" + by (simp add: deriv_shift_0' add_ac o_def fun_eq_iff) + finally have F': "(\w. deriv f (z + w)) has_laurent_expansion fls_deriv F" . + have "is_pole (deriv f) z \ fls_subdegree (fls_deriv F) < 0" + using is_pole_fls_subdegree_iff[OF F'] by simp + also have "\ \ fls_subdegree F < 0" + using fls_deriv_subdegree0 fls_subdegree_deriv linorder_less_linear by fastforce + also have "\ \ is_pole f z" + using F by (simp add: has_laurent_expansion_imp_is_pole_iff) + finally show ?thesis . +qed + +lemma isolated_zero_remove_sings_iff [simp]: + assumes "isolated_singularity_at f z" + shows "isolated_zero (remove_sings f) z \ isolated_zero f z" +proof - + have *: "(\\<^sub>F x in at z. remove_sings f x \ 0) \ (\\<^sub>F x in at z. f x \ 0)" + proof + assume "(\\<^sub>F x in at z. f x \ 0)" + thus "(\\<^sub>F x in at z. remove_sings f x \ 0)" + using eventually_remove_sings_eq_at[OF assms] + by eventually_elim auto + next + assume "(\\<^sub>F x in at z. remove_sings f x \ 0)" + thus "(\\<^sub>F x in at z. f x \ 0)" + using eventually_remove_sings_eq_at[OF assms] + by eventually_elim auto + qed + show ?thesis + unfolding isolated_zero_def using assms * by simp +qed + +lemma zorder_isolated_zero_pos: + assumes "isolated_zero f z" "f analytic_on {z}" + shows "zorder f z > 0" +proof (subst zorder_pos_iff' [OF assms(2)]) + show "f z = 0" + using assms by (simp add: zero_isolated_zero_analytic) +next + have "\\<^sub>F z in at z. f z \ 0" + using assms by (auto simp: isolated_zero_def) + thus "\\<^sub>F z in at z. f z \ 0" + by (simp add: eventually_frequently) +qed + +lemma zorder_isolated_zero_pos': + assumes "isolated_zero f z" "isolated_singularity_at f z" + shows "zorder f z > 0" +proof - + from assms(1) have "f \z\ 0" + by (simp add: isolated_zero_def) + with assms(2) have "remove_sings f analytic_on {z}" + by (intro remove_sings_analytic_on) + hence "zorder (remove_sings f) z > 0" + using assms by (intro zorder_isolated_zero_pos) auto + thus ?thesis + using assms by simp +qed + +lemma zero_isolated_zero_nicely_meromorphic: + assumes "isolated_zero f z" "f nicely_meromorphic_on {z}" + shows "f z = 0" +proof - + have "\is_pole f z" + using assms pole_is_not_zero by blast + with assms(2) have "f analytic_on {z}" + by (simp add: nicely_meromorphic_on_imp_analytic_at) + with zero_isolated_zero_analytic assms(1) show ?thesis + by blast +qed + +lemma meromorphic_on_imp_not_zero_cosparse: + assumes "f meromorphic_on A" + shows "eventually (\z. \isolated_zero f z) (cosparse A)" +proof - + have "eventually (\z. \is_pole (\z. inverse (f z)) z) (cosparse A)" + by (intro meromorphic_on_imp_not_pole_cosparse meromorphic_intros assms) + thus ?thesis + by (simp add: is_pole_inverse_iff) +qed + +lemma nicely_meromorphic_on_inverse [meromorphic_intros]: + assumes "f nicely_meromorphic_on A" + shows "(\x. inverse (f x)) nicely_meromorphic_on A" + unfolding nicely_meromorphic_on_def +proof (intro conjI ballI) + fix z assume z: "z \ A" + have "is_pole f z \ f z = 0 \ f \z\ f z" + using assms z by (auto simp: nicely_meromorphic_on_def) + thus "is_pole (\x. inverse (f x)) z \ inverse (f z) = 0 \ + (\x. inverse (f x)) \z\ inverse (f z)" + proof + assume "is_pole f z \ f z = 0" + hence "isolated_zero (\z. inverse (f z)) z \ inverse (f z) = 0" + by (auto simp: isolated_zero_inverse_iff) + hence "(\x. inverse (f x)) \z\ inverse (f z)" + by (simp add: isolated_zero_def) + thus ?thesis .. + next + assume lim: "f \z\ f z" + hence ana: "f analytic_on {z}" + using assms is_pole_def nicely_meromorphic_on_imp_analytic_at + not_tendsto_and_filterlim_at_infinity trivial_limit_at z by blast + show ?thesis + proof (cases "isolated_zero f z") + case True + with lim have "f z = 0" + using continuous_within zero_isolated_zero by blast + with True have "is_pole (\z. inverse (f z)) z \ inverse (f z) = 0" + by (auto simp: is_pole_inverse_iff) + thus ?thesis .. + next + case False + hence "f z \ 0 \ (f z = 0 \ eventually (\z. f z = 0) (at z))" + using non_isolated_zero_imp_eventually_zero[OF ana] by blast + thus ?thesis + proof (elim disjE conjE) + assume "f z \ 0" + hence "(\z. inverse (f z)) \z\ inverse (f z)" + by (intro tendsto_intros lim) + thus ?thesis .. + next + assume *: "f z = 0" "eventually (\z. f z = 0) (at z)" + have "eventually (\z. inverse (f z) = 0) (at z)" + using *(2) by eventually_elim auto + hence "(\z. inverse (f z)) \z\ 0" + by (simp add: tendsto_eventually) + with *(1) show ?thesis + by auto + qed + qed + qed +qed (use assms in \auto simp: nicely_meromorphic_on_def intro!: meromorphic_intros\) + +lemma is_pole_zero_at_nicely_mero: + assumes "f nicely_meromorphic_on A" "is_pole f z" "z \ A" + shows "f z = 0" + by (meson assms at_neq_bot + is_pole_def nicely_meromorphic_on_def + not_tendsto_and_filterlim_at_infinity) + +lemma zero_or_pole: + assumes mero: "f nicely_meromorphic_on A" + and "z \ A" "f z = 0" and event: "\\<^sub>F x in at z. f x \ 0" + shows "isolated_zero f z \ is_pole f z" +proof - + from mero \z\A\ + have "(is_pole f z \ f z=0) \ f \z\ f z" + unfolding nicely_meromorphic_on_def by simp + moreover have "isolated_zero f z" if "f \z\ f z" + unfolding isolated_zero_def + using \f z=0\ that event tendsto_nhds_iff by auto + ultimately show ?thesis by auto +qed + +lemma isolated_zero_fls_subdegree_iff: + assumes "(\x. f (z + x)) has_laurent_expansion F" + shows "isolated_zero f z \ fls_subdegree F > 0" + using assms unfolding isolated_zero_def + by (metis Lim_at_zero fls_zero_subdegree has_laurent_expansion_eventually_nonzero_iff not_le + order.refl tendsto_0_subdegree_iff_0) + +lemma zorder_pos_imp_isolated_zero: + assumes "f meromorphic_on {z}" "eventually (\z. f z \ 0) (at z)" "zorder f z > 0" + shows "isolated_zero f z" + using assms isolated_zero_fls_subdegree_iff + by (metis has_laurent_expansion_eventually_nonzero_iff + has_laurent_expansion_zorder insertI1 + meromorphic_on_def) + +lemma zorder_neg_imp_is_pole: + assumes "f meromorphic_on {z}" "eventually (\z. f z \ 0) (at z)" "zorder f z < 0" + shows "is_pole f z" + using assms is_pole_fls_subdegree_iff at_neq_bot eventually_frequently meromorphic_at_iff + neg_zorder_imp_is_pole by blast + +lemma not_pole_not_isolated_zero_imp_zorder_eq_0: + assumes "f meromorphic_on {z}" "\is_pole f z" "\isolated_zero f z" "frequently (\z. f z \ 0) (at z)" + shows "zorder f z = 0" +proof - + have "remove_sings f analytic_on {z}" + using assms meromorphic_at_iff not_essential_def remove_sings_analytic_on by blast + moreover from this and assms have "remove_sings f z \ 0" + using isolated_zero_def meromorphic_at_iff non_zero_neighbour remove_sings_eq_0_iff by blast + moreover have "frequently (\z. remove_sings f z \ 0) (at z)" + using assms analytic_at_neq_imp_eventually_neq calculation(1,2) + eventually_frequently trivial_limit_at by blast + ultimately have "zorder (remove_sings f) z = 0" + using zorder_eq_0_iff by blast + thus ?thesis + using assms(1) meromorphic_at_iff by auto +qed + +lemma not_essential_compose: + assumes "not_essential f (g z)" "g analytic_on {z}" + shows "not_essential (\x. f (g x)) z" +proof (cases "isolated_zero (\w. g w - g z) z") + case False + hence "eventually (\w. g w - g z = 0) (nhds z)" + by (intro non_isolated_zero_imp_eventually_zero' analytic_intros assms) auto + hence "not_essential (\x. f (g x)) z \ not_essential (\_. f (g z)) z" + by (intro not_essential_cong refl) + (auto elim!: eventually_mono simp: eventually_at_filter) + thus ?thesis + by (simp add: not_essential_const) +next + case True + hence ev: "eventually (\w. g w \ g z) (at z)" + by (auto simp: isolated_zero_def) + from assms consider c where "f \g z\ c" | "is_pole f (g z)" + by (auto simp: not_essential_def) + have "isCont g z" + by (rule analytic_at_imp_isCont) fact + hence lim: "g \z\ g z" + using isContD by blast + + from assms(1) consider c where "f \g z\ c" | "is_pole f (g z)" + unfolding not_essential_def by blast + thus ?thesis + proof cases + fix c assume "f \g z\ c" + hence "(\x. f (g x)) \z\ c" + by (rule filterlim_compose) (use lim ev in \auto simp: filterlim_at\) + thus ?thesis + by (auto simp: not_essential_def) + next + assume "is_pole f (g z)" + hence "is_pole (\x. f (g x)) z" + by (rule is_pole_compose) fact+ + thus ?thesis + by (auto simp: not_essential_def) + qed +qed + + +lemma isolated_singularity_at_compose: + assumes "isolated_singularity_at f (g z)" "g analytic_on {z}" + shows "isolated_singularity_at (\x. f (g x)) z" +proof (cases "isolated_zero (\w. g w - g z) z") + case False + hence "eventually (\w. g w - g z = 0) (nhds z)" + by (intro non_isolated_zero_imp_eventually_zero') (use assms in \auto intro!: analytic_intros\) + hence "isolated_singularity_at (\x. f (g x)) z \ isolated_singularity_at (\_. f (g z)) z" + by (intro isolated_singularity_at_cong refl) + (auto elim!: eventually_mono simp: eventually_at_filter) + thus ?thesis + by (simp add: isolated_singularity_at_const) +next + case True + from assms(1) obtain r where r: "r > 0" "f analytic_on ball (g z) r - {g z}" + by (auto simp: isolated_singularity_at_def) + hence holo_f: "f holomorphic_on ball (g z) r - {g z}" + by (subst (asm) analytic_on_open) auto + from assms(2) obtain r' where r': "r' > 0" "g holomorphic_on ball z r'" + by (auto simp: analytic_on_def) + + have "continuous_on (ball z r') g" + using holomorphic_on_imp_continuous_on r' by blast + hence "isCont g z" + using r' by (subst (asm) continuous_on_eq_continuous_at) auto + hence "g \z\ g z" + using isContD by blast + hence "eventually (\w. g w \ ball (g z) r) (at z)" + using \r > 0\ unfolding tendsto_def by force + moreover have "eventually (\w. g w \ g z) (at z)" using True + by (auto simp: isolated_zero_def elim!: eventually_mono) + ultimately have "eventually (\w. g w \ ball (g z) r - {g z}) (at z)" + by eventually_elim auto + then obtain r'' where r'': "r'' > 0" "\w\ball z r''-{z}. g w \ ball (g z) r - {g z}" + unfolding eventually_at_filter eventually_nhds_metric ball_def + by (auto simp: dist_commute) + have "f \ g holomorphic_on ball z (min r' r'') - {z}" + proof (rule holomorphic_on_compose_gen) + show "g holomorphic_on ball z (min r' r'') - {z}" + by (rule holomorphic_on_subset[OF r'(2)]) auto + show "f holomorphic_on ball (g z) r - {g z}" + by fact + show "g ` (ball z (min r' r'') - {z}) \ ball (g z) r - {g z}" + using r'' by force + qed + hence "f \ g analytic_on ball z (min r' r'') - {z}" + by (subst analytic_on_open) auto + thus ?thesis using \r' > 0\ \r'' > 0\ + by (auto simp: isolated_singularity_at_def o_def intro!: exI[of _ "min r' r''"]) +qed + +lemma is_pole_power_int_0: + assumes "f analytic_on {x}" "isolated_zero f x" "n < 0" + shows "is_pole (\x. f x powi n) x" +proof - + have "f \x\ f x" + using assms(1) by (simp add: analytic_at_imp_isCont isContD) + with assms show ?thesis + unfolding is_pole_def + by (intro filterlim_power_int_neg_at_infinity) (auto simp: isolated_zero_def) +qed + +lemma isolated_zero_imp_not_constant_on: + fixes f :: "'a :: perfect_space \ 'b :: real_normed_div_algebra" + assumes "isolated_zero f x" "x \ A" "open A" + shows "\f constant_on A" +proof + assume "f constant_on A" + then obtain c where c: "\x. x \ A \ f x = c" + by (auto simp: constant_on_def) + have "eventually (\z. z \ A - {x}) (at x)" + by (intro eventually_at_in_open assms) + hence "eventually (\z. f z = c) (at x)" + by eventually_elim (use c in auto) + hence "f \x\ c" + using tendsto_eventually by blast + moreover from assms have "f \x\ 0" + by (simp add: isolated_zero_def) + ultimately have [simp]: "c = 0" + using tendsto_unique[of "at x" f c 0] by (simp add: at_neq_bot) + + have "eventually (\x. f x \ 0) (at x)" + using assms by (auto simp: isolated_zero_def) + moreover have "eventually (\x. x \ A) (at x)" + using assms by (intro eventually_at_in_open') auto + ultimately have "eventually (\x. False) (at x)" + by eventually_elim (use c in auto) + thus False + by simp +qed + end diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Complex_Analysis/Weierstrass_Factorization.thy --- a/src/HOL/Complex_Analysis/Weierstrass_Factorization.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Complex_Analysis/Weierstrass_Factorization.thy Wed Apr 16 21:13:33 2025 +0100 @@ -339,8 +339,16 @@ lemma isolated_zero: assumes "z \ range a" shows "isolated_zero f z" - using not_islimpt_range_a[of z] assms - by (auto simp: isolated_zero_altdef zero) +proof - + have "eventually (\z. f z \ 0) (at z)" + using not_islimpt_range_a[of z] by (auto simp: islimpt_iff_eventually zero) + moreover have "f \z\ f z" + by (intro isContD analytic_at_imp_isCont analytic) + hence "f \z\ 0" + using assms zero[of z] by auto + ultimately show ?thesis + by (auto simp: isolated_zero_def) +qed lemma zorder: "zorder f z = card (a -` {z})" proof - @@ -414,7 +422,7 @@ have "zorder (\w. weierstrass_factor (p n) (1 / a n * w)) z = zorder (weierstrass_factor (p n)) (1 / a n * z)" using a_nonzero[of n] eventually_neq_at_within[of 1 "z / a n" UNIV] - by (intro zorder_scale analytic_intros) auto + by (intro zorder_scale analytic_intros analytic_on_imp_meromorphic_on) auto hence "zorder (\w. g w n) z = zorder (weierstrass_factor (p n)) 1" using n a_nonzero[of n] by (auto simp: g_def) thus "zorder (\w. g w n) z = 1" diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Complex_Analysis/Winding_Numbers.thy --- a/src/HOL/Complex_Analysis/Winding_Numbers.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Complex_Analysis/Winding_Numbers.thy Wed Apr 16 21:13:33 2025 +0100 @@ -1185,6 +1185,26 @@ by (intro winding_number_pos_lt [OF valid_path_linepath z assms]) (simp add: linepath_def algebra_simps) qed +lemma winding_number_linepath_neg_lt: + assumes "0 < Im ((a - b) * cnj (a - z))" + shows "Re(winding_number(linepath a b) z) < 0" +proof - + have z: "z \ path_image (linepath a b)" + using assms + by (simp add: closed_segment_def) (force simp: algebra_simps) + have "Re(winding_number(linepath a b) z) = + -Re(winding_number(reversepath (linepath a b)) z)" + by (subst winding_number_reversepath) (use z in auto) + also have "\ = - Re(winding_number(linepath b a) z)" + by simp + finally have "Re (winding_number (linepath a b) z) + = - Re (winding_number (linepath b a) z)" . + moreover have "0 < Re (winding_number (linepath b a) z)" + using winding_number_linepath_pos_lt[OF assms] . + ultimately show ?thesis by auto +qed + + subsection\<^marker>\tag unimportant\ \More winding number properties\ text\including the fact that it's +-1 inside a simple closed curve.\ @@ -2184,6 +2204,12 @@ using simple_closed_path_winding_number_cases by fastforce +lemma simple_closed_path_winding_number_neg: + "\simple_path \; pathfinish \ = pathstart \; z \ path_image \; Re (winding_number \ z) < 0\ + \ winding_number \ z = -1" + using simple_closed_path_winding_number_cases by fastforce + + subsection \Winding number for rectangular paths\ proposition winding_number_rectpath: diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Computational_Algebra/Primes.thy --- a/src/HOL/Computational_Algebra/Primes.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Computational_Algebra/Primes.thy Wed Apr 16 21:13:33 2025 +0100 @@ -542,6 +542,25 @@ shows "d dvd p ^ k \ (\i\k. d = p ^ i)" using assms divides_primepow [of p d k] by (auto intro: le_imp_power_dvd) +lemma gcd_prime_int: + assumes "prime (p :: int)" + shows "gcd p k = (if p dvd k then p else 1)" +proof - + have "p \ 0" + using assms prime_ge_0_int by auto + show ?thesis + proof (cases "p dvd k") + case True + thus ?thesis using assms \p \ 0\ by auto + next + case False + hence "coprime p k" + using assms by (simp add: prime_imp_coprime) + with False show ?thesis + by auto + qed +qed + subsection \Chinese Remainder Theorem Variants\ diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Deriv.thy Wed Apr 16 21:13:33 2025 +0100 @@ -1067,8 +1067,8 @@ by (simp add: DERIV_unique Uniq_def) lemma DERIV_sum[derivative_intros]: - "(\ n. n \ S \ ((\x. f x n) has_field_derivative (f' x n)) F) \ - ((\x. sum (f x) S) has_field_derivative sum (f' x) S) F" + "(\ n. n \ S \ ((\x. f x n) has_field_derivative (f' n)) F) \ + ((\x. sum (f x) S) has_field_derivative sum f' S) F" by (rule has_derivative_imp_has_field_derivative [OF has_derivative_sum]) (auto simp: sum_distrib_left mult_commute_abs dest: has_field_derivative_imp_has_derivative) diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Euclidean_Rings.thy --- a/src/HOL/Euclidean_Rings.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Euclidean_Rings.thy Wed Apr 16 21:13:33 2025 +0100 @@ -1711,6 +1711,9 @@ end +lemma of_int_div: "b dvd a \ of_int (a div b) = (of_int a / of_int b :: 'a :: field_char_0)" + by (elim dvdE) (auto simp: divide_simps mult_ac) + subsubsection \Algebraic foundations\ diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Int.thy --- a/src/HOL/Int.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Int.thy Wed Apr 16 21:13:33 2025 +0100 @@ -935,7 +935,7 @@ lemma Ints_minus [simp]: "a \ \ \ -a \ \" by (force simp add: Ints_def simp flip: of_int_minus intro: range_eqI) -lemma minus_in_Ints_iff: "-x \ \ \ x \ \" +lemma minus_in_Ints_iff [simp]: "-x \ \ \ x \ \" using Ints_minus[of x] Ints_minus[of "-x"] by auto lemma Ints_diff [simp]: "a \ \ \ b \ \ \ a - b \ \" @@ -1079,6 +1079,61 @@ finally show ?thesis . qed +lemma add_in_Ints_iff_left [simp]: "x \ \ \ x + y \ \ \ y \ \" + by (metis Ints_add Ints_diff add_diff_cancel_left') + +lemma add_in_Ints_iff_right [simp]: "y \ \ \ x + y \ \ \ x \ \" + by (subst add.commute) auto + +lemma diff_in_Ints_iff_left [simp]: "x \ \ \ x - y \ \ \ y \ \" + by (metis Ints_diff add_in_Ints_iff_left diff_add_cancel) + +lemma diff_in_Ints_iff_right [simp]: "y \ \ \ x - y \ \ \ x \ \" + by (metis Ints_minus diff_in_Ints_iff_left minus_diff_eq) + +lemmas [simp] = minus_in_Ints_iff + +lemma fraction_not_in_Ints: + assumes "\(n dvd m)" "n \ 0" + shows "of_int m / of_int n \ (\ :: 'a :: {division_ring,ring_char_0} set)" +proof + assume "of_int m / (of_int n :: 'a) \ \" + then obtain k where "of_int m / of_int n = (of_int k :: 'a)" by (elim Ints_cases) + with assms have "of_int m = (of_int (k * n) :: 'a)" by (auto simp add: field_split_simps) + hence "m = k * n" by (subst (asm) of_int_eq_iff) + hence "n dvd m" by simp + with assms(1) show False by contradiction +qed + +lemma of_int_div_of_int_in_Ints_iff: + "(of_int n / of_int m :: 'a :: {division_ring,ring_char_0}) \ \ \ m = 0 \ m dvd n" +proof + assume *: "m = 0 \ m dvd n" + have "of_int n / of_int m \ (\ :: 'a set)" if "m \ 0" "m dvd n" + proof - + from \m dvd n\ obtain k where "n = m * k" + by (elim dvdE) + hence "n = k * m" + by (simp add: mult.commute) + hence "of_int n / (of_int m :: 'a) = of_int k" + using \m \ 0\ by (simp add: field_simps) + also have "\ \ \" + by auto + finally show ?thesis . + qed + with * show "of_int n / of_int m \ (\ :: 'a set)" + by (cases "m = 0") auto +next + assume *: "(of_int n / of_int m :: 'a) \ \" + thus "m = 0 \ m dvd n" + using fraction_not_in_Ints[of m n, where ?'a = 'a] by auto +qed + +lemma fraction_numeral_not_in_Ints [simp]: + assumes "\(numeral b :: int) dvd numeral a" + shows "numeral a / numeral b \ (\ :: 'a :: {division_ring, ring_char_0} set)" + using fraction_not_in_Ints[of "numeral b" "numeral a", where ?'a = 'a] assms by simp + subsection \\<^term>\sum\ and \<^term>\prod\\ @@ -1733,6 +1788,18 @@ by (simp add: ac_simps) qed +lemma fraction_numeral_not_in_Ints' [simp]: + assumes "b \ Num.One" + shows "1 / numeral b \ (\ :: 'a :: {division_ring, ring_char_0} set)" +proof - + have *: "\numeral b dvd (1 :: int)" + using assms by simp + have "of_int 1 / of_int (numeral b) \ (\ :: 'a set)" + by (rule fraction_not_in_Ints) (use * in auto) + thus ?thesis + by simp +qed + subsection \Powers with integer exponents\ diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Library/Nonpos_Ints.thy --- a/src/HOL/Library/Nonpos_Ints.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Library/Nonpos_Ints.thy Wed Apr 16 21:13:33 2025 +0100 @@ -329,19 +329,7 @@ finally show ?thesis . qed -lemma fraction_not_in_ints: - assumes "\(n dvd m)" "n \ 0" - shows "of_int m / of_int n \ (\ :: 'a :: {division_ring,ring_char_0} set)" -proof - assume "of_int m / (of_int n :: 'a) \ \" - then obtain k where "of_int m / of_int n = (of_int k :: 'a)" by (elim Ints_cases) - with assms have "of_int m = (of_int (k * n) :: 'a)" by (auto simp add: field_split_simps) - hence "m = k * n" by (subst (asm) of_int_eq_iff) - hence "n dvd m" by simp - with assms(1) show False by contradiction -qed - -lemma fraction_not_in_nats: +lemma fraction_not_in_Nats: assumes "\n dvd m" "n \ 0" shows "of_int m / of_int n \ (\ :: 'a :: {division_ring,ring_char_0} set)" proof @@ -349,7 +337,7 @@ also note Nats_subset_Ints finally have "of_int m / of_int n \ (\ :: 'a set)" . moreover have "of_int m / of_int n \ (\ :: 'a set)" - using assms by (intro fraction_not_in_ints) + using assms by (intro fraction_not_in_Ints) ultimately show False by contradiction qed @@ -369,7 +357,7 @@ \ (numeral b :: int) dvd numeral a" (is "?L=?R") proof show "?L \ ?R" - by (metis fraction_not_in_ints of_int_numeral zero_neq_numeral) + by (metis fraction_not_in_Ints of_int_numeral zero_neq_numeral) assume ?R then obtain k::int where "numeral a = numeral b * (of_int k :: 'a)" unfolding dvd_def by (metis of_int_mult of_int_numeral) diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Number_Theory/Cong.thy --- a/src/HOL/Number_Theory/Cong.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Number_Theory/Cong.thy Wed Apr 16 21:13:33 2025 +0100 @@ -128,6 +128,46 @@ "[c mod (b * a) = d] (mod a) \ [c = d] (mod a)" using mod_mult_cong_right [of c a b d] by (simp add: ac_simps) +lemma cong_mod_leftI [simp]: + "[b = c] (mod a) \ [b mod a = c] (mod a)" + by (simp add: cong_def) + +lemma cong_mod_rightI [simp]: + "[b = c] (mod a) \ [b = c mod a] (mod a)" + by (simp add: cong_def) + +lemma cong_cmult_leftI: "[a = b] (mod m) \ [c * a = c * b] (mod (c * m))" + by (metis cong_def local.mult_mod_right) + +lemma cong_cmult_rightI: "[a = b] (mod m) \ [a * c = b * c] (mod (m * c))" + using cong_cmult_leftI[of a b m c] by (simp add: mult.commute) + +lemma cong_dvd_mono_modulus: + assumes "[a = b] (mod m)" "m' dvd m" + shows "[a = b] (mod m')" + using assms by (metis cong_def local.mod_mod_cancel) + +lemma coprime_cong_transfer_left: + assumes "coprime a b" "[a = a'] (mod b)" + shows "coprime a' b" + using assms by (metis cong_0 cong_def local.coprime_mod_left_iff) + +lemma coprime_cong_transfer_right: + assumes "coprime a b" "[b = b'] (mod a)" + shows "coprime a b'" + using coprime_cong_transfer_left[of b a b'] assms + by (simp add: coprime_commute) + +lemma coprime_cong_cong_left: + assumes "[a = a'] (mod b)" + shows "coprime a b \ coprime a' b" + using assms cong_sym_eq coprime_cong_transfer_left by blast + +lemma coprime_cong_cong_right: + assumes "[b = b'] (mod a)" + shows "coprime a b \ coprime a b'" + using coprime_cong_cong_left[OF assms] by (simp add: coprime_commute) + end context unique_euclidean_ring @@ -200,6 +240,9 @@ "[x = y] (mod m)" if "[x = y] (mod m * n)" using that by (simp add: cong_iff_dvd_diff) (rule dvd_mult_left) +lemma cong_uminus: "[x = y] (mod m) \ [-x = -y] (mod m)" + unfolding cong_minus_minus_iff . + end lemma cong_abs [simp]: diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Number_Theory/Modular_Inverse.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Number_Theory/Modular_Inverse.thy Wed Apr 16 21:13:33 2025 +0100 @@ -0,0 +1,143 @@ +section \Modular Inverses\ +theory Modular_Inverse + imports Cong "HOL-Library.FuncSet" +begin + +text \ + The following returns the unique number $m$ such that $mn \equiv 1\pmod{p}$ if there is one, + i.e.\ if $n$ and $p$ are coprime, and otherwise $0$ by convention. +\ +definition modular_inverse where + "modular_inverse p n = (if coprime p n then fst (bezout_coefficients n p) mod p else 0)" + +lemma cong_modular_inverse1: + assumes "coprime n p" + shows "[n * modular_inverse p n = 1] (mod p)" +proof - + have "[fst (bezout_coefficients n p) * n + snd (bezout_coefficients n p) * p = + modular_inverse p n * n + 0] (mod p)" + unfolding modular_inverse_def using assms + by (intro cong_add cong_mult) (auto simp: Cong.cong_def coprime_commute) + also have "fst (bezout_coefficients n p) * n + snd (bezout_coefficients n p) * p = gcd n p" + by (simp add: bezout_coefficients_fst_snd) + also have "\ = 1" + using assms by simp + finally show ?thesis + by (simp add: cong_sym mult_ac) +qed + +lemma cong_modular_inverse2: + assumes "coprime n p" + shows "[modular_inverse p n * n = 1] (mod p)" + using cong_modular_inverse1[OF assms] by (simp add: mult.commute) + +lemma coprime_modular_inverse [simp, intro]: + fixes n :: "'a :: {euclidean_ring_gcd,unique_euclidean_semiring}" + assumes "coprime n p" + shows "coprime (modular_inverse p n) p" + using cong_modular_inverse1[OF assms] assms + by (meson cong_imp_coprime cong_sym coprime_1_left coprime_mult_left_iff) + +lemma modular_inverse_int_nonneg: "p > 0 \ modular_inverse p (n :: int) \ 0" + by (simp add: modular_inverse_def) + +lemma modular_inverse_int_less: "p > 0 \ modular_inverse p (n :: int) < p" + by (simp add: modular_inverse_def) + +lemma modular_inverse_int_eqI: + fixes x y :: int + assumes "y \ {0.. = 1 * y] (mod m)" + using \coprime x m\ by (intro cong_mult cong_refl cong_modular_inverse2) + finally have "[modular_inverse m x = y] (mod m)" + by simp + thus "modular_inverse m x = y" + using assms by (simp add: Cong.cong_def modular_inverse_def) +qed + +lemma modular_inverse_1 [simp]: + assumes "m > (1 :: int)" + shows "modular_inverse m 1 = 1" + by (rule modular_inverse_int_eqI) (use assms in auto) + +lemma modular_inverse_int_mult: + fixes x y :: int + assumes "coprime x m" "coprime y m" "m > 0" + shows "modular_inverse m (x * y) = (modular_inverse m y * modular_inverse m x) mod m" +proof (rule modular_inverse_int_eqI) + show "modular_inverse m y * modular_inverse m x mod m \ {0.. = 1 * 1] (mod m)" + by (intro cong_mult cong_modular_inverse1 assms) + finally show "[x * y * (modular_inverse m y * modular_inverse m x mod m) = 1] (mod m)" + by simp +qed + +lemma bij_betw_int_remainders_mult: + fixes a n :: int + assumes a: "coprime a n" + shows "bij_betw (\m. a * m mod n) {1.. a * m mod n \ {1.. {1..n dvd (a * m)" + using m by (simp add: coprime_commute coprime_dvd_mult_right_iff zdvd_not_zless) + hence "a * m mod n > 0" + using m order_le_less by fastforce + thus "a * m mod n \ {1..m. a' * m mod n"]) auto +qed + +lemma mult_modular_inverse_of_not_coprime [simp]: "\coprime a m \ modular_inverse m a = 0" + by (simp add: coprime_commute modular_inverse_def) + +lemma mult_modular_inverse_eq_0_iff: + fixes a :: "'a :: {unique_euclidean_semiring, euclidean_ring_gcd}" + shows "\is_unit m \ modular_inverse m a = 0 \ \coprime a m" + by (metis coprime_modular_inverse mult_modular_inverse_of_not_coprime coprime_0_left_iff) + +lemma mult_modular_inverse_int_pos: "m > 1 \ coprime a m \ modular_inverse m a > (0 :: int)" + by (simp add: modular_inverse_int_nonneg mult_modular_inverse_eq_0_iff order.strict_iff_order) + +lemma abs_mult_modular_inverse_int_less: "m \ 0 \ \modular_inverse m a :: int\ < \m\" + by (auto simp: modular_inverse_def intro!: abs_mod_less) + +lemma modular_inverse_int_less': "m \ 0 \ (modular_inverse m a :: int) < \m\" + using abs_mult_modular_inverse_int_less[of m a] by linarith + +end \ No newline at end of file diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Number_Theory/Number_Theory.thy --- a/src/HOL/Number_Theory/Number_Theory.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Number_Theory/Number_Theory.thy Wed Apr 16 21:13:33 2025 +0100 @@ -11,6 +11,7 @@ Pocklington Prime_Powers Residue_Primitive_Roots + Modular_Inverse begin end diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Power.thy --- a/src/HOL/Power.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Power.thy Wed Apr 16 21:13:33 2025 +0100 @@ -836,6 +836,19 @@ using assms by (metis add.inverse_inverse linear mult_le_one neg_equal_0_iff_equal neg_le_iff_le power2_eq_square power_minus_Bit0) +lemma power2_mono: "\x\ \ \y\ \ x ^ 2 \ y ^ 2" + by (simp add: abs_le_square_iff) + +lemma power2_strict_mono: + assumes "\x\ < \y\" + shows "x ^ 2 < y ^ 2" +proof - + have "\x\ ^ 2 < \y\ ^ 2" + by (rule power_strict_mono) (use assms in auto) + thus ?thesis + by simp +qed + end subsection \Miscellaneous rules\ diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Rings.thy Wed Apr 16 21:13:33 2025 +0100 @@ -422,6 +422,15 @@ then show "- x dvd y" .. qed +lemma dvd_diff_right_iff: + assumes "a dvd b" + shows "a dvd b - c \ a dvd c" (is "?P \ ?Q") + using dvd_add_right_iff[of a b "-c"] assms by auto + +lemma dvd_diff_left_iff: + shows "a dvd c \ a dvd b - c \ a dvd b" + using dvd_add_left_iff[of a "-c" b] by auto + lemma dvd_diff [simp]: "x dvd y \ x dvd z \ x dvd (y - z)" using dvd_add [of x y "- z"] by simp diff -r 1b17f0a41aa3 -r 819688d4cc45 src/HOL/Vector_Spaces.thy --- a/src/HOL/Vector_Spaces.thy Wed Apr 16 21:13:27 2025 +0100 +++ b/src/HOL/Vector_Spaces.thy Wed Apr 16 21:13:33 2025 +0100 @@ -75,6 +75,19 @@ and linear_scale_left = module_hom_scale_left and linear_uminus = module_hom_uminus +lemma linear_representation: + assumes "independent B" "span B = UNIV" + shows "linear scale (*) (\v. representation B v b)" +proof (unfold_locales, goal_cases) + case (5 x y) + show ?case + using assms by (subst representation_add) auto +next + case (6 r x) + show ?case + using assms by (subst representation_scale) auto +qed (simp_all add: algebra_simps) + lemma linear_imp_scale: fixes D::"'a \ 'b" assumes "linear (*) scale D"