--- a/src/HOL/Analysis/Change_Of_Vars.thy Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu Sep 19 12:36:15 2019 +0100
@@ -9,41 +9,6 @@
begin
-subsection \<open>Orthogonal Transformation of Balls\<close>
-
-lemma image_orthogonal_transformation_ball:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
- assumes "orthogonal_transformation f"
- shows "f ` ball x r = ball (f x) r"
-proof (intro equalityI subsetI)
- fix y assume "y \<in> f ` ball x r"
- with assms show "y \<in> ball (f x) r"
- by (auto simp: orthogonal_transformation_isometry)
-next
- fix y assume y: "y \<in> ball (f x) r"
- then obtain z where z: "y = f z"
- using assms orthogonal_transformation_surj by blast
- with y assms show "y \<in> f ` ball x r"
- by (auto simp: orthogonal_transformation_isometry)
-qed
-
-lemma image_orthogonal_transformation_cball:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
- assumes "orthogonal_transformation f"
- shows "f ` cball x r = cball (f x) r"
-proof (intro equalityI subsetI)
- fix y assume "y \<in> f ` cball x r"
- with assms show "y \<in> cball (f x) r"
- by (auto simp: orthogonal_transformation_isometry)
-next
- fix y assume y: "y \<in> cball (f x) r"
- then obtain z where z: "y = f z"
- using assms orthogonal_transformation_surj by blast
- with y assms show "y \<in> f ` cball x r"
- by (auto simp: orthogonal_transformation_isometry)
-qed
-
-
subsection \<open>Measurable Shear and Stretch\<close>
proposition
--- a/src/HOL/Analysis/Complex_Transcendental.thy Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Sep 19 12:36:15 2019 +0100
@@ -2568,12 +2568,23 @@
apply (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide)
done
-lemma lim_ln_over_n: "((\<lambda>n. ln(real_of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
+lemma lim_ln_over_n [tendsto_intros]: "((\<lambda>n. ln(real_of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]]
apply (subst filterlim_sequentially_Suc [symmetric])
apply (simp add: lim_sequentially dist_norm)
done
+lemma lim_log_over_n [tendsto_intros]:
+ "(\<lambda>n. log k n/n) \<longlonglongrightarrow> 0"
+proof -
+ have *: "log k n/n = (1/ln k) * (ln n / n)" for n
+ unfolding log_def by auto
+ have "(\<lambda>n. (1/ln k) * (ln n / n)) \<longlonglongrightarrow> (1/ln k) * 0"
+ by (intro tendsto_intros)
+ then show ?thesis
+ unfolding * by auto
+qed
+
lemma lim_1_over_complex_power:
assumes "0 < Re s"
shows "(\<lambda>n. 1 / of_nat n powr s) \<longlonglongrightarrow> 0"
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Thu Sep 19 12:36:15 2019 +0100
@@ -2000,6 +2000,11 @@
lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
by (auto intro!: antisym infdist_nonneg infdist_le2)
+lemma infdist_Un_min:
+ assumes "A \<noteq> {}" "B \<noteq> {}"
+ shows "infdist x (A \<union> B) = min (infdist x A) (infdist x B)"
+using assms by (simp add: infdist_def cINF_union inf_real_def)
+
lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
proof (cases "A = {}")
case True
@@ -2041,6 +2046,9 @@
finally show ?thesis by simp
qed
+lemma infdist_triangle_abs: "\<bar>infdist x A - infdist y A\<bar> \<le> dist x y"
+ by (metis (full_types) abs_diff_le_iff diff_le_eq dist_commute infdist_triangle)
+
lemma in_closure_iff_infdist_zero:
assumes "A \<noteq> {}"
shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
@@ -3236,6 +3244,15 @@
by (auto simp: setdist_def infdist_def)
qed
+lemma infdist_mono:
+ assumes "A \<subseteq> B" "A \<noteq> {}"
+ shows "infdist x B \<le> infdist x A"
+ by (simp add: assms infdist_eq_setdist setdist_subset_right)
+
+lemma infdist_singleton [simp]:
+ "infdist x {y} = dist x y"
+ by (simp add: infdist_eq_setdist)
+
proposition setdist_attains_inf:
assumes "compact B" "B \<noteq> {}"
obtains y where "y \<in> B" "setdist A B = infdist y A"
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Thu Sep 19 12:36:15 2019 +0100
@@ -9,17 +9,13 @@
theory Elementary_Normed_Spaces
imports
"HOL-Library.FuncSet"
- Elementary_Metric_Spaces Linear_Algebra
+ Elementary_Metric_Spaces Cartesian_Space
Connected
begin
+subsection \<open>Orthogonal Transformation of Balls\<close>
subsection\<^marker>\<open>tag unimportant\<close> \<open>Various Lemmas Combining Imports\<close>
-lemma countable_PiE:
- "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)"
- by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
-
-
lemma open_sums:
fixes T :: "('b::real_normed_vector) set"
assumes "open S \<or> open T"
@@ -53,6 +49,38 @@
qed
qed
+lemma image_orthogonal_transformation_ball:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+ assumes "orthogonal_transformation f"
+ shows "f ` ball x r = ball (f x) r"
+proof (intro equalityI subsetI)
+ fix y assume "y \<in> f ` ball x r"
+ with assms show "y \<in> ball (f x) r"
+ by (auto simp: orthogonal_transformation_isometry)
+next
+ fix y assume y: "y \<in> ball (f x) r"
+ then obtain z where z: "y = f z"
+ using assms orthogonal_transformation_surj by blast
+ with y assms show "y \<in> f ` ball x r"
+ by (auto simp: orthogonal_transformation_isometry)
+qed
+
+lemma image_orthogonal_transformation_cball:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+ assumes "orthogonal_transformation f"
+ shows "f ` cball x r = cball (f x) r"
+proof (intro equalityI subsetI)
+ fix y assume "y \<in> f ` cball x r"
+ with assms show "y \<in> cball (f x) r"
+ by (auto simp: orthogonal_transformation_isometry)
+next
+ fix y assume y: "y \<in> cball (f x) r"
+ then obtain z where z: "y = f z"
+ using assms orthogonal_transformation_surj by blast
+ with y assms show "y \<in> f ` cball x r"
+ by (auto simp: orthogonal_transformation_isometry)
+qed
+
subsection \<open>Support\<close>
--- a/src/HOL/Analysis/Elementary_Topology.thy Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Thu Sep 19 12:36:15 2019 +0100
@@ -2479,6 +2479,14 @@
unfolding homeomorphism_def
by (intro conjI ballI continuous_on_compose) (auto simp: image_iff)
+lemma homeomorphism_cong:
+ "homeomorphism X' Y' f' g'"
+ if "homeomorphism X Y f g" "X' = X" "Y' = Y" "\<And>x. x \<in> X \<Longrightarrow> f' x = f x" "\<And>y. y \<in> Y \<Longrightarrow> g' y = g y"
+ using that by (auto simp add: homeomorphism_def)
+
+lemma homeomorphism_empty [simp]:
+ "homeomorphism {} {} f g"
+ unfolding homeomorphism_def by auto
lemma homeomorphism_symD: "homeomorphism S t f g \<Longrightarrow> homeomorphism t S g f"
by (simp add: homeomorphism_def)
--- a/src/HOL/Library/Extended_Real.thy Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Library/Extended_Real.thy Thu Sep 19 12:36:15 2019 +0100
@@ -1725,13 +1725,44 @@
by (cases a b c rule: ereal3_cases)
(auto simp: field_simps zero_less_mult_iff)
-lemma ereal_inverse_real: "\<bar>z\<bar> \<noteq> \<infinity> \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> ereal (inverse (real_of_ereal z)) = inverse z"
- by (cases z) simp_all
+lemma ereal_inverse_real [simp]: "\<bar>z\<bar> \<noteq> \<infinity> \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> ereal (inverse (real_of_ereal z)) = inverse z"
+ by auto
lemma ereal_inverse_mult:
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse (a * (b::ereal)) = inverse a * inverse b"
by (cases a; cases b) auto
+lemma inverse_eq_infinity_iff_eq_zero [simp]:
+ "1/(x::ereal) = \<infinity> \<longleftrightarrow> x = 0"
+by (simp add: divide_ereal_def)
+
+lemma ereal_distrib_left:
+ fixes a b c :: ereal
+ assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>"
+ and "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>"
+ and "\<bar>c\<bar> \<noteq> \<infinity>"
+ shows "c * (a + b) = c * a + c * b"
+using assms
+by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
+
+lemma ereal_distrib_minus_left:
+ fixes a b c :: ereal
+ assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>"
+ and "a \<noteq> -\<infinity> \<or> b \<noteq> -\<infinity>"
+ and "\<bar>c\<bar> \<noteq> \<infinity>"
+ shows "c * (a - b) = c * a - c * b"
+using assms
+by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
+
+lemma ereal_distrib_minus_right:
+ fixes a b c :: ereal
+ assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>"
+ and "a \<noteq> -\<infinity> \<or> b \<noteq> -\<infinity>"
+ and "\<bar>c\<bar> \<noteq> \<infinity>"
+ shows "(a - b) * c = a * c - b * c"
+using assms
+by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
+
subsection "Complete lattice"
@@ -4116,6 +4147,11 @@
by (force simp: continuous_on_def mult_ac)
qed (insert assms, auto simp: mono_def ereal_mult_right_mono)
+lemma Liminf_ereal_mult_left:
+ assumes "F \<noteq> bot" "(c::real) \<ge> 0"
+ shows "Liminf F (\<lambda>n. ereal c * f n) = ereal c * Liminf F f"
+using Liminf_ereal_mult_right[OF assms] by (subst (1 2) mult.commute)
+
lemma Limsup_ereal_mult_left:
assumes "F \<noteq> bot" "(c::real) \<ge> 0"
shows "Limsup F (\<lambda>n. ereal c * f n) = ereal c * Limsup F f"
--- a/src/HOL/Power.thy Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Power.thy Thu Sep 19 12:36:15 2019 +0100
@@ -54,12 +54,6 @@
lemma power_mult: "a ^ (m * n) = (a ^ m) ^ n"
by (induct n) (simp_all add: power_add)
-lemma power2_eq_square: "a\<^sup>2 = a * a"
- by (simp add: numeral_2_eq_2)
-
-lemma power3_eq_cube: "a ^ 3 = a * a * a"
- by (simp add: numeral_3_eq_3 mult.assoc)
-
lemma power_even_eq: "a ^ (2 * n) = (a ^ n)\<^sup>2"
by (subst mult.commute) (simp add: power_mult)
@@ -73,6 +67,15 @@
by (simp only: numeral_Bit1 One_nat_def add_Suc_right add_0_right
power_Suc power_add Let_def mult.assoc)
+lemma power2_eq_square: "a\<^sup>2 = a * a"
+ by (simp add: numeral_2_eq_2)
+
+lemma power3_eq_cube: "a ^ 3 = a * a * a"
+ by (simp add: numeral_3_eq_3 mult.assoc)
+
+lemma power4_eq_xxxx: "x^4 = x * x * x * x"
+ by (simp add: mult.assoc power_numeral_even)
+
lemma funpow_times_power: "(times x ^^ f x) = times (x ^ f x)"
proof (induct "f x" arbitrary: f)
case 0