# HG changeset patch # User paulson # Date 1675779008 0 # Node ID 0cdb384bf56a5ed4246689c9e7b0da333622eea8 # Parent 8f2e6186408f742cad316846deb482f0d7bdaf18 More new theorems from the number theory development diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Analysis/Complex_Transcendental.thy --- a/src/HOL/Analysis/Complex_Transcendental.thy Mon Feb 06 15:41:23 2023 +0000 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Feb 07 14:10:08 2023 +0000 @@ -245,6 +245,22 @@ shows "(\x. cos (f x)) holomorphic_on A" using holomorphic_on_compose[OF assms holomorphic_on_cos] by (simp add: o_def) +lemma analytic_on_sin [analytic_intros]: "sin analytic_on A" + using analytic_on_holomorphic holomorphic_on_sin by blast + +lemma analytic_on_sin' [analytic_intros]: + "f analytic_on A \ (\z. z \ A \ f z \ range (\n. complex_of_real pi * of_int n)) \ + (\z. sin (f z)) analytic_on A" + using analytic_on_compose_gen[OF _ analytic_on_sin[of UNIV], of f A] by (simp add: o_def) + +lemma analytic_on_cos [analytic_intros]: "cos analytic_on A" + using analytic_on_holomorphic holomorphic_on_cos by blast + +lemma analytic_on_cos' [analytic_intros]: + "f analytic_on A \ (\z. z \ A \ f z \ range (\n. complex_of_real pi * of_int n)) \ + (\z. cos (f z)) analytic_on A" + using analytic_on_compose_gen[OF _ analytic_on_cos[of UNIV], of f A] by (simp add: o_def) + subsection\<^marker>\tag unimportant\\More on the Polar Representation of Complex Numbers\ lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)" @@ -3160,6 +3176,9 @@ by simp qed +lemma csqrt_conv_powr: "csqrt z = z powr (1/2)" + by (auto simp: csqrt_exp_Ln powr_def) + lemma csqrt_mult: assumes "Arg z + Arg w \ {-pi<..pi}" shows "csqrt (z * w) = csqrt z * csqrt w" @@ -3237,12 +3256,27 @@ by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_csqrt) lemma continuous_on_csqrt [continuous_intros]: - "(\z. z \ s \ z \ \\<^sub>\\<^sub>0) \ continuous_on s csqrt" + "continuous_on (-\\<^sub>\\<^sub>0) csqrt" by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt) -lemma holomorphic_on_csqrt: - "(\z. z \ s \ z \ \\<^sub>\\<^sub>0) \ csqrt holomorphic_on s" - by (simp add: field_differentiable_within_csqrt holomorphic_on_def) +lemma holomorphic_on_csqrt [holomorphic_intros]: "csqrt holomorphic_on -\\<^sub>\\<^sub>0" +proof - + have *: "(\z. exp (ln z / 2)) holomorphic_on -\\<^sub>\\<^sub>0" + by (intro holomorphic_intros) auto + then show ?thesis + using field_differentiable_within_csqrt holomorphic_on_def by auto +qed + +lemma holomorphic_on_csqrt' [holomorphic_intros]: + "f holomorphic_on A \ (\z. z \ A \ f z \ \\<^sub>\\<^sub>0) \ (\z. csqrt (f z)) holomorphic_on A" + using holomorphic_on_compose_gen[OF _ holomorphic_on_csqrt, of f A] by (auto simp: o_def) + +lemma analytic_on_csqrt [analytic_intros]: "csqrt analytic_on -\\<^sub>\\<^sub>0" + using holomorphic_on_csqrt by (subst analytic_on_open) auto + +lemma analytic_on_csqrt' [analytic_intros]: + "f analytic_on A \ (\z. z \ A \ f z \ \\<^sub>\\<^sub>0) \ (\z. csqrt (f z)) analytic_on A" + using analytic_on_compose_gen[OF _ analytic_on_csqrt, of f A] by (auto simp: o_def) lemma continuous_within_closed_nontrivial: "closed s \ a \ s ==> continuous (at a within s) f" diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Analysis/FPS_Convergence.thy --- a/src/HOL/Analysis/FPS_Convergence.thy Mon Feb 06 15:41:23 2023 +0000 +++ b/src/HOL/Analysis/FPS_Convergence.thy Tue Feb 07 14:10:08 2023 +0000 @@ -624,6 +624,10 @@ named_theorems fps_expansion_intros +lemma has_fps_expansion_schematicI: + "f has_fps_expansion A \ A = B \ f has_fps_expansion B" + by simp + lemma fps_nth_fps_expansion: fixes f :: "complex \ complex" assumes "f has_fps_expansion F" diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Feb 06 15:41:23 2023 +0000 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Feb 07 14:10:08 2023 +0000 @@ -105,7 +105,7 @@ by (intro enn2real_mono emeasure_mono) (auto simp: emeasure_lborel_cbox_eq) lemma content_lt_nz: "0 < content (cbox a b) \ content (cbox a b) \ 0" - unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce + by (fact zero_less_measure_iff) lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)" unfolding measure_lborel_cbox_eq Basis_prod_def @@ -534,11 +534,23 @@ shows "(f has_integral y) S \ ((\x. f x * c) has_integral (y * c)) S" using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def) +lemma integrable_on_mult_left: + fixes c :: "'a :: real_normed_algebra" + assumes "f integrable_on A" + shows "(\x. f x * c) integrable_on A" + using assms has_integral_mult_left by blast + lemma has_integral_divide: fixes c :: "_ :: real_normed_div_algebra" shows "(f has_integral y) S \ ((\x. f x / c) has_integral (y / c)) S" unfolding divide_inverse by (simp add: has_integral_mult_left) +lemma integrable_on_divide: + fixes c :: "'a :: real_normed_div_algebra" + assumes "f integrable_on A" + shows "(\x. f x / c) integrable_on A" + using assms has_integral_divide by blast + text\The case analysis eliminates the condition \<^term>\f integrable_on S\ at the cost of the type class constraint \division_ring\\ corollary integral_mult_left [simp]: @@ -567,9 +579,35 @@ lemma has_integral_mult_right: fixes c :: "'a :: real_normed_algebra" - shows "(f has_integral y) i \ ((\x. c * f x) has_integral (c * y)) i" + shows "(f has_integral y) A \ ((\x. c * f x) has_integral (c * y)) A" using has_integral_linear[OF _ bounded_linear_mult_right] by (simp add: comp_def) +lemma integrable_on_mult_right: + fixes c :: "'a :: real_normed_algebra" + assumes "f integrable_on A" + shows "(\x. c * f x) integrable_on A" + using assms has_integral_mult_right by blast + +lemma integrable_on_mult_right_iff [simp]: + fixes c :: "'a :: real_normed_field" + assumes "c \ 0" + shows "(\x. c * f x) integrable_on A \ f integrable_on A" + using integrable_on_mult_right[of f A c] + integrable_on_mult_right[of "\x. c * f x" A "inverse c"] assms + by (auto simp: field_simps) + +lemma integrable_on_mult_left_iff [simp]: + fixes c :: "'a :: real_normed_field" + assumes "c \ 0" + shows "(\x. f x * c) integrable_on A \ f integrable_on A" + using integrable_on_mult_right_iff[OF assms, of f A] by (simp add: mult.commute) + +lemma integrable_on_div_iff [simp]: + fixes c :: "'a :: real_normed_field" + assumes "c \ 0" + shows "(\x. f x / c) integrable_on A \ f integrable_on A" + using integrable_on_mult_right_iff[of "inverse c" f A] assms by (simp add: field_simps) + lemma has_integral_cmul: "(f has_integral k) S \ ((\x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) S" unfolding o_def[symmetric] by (metis has_integral_linear bounded_linear_scaleR_right) @@ -578,14 +616,7 @@ fixes c :: real assumes "c \ 0 \ (f has_integral x) A" shows "((\x. c * f x) has_integral c * x) A" -proof (cases "c = 0") - case True - then show ?thesis by simp -next - case False - from has_integral_cmul[OF assms[OF this], of c] show ?thesis - unfolding real_scaleR_def . -qed + by (metis assms has_integral_is_0 has_integral_mult_right lambda_zero) lemma has_integral_neg: "(f has_integral k) S \ ((\x. -(f x)) has_integral -k) S" by (drule_tac c="-1" in has_integral_cmul) auto @@ -5028,6 +5059,15 @@ shows "integral(box a b) f = integral(cbox a b) f" by (metis has_integral_integrable_integral has_integral_open_interval not_integrable_integral) +lemma integrable_on_open_interval_real: + fixes f :: "real \ 'b :: banach" + shows "f integrable_on {a<.. f integrable_on {a..b}" + using integrable_on_open_interval[of f a b] by simp + +lemma integral_open_interval_real: + "integral {a..b} (f :: real \ 'a :: banach) = integral {a<..<(b::real)} f" + using integral_open_interval[of a b f] by simp + lemma has_integral_Icc_iff_Ioo: fixes f :: "real \ 'a :: banach" shows "(f has_integral I) {a..b} \ (f has_integral I) {a<.. S \ outside S" by (metis assms closed_open closure_minimal inside_outside open_inside sup_ge2) +lemma closed_path_image_Un_inside: + fixes g :: "real \ 'a :: real_normed_vector" + assumes "path g" + shows "closed (path_image g \ inside (path_image g))" + by (simp add: assms closed_Compl closed_path_image open_outside union_with_inside) + lemma frontier_outside_subset: fixes S :: "'a::real_normed_vector set" assumes "closed S" diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Complex.thy --- a/src/HOL/Complex.thy Mon Feb 06 15:41:23 2023 +0000 +++ b/src/HOL/Complex.thy Tue Feb 07 14:10:08 2023 +0000 @@ -1297,6 +1297,11 @@ field_simps real_sqrt_mult[symmetric] real_sqrt_divide) qed +lemma csqrt_power_even: + assumes "even n" + shows "csqrt z ^ n = z ^ (n div 2)" + by (metis assms dvd_mult_div_cancel power2_csqrt power_mult) + lemma norm_csqrt [simp]: "norm (csqrt z) = sqrt (norm z)" by (metis abs_of_nonneg norm_ge_zero norm_mult power2_csqrt power2_eq_square real_sqrt_abs) diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Filter.thy --- a/src/HOL/Filter.thy Mon Feb 06 15:41:23 2023 +0000 +++ b/src/HOL/Filter.thy Tue Feb 07 14:10:08 2023 +0000 @@ -1287,6 +1287,10 @@ translations "LIM x F1. f :> F2" == "CONST filterlim (\x. f) F2 F1" +lemma filterlim_filtercomapI: "filterlim f F G \ filterlim (\x. f (g x)) F (filtercomap g G)" + unfolding filterlim_def + by (metis order_trans filtermap_filtercomap filtermap_filtermap filtermap_mono) + lemma filterlim_top [simp]: "filterlim f top F" by (simp add: filterlim_def) diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Limits.thy --- a/src/HOL/Limits.thy Mon Feb 06 15:41:23 2023 +0000 +++ b/src/HOL/Limits.thy Tue Feb 07 14:10:08 2023 +0000 @@ -1270,6 +1270,13 @@ shows "continuous_on s (\x. power_int (f x) n)" using assms unfolding continuous_on_def by (blast intro: tendsto_power_int) +lemma tendsto_power_int' [tendsto_intros]: + fixes a :: "'a::real_normed_div_algebra" + assumes f: "(f \ a) F" + and a: "a \ 0 \ n \ 0" + shows "((\x. power_int (f x) n) \ power_int a n) F" + using assms by (cases n rule: int_cases4) (auto intro!: tendsto_intros simp: power_int_minus) + lemma tendsto_sgn [tendsto_intros]: "(f \ l) F \ l \ 0 \ ((\x. sgn (f x)) \ sgn l) F" for l :: "'a::real_normed_vector" unfolding sgn_div_norm by (simp add: tendsto_intros) @@ -1782,6 +1789,22 @@ by (subst filterlim_inverse_at_iff[symmetric]) simp_all qed +lemma filterlim_power_int_neg_at_infinity: + fixes f :: "_ \ 'a::{real_normed_div_algebra, division_ring}" + assumes "n < 0" and lim: "(f \ 0) F" and ev: "eventually (\x. f x \ 0) F" + shows "filterlim (\x. f x powi n) at_infinity F" +proof - + have lim': "((\x. f x ^ nat (- n)) \ 0) F" + by (rule tendsto_eq_intros lim)+ (use \n < 0\ in auto) + have ev': "eventually (\x. f x ^ nat (-n) \ 0) F" + using ev by eventually_elim (use \n < 0\ in auto) + have "filterlim (\x. inverse (f x ^ nat (-n))) at_infinity F" + by (intro filterlim_compose[OF filterlim_inverse_at_infinity]) + (use lim' ev' in \auto simp: filterlim_at\) + thus ?thesis + using \n < 0\ by (simp add: power_int_def power_inverse) +qed + lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \ ((\x. inverse (f x) :: real) \ 0) F" by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff) @@ -1937,6 +1960,13 @@ using c filterlim_tendsto_pos_mult_at_top[of "\x. - f x" "- c" F, OF _ _ g] unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp + +lemma filterlim_cmult_at_bot_at_top: + assumes "filterlim (h :: _ \ real) at_top F" "c \ 0" "G = (if c > 0 then at_top else at_bot)" + shows "filterlim (\x. c * h x) G F" + using assms filterlim_tendsto_pos_mult_at_top[OF tendsto_const[of c], of h F] + filterlim_tendsto_neg_mult_at_bot[OF tendsto_const[of c], of h F] by simp + lemma filterlim_pow_at_top: fixes f :: "'a \ real" assumes "0 < n" @@ -2688,10 +2718,9 @@ assumes "0 \ x" "x < 1" shows "(\n. x ^ n) \ 0" proof (cases "x = 0") - case False - with \0 \ x\ have x0: "0 < x" by simp - then have "1 < inverse x" - using \x < 1\ by (rule one_less_inverse) + case False + with \0 \ x\ have "1 < inverse x" + using \x < 1\ by (simp add: one_less_inverse) then have "(\n. inverse (inverse x ^ n)) \ 0" by (rule LIMSEQ_inverse_realpow_zero) then show ?thesis by (simp add: power_inverse) diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Mon Feb 06 15:41:23 2023 +0000 +++ b/src/HOL/Real_Vector_Spaces.thy Tue Feb 07 14:10:08 2023 +0000 @@ -986,6 +986,9 @@ for a b :: "'a::{real_normed_field,field}" by (simp add: divide_inverse norm_mult norm_inverse) +lemma dist_divide_right: "dist (a/c) (b/c) = dist a b / norm c" for c :: "'a :: real_normed_field" + by (metis diff_divide_distrib dist_norm norm_divide) + lemma norm_inverse_le_norm: fixes x :: "'a::real_normed_div_algebra" shows "r \ norm x \ 0 < r \ norm (inverse x) \ inverse r" @@ -1134,7 +1137,6 @@ finally show ?thesis . qed - subsection \Metric spaces\ class metric_space = uniformity_dist + open_uniformity + diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Series.thy --- a/src/HOL/Series.thy Mon Feb 06 15:41:23 2023 +0000 +++ b/src/HOL/Series.thy Tue Feb 07 14:10:08 2023 +0000 @@ -860,6 +860,26 @@ end +text \Application to convergence of the log function\ +lemma norm_summable_ln_series: + fixes z :: "'a :: {real_normed_field, banach}" + assumes "norm z < 1" + shows "summable (\n. norm (z ^ n / of_nat n))" +proof (rule summable_comparison_test) + show "summable (\n. norm (z ^ n))" + using assms unfolding norm_power by (intro summable_geometric) auto + have "norm z ^ n / real n \ norm z ^ n" for n + proof (cases "n = 0") + case False + hence "norm z ^ n * 1 \ norm z ^ n * real n" + by (intro mult_left_mono) auto + thus ?thesis + using False by (simp add: field_simps) + qed auto + thus "\N. \n\N. norm (norm (z ^ n / of_nat n)) \ norm (z ^ n)" + by (intro exI[of _ 0]) (auto simp: norm_power norm_divide) +qed + text \Relations among convergence and absolute convergence for power series.\ diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Mon Feb 06 15:41:23 2023 +0000 +++ b/src/HOL/Transcendental.thy Tue Feb 07 14:10:08 2023 +0000 @@ -6731,14 +6731,6 @@ subsubsection \More specific properties of the real functions\ -lemma sinh_real_zero_iff [simp]: "sinh (x::real) = 0 \ x = 0" -proof - - have "(-1 :: real) < 0" by simp - also have "0 < exp x" by simp - finally have "exp x \ -1" by (intro notI) simp - thus ?thesis by (subst sinh_zero_iff) simp -qed - lemma plus_inverse_ge_2: fixes x :: real assumes "x > 0" @@ -6773,21 +6765,6 @@ lemma cosh_real_nonzero [simp]: "cosh (x :: real) \ 0" using cosh_real_ge_1[of x] by simp -lemma tanh_real_nonneg_iff [simp]: "tanh (x :: real) \ 0 \ x \ 0" - by (simp add: tanh_def field_simps) - -lemma tanh_real_pos_iff [simp]: "tanh (x :: real) > 0 \ x > 0" - by (simp add: tanh_def field_simps) - -lemma tanh_real_nonpos_iff [simp]: "tanh (x :: real) \ 0 \ x \ 0" - by (simp add: tanh_def field_simps) - -lemma tanh_real_neg_iff [simp]: "tanh (x :: real) < 0 \ x < 0" - by (simp add: tanh_def field_simps) - -lemma tanh_real_zero_iff [simp]: "tanh (x :: real) = 0 \ x = 0" - by (simp add: tanh_def field_simps) - lemma arsinh_real_def: "arsinh (x::real) = ln (x + sqrt (x^2 + 1))" by (simp add: arsinh_def powr_half_sqrt) @@ -6860,8 +6837,29 @@ finally show ?thesis . qed +lemma sinh_real_zero_iff [simp]: "sinh x = 0 \ x = 0" + by (metis arsinh_0 arsinh_sinh_real sinh_0) + +lemma cosh_real_one_iff [simp]: "cosh x = 1 \ x = 0" + by (smt (verit, best) Transcendental.arcosh_cosh_real cosh_0 cosh_minus) + +lemma tanh_real_nonneg_iff [simp]: "tanh x \ 0 \ x \ 0" + by (simp add: tanh_def field_simps) + +lemma tanh_real_pos_iff [simp]: "tanh x > 0 \ x > 0" + by (simp add: tanh_def field_simps) + +lemma tanh_real_nonpos_iff [simp]: "tanh x \ 0 \ x \ 0" + by (simp add: tanh_def field_simps) + +lemma tanh_real_neg_iff [simp]: "tanh x < 0 \ x < 0" + by (simp add: tanh_def field_simps) + +lemma tanh_real_zero_iff [simp]: "tanh x = 0 \ x = 0" + by (simp add: tanh_def field_simps) + end - + lemma sinh_real_strict_mono: "strict_mono (sinh :: real \ real)" by (rule pos_deriv_imp_strict_mono derivative_intros)+ auto