--- a/src/HOL/Analysis/Path_Connected.thy Fri Jul 16 15:42:52 2021 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Fri Jul 16 20:13:12 2021 +0100
@@ -137,6 +137,24 @@
subsection\<^marker>\<open>tag unimportant\<close>\<open>Basic lemmas about paths\<close>
+lemma path_of_real: "path complex_of_real"
+ unfolding path_def by (intro continuous_intros)
+
+lemma path_const: "path (\<lambda>t. a)" for a::"'a::real_normed_vector"
+ unfolding path_def by (intro continuous_intros)
+
+lemma path_minus: "path g \<Longrightarrow> path (\<lambda>t. - g t)" for g::"real\<Rightarrow>'a::real_normed_vector"
+ unfolding path_def by (intro continuous_intros)
+
+lemma path_add: "\<lbrakk>path f; path g\<rbrakk> \<Longrightarrow> path (\<lambda>t. f t + g t)" for f::"real\<Rightarrow>'a::real_normed_vector"
+ unfolding path_def by (intro continuous_intros)
+
+lemma path_diff: "\<lbrakk>path f; path g\<rbrakk> \<Longrightarrow> path (\<lambda>t. f t - g t)" for f::"real\<Rightarrow>'a::real_normed_vector"
+ unfolding path_def by (intro continuous_intros)
+
+lemma path_mult: "\<lbrakk>path f; path g\<rbrakk> \<Longrightarrow> path (\<lambda>t. f t * g t)" for f::"real\<Rightarrow>'a::real_normed_field"
+ unfolding path_def by (intro continuous_intros)
+
lemma pathin_iff_path_real [simp]: "pathin euclideanreal g \<longleftrightarrow> path g"
by (simp add: pathin_def path_def)
--- a/src/HOL/Analysis/Starlike.thy Fri Jul 16 15:42:52 2021 +0200
+++ b/src/HOL/Analysis/Starlike.thy Fri Jul 16 20:13:12 2021 +0100
@@ -1493,16 +1493,7 @@
and "affine T"
and "rel_interior S \<inter> T \<noteq> {}"
shows "closure (S \<inter> T) = closure S \<inter> T"
-proof -
- have "affine hull T = T"
- using assms by auto
- then have "rel_interior T = T"
- using rel_interior_affine_hull[of T] by metis
- moreover have "closure T = T"
- using assms affine_closed[of T] by auto
- ultimately show ?thesis
- using convex_closure_inter_two[of S T] assms affine_imp_convex by auto
-qed
+ by (metis affine_imp_convex assms convex_closure_inter_two rel_interior_affine rel_interior_eq_closure)
lemma connected_component_1_gen:
fixes S :: "'a :: euclidean_space set"
@@ -1523,16 +1514,7 @@
and "affine T"
and "rel_interior S \<inter> T \<noteq> {}"
shows "rel_interior (S \<inter> T) = rel_interior S \<inter> T"
-proof -
- have "affine hull T = T"
- using assms by auto
- then have "rel_interior T = T"
- using rel_interior_affine_hull[of T] by metis
- moreover have "closure T = T"
- using assms affine_closed[of T] by auto
- ultimately show ?thesis
- using convex_rel_interior_inter_two[of S T] assms affine_imp_convex by auto
-qed
+ by (simp add: affine_imp_convex assms convex_rel_interior_inter_two rel_interior_affine)
lemma convex_affine_rel_frontier_Int:
fixes S T :: "'n::euclidean_space set"
@@ -1547,49 +1529,8 @@
lemma rel_interior_convex_Int_affine:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "affine T" "interior S \<inter> T \<noteq> {}"
- shows "rel_interior(S \<inter> T) = interior S \<inter> T"
-proof -
- obtain a where aS: "a \<in> interior S" and aT:"a \<in> T"
- using assms by force
- have "rel_interior S = interior S"
- by (metis (no_types) aS affine_hull_nonempty_interior equals0D rel_interior_interior)
- then show ?thesis
- by (metis (no_types) affine_imp_convex assms convex_rel_interior_inter_two hull_same rel_interior_affine_hull)
-qed
-
-lemma closure_convex_Int_affine:
- fixes S :: "'a::euclidean_space set"
- assumes "convex S" "affine T" "rel_interior S \<inter> T \<noteq> {}"
- shows "closure(S \<inter> T) = closure S \<inter> T"
-proof
- have "closure (S \<inter> T) \<subseteq> closure T"
- by (simp add: closure_mono)
- also have "... \<subseteq> T"
- by (simp add: affine_closed assms)
- finally show "closure(S \<inter> T) \<subseteq> closure S \<inter> T"
- by (simp add: closure_mono)
-next
- obtain a where "a \<in> rel_interior S" "a \<in> T"
- using assms by auto
- then have ssT: "subspace ((\<lambda>x. (-a)+x) ` T)" and "a \<in> S"
- using affine_diffs_subspace rel_interior_subset assms by blast+
- show "closure S \<inter> T \<subseteq> closure (S \<inter> T)"
- proof
- fix x assume "x \<in> closure S \<inter> T"
- show "x \<in> closure (S \<inter> T)"
- proof (cases "x = a")
- case True
- then show ?thesis
- using \<open>a \<in> S\<close> \<open>a \<in> T\<close> closure_subset by fastforce
- next
- case False
- then have "x \<in> closure(open_segment a x)"
- by auto
- then show ?thesis
- using \<open>x \<in> closure S \<inter> T\<close> assms convex_affine_closure_Int by blast
- qed
- qed
-qed
+ shows "rel_interior(S \<inter> T) = interior S \<inter> T"
+ by (metis Int_emptyI assms convex_affine_rel_interior_Int empty_iff interior_rel_interior_gen)
lemma subset_rel_interior_convex:
fixes S T :: "'n::euclidean_space set"
--- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy Fri Jul 16 15:42:52 2021 +0200
+++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy Fri Jul 16 20:13:12 2021 +0100
@@ -82,6 +82,38 @@
thus ?thesis by simp
qed
+corollary analytic_continuation':
+ assumes "f holomorphic_on S" "open S" "connected S"
+ and "U \<subseteq> S" "\<xi> \<in> S" "\<xi> islimpt U"
+ and "f constant_on U"
+ shows "f constant_on S"
+proof -
+ obtain c where c: "\<And>x. x \<in> U \<Longrightarrow> f x - c = 0"
+ by (metis \<open>f constant_on U\<close> constant_on_def diff_self)
+ have "(\<lambda>z. f z - c) holomorphic_on S"
+ using assms by (intro holomorphic_intros)
+ with c analytic_continuation assms have "\<And>x. x \<in> S \<Longrightarrow> f x - c = 0"
+ by blast
+ then show ?thesis
+ unfolding constant_on_def by force
+qed
+
+lemma holomorphic_compact_finite_zeros:
+ assumes S: "f holomorphic_on S" "open S" "connected S"
+ and "compact K" "K \<subseteq> S"
+ and "\<not> f constant_on S"
+ shows "finite {z\<in>K. f z = 0}"
+proof (rule ccontr)
+ assume "infinite {z\<in>K. f z = 0}"
+ then obtain z where "z \<in> K" and z: "z islimpt {z\<in>K. f z = 0}"
+ using \<open>compact K\<close> by (auto simp: compact_eq_Bolzano_Weierstrass)
+ moreover have "{z\<in>K. f z = 0} \<subseteq> S"
+ using \<open>K \<subseteq> S\<close> by blast
+ ultimately show False
+ using assms analytic_continuation [OF S] unfolding constant_on_def
+ by blast
+qed
+
subsection\<open>Open mapping theorem\<close>
lemma holomorphic_contract_to_zero:
--- a/src/HOL/Conditionally_Complete_Lattices.thy Fri Jul 16 15:42:52 2021 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Fri Jul 16 20:13:12 2021 +0100
@@ -427,6 +427,25 @@
"A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_below A \<Longrightarrow> Inf A \<le> Sup A"
by (auto intro!: cSup_upper2[of "SOME a. a \<in> A"] intro: someI cInf_lower)
+ context
+ fixes f :: "'a \<Rightarrow> 'b::conditionally_complete_lattice"
+ assumes "mono f"
+ begin
+
+ lemma mono_cInf: "\<lbrakk>bdd_below A; A\<noteq>{}\<rbrakk> \<Longrightarrow> f (Inf A) \<le> (INF x\<in>A. f x)"
+ by (simp add: \<open>mono f\<close> conditionally_complete_lattice_class.cINF_greatest cInf_lower monoD)
+
+ lemma mono_cSup: "\<lbrakk>bdd_above A; A\<noteq>{}\<rbrakk> \<Longrightarrow> (SUP x\<in>A. f x) \<le> f (Sup A)"
+ by (simp add: \<open>mono f\<close> conditionally_complete_lattice_class.cSUP_least cSup_upper monoD)
+
+ lemma mono_cINF: "\<lbrakk>bdd_below (A`I); I\<noteq>{}\<rbrakk> \<Longrightarrow> f (INF i\<in>I. A i) \<le> (INF x\<in>I. f (A x))"
+ by (simp add: \<open>mono f\<close> conditionally_complete_lattice_class.cINF_greatest cINF_lower monoD)
+
+ lemma mono_cSUP: "\<lbrakk>bdd_above (A`I); I\<noteq>{}\<rbrakk> \<Longrightarrow> (SUP x\<in>I. f (A x)) \<le> f (SUP i\<in>I. A i)"
+ by (simp add: \<open>mono f\<close> conditionally_complete_lattice_class.cSUP_least cSUP_upper monoD)
+
+ end
+
end
instance complete_lattice \<subseteq> conditionally_complete_lattice
--- a/src/HOL/Deriv.thy Fri Jul 16 15:42:52 2021 +0200
+++ b/src/HOL/Deriv.thy Fri Jul 16 20:13:12 2021 +0100
@@ -959,6 +959,12 @@
shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x * a) has_vector_derivative (x * a)) F"
by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_left])
+lemma has_vector_derivative_divide[derivative_intros]:
+ fixes a :: "'a::real_normed_field"
+ shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x / a) has_vector_derivative (x / a)) F"
+ using has_vector_derivative_mult_left [of f x F "inverse a"]
+ by (simp add: field_class.field_divide_inverse)
+
subsection \<open>Derivatives\<close>
--- a/src/HOL/Groups.thy Fri Jul 16 15:42:52 2021 +0200
+++ b/src/HOL/Groups.thy Fri Jul 16 20:13:12 2021 +0100
@@ -639,6 +639,11 @@
end
+lemma mono_add:
+ fixes a :: "'a::ordered_ab_semigroup_add"
+ shows "mono ((+) a)"
+ by (simp add: add_left_mono monoI)
+
text \<open>Strict monotonicity in both arguments\<close>
class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +
assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
--- a/src/HOL/Real_Vector_Spaces.thy Fri Jul 16 15:42:52 2021 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Fri Jul 16 20:13:12 2021 +0100
@@ -764,6 +764,9 @@
finally show ?thesis by simp
qed
+lemma bdd_below_norm_image: "bdd_below (norm ` A)"
+ by (meson bdd_belowI2 norm_ge_zero)
+
end
class real_normed_algebra = real_algebra + real_normed_vector +
--- a/src/HOL/Rings.thy Fri Jul 16 15:42:52 2021 +0200
+++ b/src/HOL/Rings.thy Fri Jul 16 20:13:12 2021 +0100
@@ -1884,6 +1884,11 @@
end
+lemma mono_mult:
+ fixes a :: "'a::ordered_semiring"
+ shows "a \<ge> 0 \<Longrightarrow> mono ((*) a)"
+ by (simp add: mono_def mult_left_mono)
+
class ordered_semiring_0 = semiring_0 + ordered_semiring
begin