--- a/src/HOL/Analysis/Path_Connected.thy Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Mon Sep 25 17:06:05 2023 +0100
@@ -447,6 +447,18 @@
"simple_path c \<Longrightarrow> path_image c - {pathstart c,pathfinish c} \<noteq> {}"
by (simp add: simple_path_endless)
+lemma simple_path_continuous_image:
+ assumes "simple_path f" "continuous_on (path_image f) g" "inj_on g (path_image f)"
+ shows "simple_path (g \<circ> f)"
+ unfolding simple_path_def
+proof
+ show "path (g \<circ> f)"
+ using assms unfolding simple_path_def by (intro path_continuous_image) auto
+ from assms have [simp]: "g (f x) = g (f y) \<longleftrightarrow> f x = f y" if "x \<in> {0..1}" "y \<in> {0..1}" for x y
+ unfolding inj_on_def path_image_def using that by fastforce
+ show "loop_free (g \<circ> f)"
+ using assms(1) by (auto simp: loop_free_def simple_path_def)
+qed
subsection\<^marker>\<open>tag unimportant\<close>\<open>The operations on paths\<close>
--- a/src/HOL/Analysis/Uniform_Limit.thy Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Analysis/Uniform_Limit.thy Mon Sep 25 17:06:05 2023 +0100
@@ -56,12 +56,28 @@
unfolding uniform_limit_iff eventually_at
by (fastforce dest: spec[where x = "e / 2" for e])
+lemma uniform_limit_compose:
+ assumes ul: "uniform_limit X g l F"
+ and cont: "uniformly_continuous_on U f"
+ and g: "\<forall>\<^sub>F n in F. g n ` X \<subseteq> U" and l: "l ` X \<subseteq> U"
+ shows "uniform_limit X (\<lambda>a b. f (g a b)) (f \<circ> l) F"
+proof (rule uniform_limitI)
+ fix \<epsilon>::real
+ assume "0 < \<epsilon>"
+ then obtain \<delta> where "\<delta> > 0" and \<delta>: "\<And>u v. \<lbrakk>u\<in>U; v\<in>U; dist u v < \<delta>\<rbrakk> \<Longrightarrow> dist (f u) (f v) < \<epsilon>"
+ by (metis cont uniformly_continuous_on_def)
+ show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (f (g n x)) ((f \<circ> l) x) < \<epsilon>"
+ using uniform_limitD [OF ul \<open>\<delta>>0\<close>] g unfolding o_def
+ by eventually_elim (use \<delta> l in blast)
+qed
+
lemma metric_uniform_limit_imp_uniform_limit:
assumes f: "uniform_limit S f a F"
assumes le: "eventually (\<lambda>x. \<forall>y\<in>S. dist (g x y) (b y) \<le> dist (f x y) (a y)) F"
shows "uniform_limit S g b F"
proof (rule uniform_limitI)
- fix e :: real assume "0 < e"
+ fix e :: real
+ assume "0 < e"
from uniform_limitD[OF f this] le
show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (g x y) (b y) < e"
by eventually_elim force
--- a/src/HOL/Complex.thy Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Complex.thy Mon Sep 25 17:06:05 2023 +0100
@@ -769,6 +769,14 @@
lemma Im_sum[simp]: "Im (sum f s) = (\<Sum>x\<in>s. Im(f x))"
by (induct s rule: infinite_finite_induct) auto
+lemma Rats_complex_of_real_iff [iff]: "complex_of_real x \<in> \<rat> \<longleftrightarrow> x \<in> \<rat>"
+proof -
+ have "\<And>a b. \<lbrakk>0 < b; x = complex_of_int a / complex_of_int b\<rbrakk> \<Longrightarrow> x \<in> \<rat>"
+ by (metis Rats_divide Rats_of_int Re_complex_of_real Re_divide_of_real of_real_of_int_eq)
+ then show ?thesis
+ by (auto simp: elim!: Rats_cases')
+qed
+
lemma sum_Re_le_cmod: "(\<Sum>i\<in>I. Re (z i)) \<le> cmod (\<Sum>i\<in>I. z i)"
by (metis Re_sum complex_Re_le_cmod)
--- a/src/HOL/Complex_Analysis/Meromorphic.thy Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Complex_Analysis/Meromorphic.thy Mon Sep 25 17:06:05 2023 +0100
@@ -2,23 +2,6 @@
imports Laurent_Convergence Riemann_Mapping
begin
-lemma analytic_at_cong:
- assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
- shows "f analytic_on {x} \<longleftrightarrow> g analytic_on {y}"
-proof -
- have "g analytic_on {x}" if "f analytic_on {x}" "eventually (\<lambda>x. f x = g x) (nhds x)" for f g
- proof -
- have "(\<lambda>y. f (x + y)) has_fps_expansion fps_expansion f x"
- by (rule analytic_at_imp_has_fps_expansion) fact
- also have "?this \<longleftrightarrow> (\<lambda>y. g (x + y)) has_fps_expansion fps_expansion f x"
- using that by (intro has_fps_expansion_cong refl) (auto simp: nhds_to_0' eventually_filtermap)
- finally show ?thesis
- by (rule has_fps_expansion_imp_analytic)
- qed
- from this[of f g] this[of g f] show ?thesis using assms
- by (auto simp: eq_commute)
-qed
-
definition remove_sings :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
"remove_sings f z = (if \<exists>c. f \<midarrow>z\<rightarrow> c then Lim (at z) f else 0)"
@@ -2330,4 +2313,4 @@
finally show ?thesis .
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Conditionally_Complete_Lattices.thy Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Mon Sep 25 17:06:05 2023 +0100
@@ -590,6 +590,68 @@
lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded)
+lemma Sup_inverse_eq_inverse_Inf:
+ fixes f::"'b \<Rightarrow> 'a::{conditionally_complete_linorder,linordered_field}"
+ assumes "bdd_above (range f)" "L > 0" and geL: "\<And>x. f x \<ge> L"
+ shows "(SUP x. 1 / f x) = 1 / (INF x. f x)"
+proof (rule antisym)
+ have bdd_f: "bdd_below (range f)"
+ by (meson assms bdd_belowI2)
+ have "Inf (range f) \<ge> L"
+ by (simp add: cINF_greatest geL)
+ have bdd_invf: "bdd_above (range (\<lambda>x. 1 / f x))"
+ proof (rule bdd_aboveI2)
+ show "\<And>x. 1 / f x \<le> 1/L"
+ using assms by (auto simp: divide_simps)
+ qed
+ moreover have le_inverse_Inf: "1 / f x \<le> 1 / Inf (range f)" for x
+ proof -
+ have "Inf (range f) \<le> f x"
+ by (simp add: bdd_f cInf_lower)
+ then show ?thesis
+ using assms \<open>L \<le> Inf (range f)\<close> by (auto simp: divide_simps)
+ qed
+ ultimately show *: "(SUP x. 1 / f x) \<le> 1 / Inf (range f)"
+ by (auto simp: cSup_le_iff cINF_lower)
+ have "1 / (SUP x. 1 / f x) \<le> f y" for y
+ proof (cases "(SUP x. 1 / f x) < 0")
+ case True
+ with assms show ?thesis
+ by (meson less_asym' order_trans linorder_not_le zero_le_divide_1_iff)
+ next
+ case False
+ have "1 / f y \<le> (SUP x. 1 / f x)"
+ by (simp add: bdd_invf cSup_upper)
+ with False assms show ?thesis
+ by (metis (no_types) div_by_1 divide_divide_eq_right dual_order.strict_trans1 inverse_eq_divide
+ inverse_le_imp_le mult.left_neutral)
+ qed
+ then have "1 / (SUP x. 1 / f x) \<le> Inf (range f)"
+ using bdd_f by (simp add: le_cInf_iff)
+ moreover have "(SUP x. 1 / f x) > 0"
+ using assms cSUP_upper [OF _ bdd_invf] by (meson UNIV_I less_le_trans zero_less_divide_1_iff)
+ ultimately show "1 / Inf (range f) \<le> (SUP t. 1 / f t)"
+ using \<open>L \<le> Inf (range f)\<close> \<open>L>0\<close> by (auto simp: field_simps)
+qed
+
+lemma Inf_inverse_eq_inverse_Sup:
+ fixes f::"'b \<Rightarrow> 'a::{conditionally_complete_linorder,linordered_field}"
+ assumes "bdd_above (range f)" "L > 0" and geL: "\<And>x. f x \<ge> L"
+ shows "(INF x. 1 / f x) = 1 / (SUP x. f x)"
+proof -
+ obtain M where "M>0" and M: "\<And>x. f x \<le> M"
+ by (meson assms cSup_upper dual_order.strict_trans1 rangeI)
+ have bdd: "bdd_above (range (inverse \<circ> f))"
+ using assms le_imp_inverse_le by (auto simp: bdd_above_def)
+ have "f x > 0" for x
+ using \<open>L>0\<close> geL order_less_le_trans by blast
+ then have [simp]: "1 / inverse(f x) = f x" "1 / M \<le> 1 / f x" for x
+ using M \<open>M>0\<close> by (auto simp: divide_simps)
+ show ?thesis
+ using Sup_inverse_eq_inverse_Inf [OF bdd, of "inverse M"] \<open>M>0\<close>
+ by (simp add: inverse_eq_divide)
+qed
+
lemma Inf_insert_finite:
fixes S :: "'a::conditionally_complete_linorder set"
shows "finite S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
--- a/src/HOL/Int.thy Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Int.thy Mon Sep 25 17:06:05 2023 +0100
@@ -1738,6 +1738,12 @@
lemma power_int_numeral [simp]: "power_int x (numeral n) = x ^ numeral n"
by (simp add: power_int_def)
+lemma powi_numeral_reduce: "x powi numeral n = x * x powi int (pred_numeral n)"
+ by (simp add: numeral_eq_Suc)
+
+lemma powi_minus_numeral_reduce: "x powi - (numeral n) = inverse x * x powi - int(pred_numeral n)"
+ by (simp add: numeral_eq_Suc power_int_def)
+
lemma int_cases4 [case_names nonneg neg]:
fixes m :: int
obtains n where "m = int n" | n where "n > 0" "m = -int n"