# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1568892975 -3600
# Node ID 65371451fde8afb008925d55f5f3c5260c40c14e
# Parent  4e39d87c9737f0dc9e094f7f4d52a5abc7f80a68
A few more simple results

diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Analysis/Change_Of_Vars.thy
--- 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
diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Analysis/Complex_Transcendental.thy
--- 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"
diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- 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"
diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- 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>
 
diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Analysis/Elementary_Topology.thy
--- 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)
diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Library/Extended_Real.thy
--- 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"
diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Power.thy
--- 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