--- a/src/HOL/Analysis/Complex_Transcendental.thy Mon Feb 06 21:32:22 2023 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Feb 07 14:10:15 2023 +0000
@@ -245,6 +245,22 @@
shows "(\<lambda>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 \<Longrightarrow> (\<And>z. z \<in> A \<Longrightarrow> f z \<notin> range (\<lambda>n. complex_of_real pi * of_int n)) \<Longrightarrow>
+ (\<lambda>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 \<Longrightarrow> (\<And>z. z \<in> A \<Longrightarrow> f z \<notin> range (\<lambda>n. complex_of_real pi * of_int n)) \<Longrightarrow>
+ (\<lambda>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>\<open>tag unimportant\<close>\<open>More on the Polar Representation of Complex Numbers\<close>
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 \<in> {-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]:
- "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s csqrt"
+ "continuous_on (-\<real>\<^sub>\<le>\<^sub>0) csqrt"
by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
-lemma holomorphic_on_csqrt:
- "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> csqrt holomorphic_on s"
- by (simp add: field_differentiable_within_csqrt holomorphic_on_def)
+lemma holomorphic_on_csqrt [holomorphic_intros]: "csqrt holomorphic_on -\<real>\<^sub>\<le>\<^sub>0"
+proof -
+ have *: "(\<lambda>z. exp (ln z / 2)) holomorphic_on -\<real>\<^sub>\<le>\<^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 \<Longrightarrow> (\<And>z. z \<in> A \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> (\<lambda>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 -\<real>\<^sub>\<le>\<^sub>0"
+ using holomorphic_on_csqrt by (subst analytic_on_open) auto
+
+lemma analytic_on_csqrt' [analytic_intros]:
+ "f analytic_on A \<Longrightarrow> (\<And>z. z \<in> A \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> (\<lambda>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 \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
--- a/src/HOL/Analysis/FPS_Convergence.thy Mon Feb 06 21:32:22 2023 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy Tue Feb 07 14:10:15 2023 +0000
@@ -624,6 +624,10 @@
named_theorems fps_expansion_intros
+lemma has_fps_expansion_schematicI:
+ "f has_fps_expansion A \<Longrightarrow> A = B \<Longrightarrow> f has_fps_expansion B"
+ by simp
+
lemma fps_nth_fps_expansion:
fixes f :: "complex \<Rightarrow> complex"
assumes "f has_fps_expansion F"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Feb 06 21:32:22 2023 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Feb 07 14:10:15 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) \<longleftrightarrow> content (cbox a b) \<noteq> 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 \<Longrightarrow> ((\<lambda>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 "(\<lambda>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 \<Longrightarrow> ((\<lambda>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 "(\<lambda>x. f x / c) integrable_on A"
+ using assms has_integral_divide by blast
+
text\<open>The case analysis eliminates the condition \<^term>\<open>f integrable_on S\<close> at the cost
of the type class constraint \<open>division_ring\<close>\<close>
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 \<Longrightarrow> ((\<lambda>x. c * f x) has_integral (c * y)) i"
+ shows "(f has_integral y) A \<Longrightarrow> ((\<lambda>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 "(\<lambda>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 \<noteq> 0"
+ shows "(\<lambda>x. c * f x) integrable_on A \<longleftrightarrow> f integrable_on A"
+ using integrable_on_mult_right[of f A c]
+ integrable_on_mult_right[of "\<lambda>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 \<noteq> 0"
+ shows "(\<lambda>x. f x * c) integrable_on A \<longleftrightarrow> 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 \<noteq> 0"
+ shows "(\<lambda>x. f x / c) integrable_on A \<longleftrightarrow> 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 \<Longrightarrow> ((\<lambda>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 \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
shows "((\<lambda>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 \<Longrightarrow> ((\<lambda>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 \<Rightarrow> 'b :: banach"
+ shows "f integrable_on {a<..<b} \<longleftrightarrow> 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 \<Rightarrow> '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 \<Rightarrow> 'a :: banach"
shows "(f has_integral I) {a..b} \<longleftrightarrow> (f has_integral I) {a<..<b}"
--- a/src/HOL/Analysis/Path_Connected.thy Mon Feb 06 21:32:22 2023 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Tue Feb 07 14:10:15 2023 +0000
@@ -3375,6 +3375,12 @@
shows "closure(outside S) \<subseteq> S \<union> outside S"
by (metis assms closed_open closure_minimal inside_outside open_inside sup_ge2)
+lemma closed_path_image_Un_inside:
+ fixes g :: "real \<Rightarrow> 'a :: real_normed_vector"
+ assumes "path g"
+ shows "closed (path_image g \<union> 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"
--- a/src/HOL/Complex.thy Mon Feb 06 21:32:22 2023 +0100
+++ b/src/HOL/Complex.thy Tue Feb 07 14:10:15 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)
--- a/src/HOL/Filter.thy Mon Feb 06 21:32:22 2023 +0100
+++ b/src/HOL/Filter.thy Tue Feb 07 14:10:15 2023 +0000
@@ -1287,6 +1287,10 @@
translations
"LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"
+lemma filterlim_filtercomapI: "filterlim f F G \<Longrightarrow> filterlim (\<lambda>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)
--- a/src/HOL/Limits.thy Mon Feb 06 21:32:22 2023 +0100
+++ b/src/HOL/Limits.thy Tue Feb 07 14:10:15 2023 +0000
@@ -1270,6 +1270,13 @@
shows "continuous_on s (\<lambda>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 \<longlongrightarrow> a) F"
+ and a: "a \<noteq> 0 \<or> n \<ge> 0"
+ shows "((\<lambda>x. power_int (f x) n) \<longlongrightarrow> 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 \<longlongrightarrow> l) F \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> ((\<lambda>x. sgn (f x)) \<longlongrightarrow> 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 :: "_ \<Rightarrow> 'a::{real_normed_div_algebra, division_ring}"
+ assumes "n < 0" and lim: "(f \<longlongrightarrow> 0) F" and ev: "eventually (\<lambda>x. f x \<noteq> 0) F"
+ shows "filterlim (\<lambda>x. f x powi n) at_infinity F"
+proof -
+ have lim': "((\<lambda>x. f x ^ nat (- n)) \<longlongrightarrow> 0) F"
+ by (rule tendsto_eq_intros lim)+ (use \<open>n < 0\<close> in auto)
+ have ev': "eventually (\<lambda>x. f x ^ nat (-n) \<noteq> 0) F"
+ using ev by eventually_elim (use \<open>n < 0\<close> in auto)
+ have "filterlim (\<lambda>x. inverse (f x ^ nat (-n))) at_infinity F"
+ by (intro filterlim_compose[OF filterlim_inverse_at_infinity])
+ (use lim' ev' in \<open>auto simp: filterlim_at\<close>)
+ thus ?thesis
+ using \<open>n < 0\<close> by (simp add: power_int_def power_inverse)
+qed
+
lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 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 "\<lambda>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 :: _ \<Rightarrow> real) at_top F" "c \<noteq> 0" "G = (if c > 0 then at_top else at_bot)"
+ shows "filterlim (\<lambda>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 \<Rightarrow> real"
assumes "0 < n"
@@ -2688,10 +2718,9 @@
assumes "0 \<le> x" "x < 1"
shows "(\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
proof (cases "x = 0")
- case False
- with \<open>0 \<le> x\<close> have x0: "0 < x" by simp
- then have "1 < inverse x"
- using \<open>x < 1\<close> by (rule one_less_inverse)
+ case False
+ with \<open>0 \<le> x\<close> have "1 < inverse x"
+ using \<open>x < 1\<close> by (simp add: one_less_inverse)
then have "(\<lambda>n. inverse (inverse x ^ n)) \<longlonglongrightarrow> 0"
by (rule LIMSEQ_inverse_realpow_zero)
then show ?thesis by (simp add: power_inverse)
--- a/src/HOL/Real_Vector_Spaces.thy Mon Feb 06 21:32:22 2023 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Feb 07 14:10:15 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 \<le> norm x \<Longrightarrow> 0 < r \<Longrightarrow> norm (inverse x) \<le> inverse r"
@@ -1134,7 +1137,6 @@
finally show ?thesis .
qed
-
subsection \<open>Metric spaces\<close>
class metric_space = uniformity_dist + open_uniformity +
--- a/src/HOL/Series.thy Mon Feb 06 21:32:22 2023 +0100
+++ b/src/HOL/Series.thy Tue Feb 07 14:10:15 2023 +0000
@@ -860,6 +860,26 @@
end
+text \<open>Application to convergence of the log function\<close>
+lemma norm_summable_ln_series:
+ fixes z :: "'a :: {real_normed_field, banach}"
+ assumes "norm z < 1"
+ shows "summable (\<lambda>n. norm (z ^ n / of_nat n))"
+proof (rule summable_comparison_test)
+ show "summable (\<lambda>n. norm (z ^ n))"
+ using assms unfolding norm_power by (intro summable_geometric) auto
+ have "norm z ^ n / real n \<le> norm z ^ n" for n
+ proof (cases "n = 0")
+ case False
+ hence "norm z ^ n * 1 \<le> norm z ^ n * real n"
+ by (intro mult_left_mono) auto
+ thus ?thesis
+ using False by (simp add: field_simps)
+ qed auto
+ thus "\<exists>N. \<forall>n\<ge>N. norm (norm (z ^ n / of_nat n)) \<le> norm (z ^ n)"
+ by (intro exI[of _ 0]) (auto simp: norm_power norm_divide)
+qed
+
text \<open>Relations among convergence and absolute convergence for power series.\<close>
--- a/src/HOL/Transcendental.thy Mon Feb 06 21:32:22 2023 +0100
+++ b/src/HOL/Transcendental.thy Tue Feb 07 14:10:15 2023 +0000
@@ -6731,14 +6731,6 @@
subsubsection \<open>More specific properties of the real functions\<close>
-lemma sinh_real_zero_iff [simp]: "sinh (x::real) = 0 \<longleftrightarrow> x = 0"
-proof -
- have "(-1 :: real) < 0" by simp
- also have "0 < exp x" by simp
- finally have "exp x \<noteq> -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) \<noteq> 0"
using cosh_real_ge_1[of x] by simp
-lemma tanh_real_nonneg_iff [simp]: "tanh (x :: real) \<ge> 0 \<longleftrightarrow> x \<ge> 0"
- by (simp add: tanh_def field_simps)
-
-lemma tanh_real_pos_iff [simp]: "tanh (x :: real) > 0 \<longleftrightarrow> x > 0"
- by (simp add: tanh_def field_simps)
-
-lemma tanh_real_nonpos_iff [simp]: "tanh (x :: real) \<le> 0 \<longleftrightarrow> x \<le> 0"
- by (simp add: tanh_def field_simps)
-
-lemma tanh_real_neg_iff [simp]: "tanh (x :: real) < 0 \<longleftrightarrow> x < 0"
- by (simp add: tanh_def field_simps)
-
-lemma tanh_real_zero_iff [simp]: "tanh (x :: real) = 0 \<longleftrightarrow> 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 \<longleftrightarrow> x = 0"
+ by (metis arsinh_0 arsinh_sinh_real sinh_0)
+
+lemma cosh_real_one_iff [simp]: "cosh x = 1 \<longleftrightarrow> x = 0"
+ by (smt (verit, best) Transcendental.arcosh_cosh_real cosh_0 cosh_minus)
+
+lemma tanh_real_nonneg_iff [simp]: "tanh x \<ge> 0 \<longleftrightarrow> x \<ge> 0"
+ by (simp add: tanh_def field_simps)
+
+lemma tanh_real_pos_iff [simp]: "tanh x > 0 \<longleftrightarrow> x > 0"
+ by (simp add: tanh_def field_simps)
+
+lemma tanh_real_nonpos_iff [simp]: "tanh x \<le> 0 \<longleftrightarrow> x \<le> 0"
+ by (simp add: tanh_def field_simps)
+
+lemma tanh_real_neg_iff [simp]: "tanh x < 0 \<longleftrightarrow> x < 0"
+ by (simp add: tanh_def field_simps)
+
+lemma tanh_real_zero_iff [simp]: "tanh x = 0 \<longleftrightarrow> x = 0"
+ by (simp add: tanh_def field_simps)
+
end
-
+
lemma sinh_real_strict_mono: "strict_mono (sinh :: real \<Rightarrow> real)"
by (rule pos_deriv_imp_strict_mono derivative_intros)+ auto