Some new lemmas. Some tidying up

--- a/src/HOL/Analysis/Convex.thy	Thu Mar 02 11:34:54 2023 +0000
+++ b/src/HOL/Analysis/Convex.thy	Thu Mar 02 17:17:18 2023 +0000
@@ -2369,9 +2369,6 @@
     using hull_inc u by fastforce
 qed
 
-lemma inner_sum_Basis[simp]: "i \<in> Basis \<Longrightarrow> (\<Sum>Basis) \<bullet> i = 1"
-  by (simp add: inner_sum_left sum.If_cases inner_Basis)
-
 lemma convex_set_plus:
   assumes "convex S" and "convex T" shows "convex (S + T)"
 proof -

--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Thu Mar 02 11:34:54 2023 +0000
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Thu Mar 02 17:17:18 2023 +0000
@@ -895,6 +895,17 @@
     by (rule bounded_subset)
 qed
 
+lemma continuous_on_compact_bound:
+  assumes "compact A" "continuous_on A f"
+  obtains B where "B \<ge> 0" "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> B"
+proof -
+  have "compact (f ` A)" by (metis assms compact_continuous_image)
+  then obtain B where "\<forall>x\<in>A. norm (f x) \<le> B"
+    by (auto dest!: compact_imp_bounded simp: bounded_iff)
+  hence "max B 0 \<ge> 0" and "\<forall>x\<in>A. norm (f x) \<le> max B 0" by auto
+  thus ?thesis using that by blast
+qed
+
 lemma closure_Int_ball_not_empty:
   assumes "S \<subseteq> closure T" "x \<in> S" "r > 0"
   shows "T \<inter> ball x r \<noteq> {}"

--- a/src/HOL/Analysis/Euclidean_Space.thy	Thu Mar 02 11:34:54 2023 +0000
+++ b/src/HOL/Analysis/Euclidean_Space.thy	Thu Mar 02 17:17:18 2023 +0000
@@ -53,6 +53,9 @@
 lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u"
   unfolding sgn_div_norm by (simp add: scaleR_one)
 
+lemma inner_sum_Basis[simp]: "i \<in> Basis \<Longrightarrow> inner (\<Sum>Basis) i = 1"
+  by (simp add: inner_sum_left sum.If_cases inner_Basis)
+
 lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis"
 proof
   assume "0 \<in> Basis" thus "False"

--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Mar 02 11:34:54 2023 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Mar 02 17:17:18 2023 +0000
@@ -840,6 +840,76 @@
     by (metis assms continuous_on_compose continuous_on_swap swap_cbox_Pair)
 qed
 
+lemma open_contains_cbox:
+  fixes x :: "'a :: euclidean_space"
+  assumes "open A" "x \<in> A"
+  obtains a b where "cbox a b \<subseteq> A" "x \<in> box a b" "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
+proof -
+  from assms obtain R where R: "R > 0" "ball x R \<subseteq> A"
+    by (auto simp: open_contains_ball)
+  define r :: real where "r = R / (2 * sqrt DIM('a))"
+  from \<open>R > 0\<close> have [simp]: "r > 0" by (auto simp: r_def)
+  define d :: 'a where "d = r *\<^sub>R Topology_Euclidean_Space.One"
+  have "cbox (x - d) (x + d) \<subseteq> A"
+  proof safe
+    fix y assume y: "y \<in> cbox (x - d) (x + d)"
+    have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
+      by (subst euclidean_dist_l2) (auto simp: L2_set_def)
+    also from y have "sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2) \<le> sqrt (\<Sum>i\<in>(Basis::'a set). r\<^sup>2)"
+      by (intro real_sqrt_le_mono sum_mono power_mono)
+         (auto simp: dist_norm d_def cbox_def algebra_simps)
+    also have "\<dots> = sqrt (DIM('a) * r\<^sup>2)" by simp
+    also have "DIM('a) * r\<^sup>2 = (R / 2) ^ 2"
+      by (simp add: r_def power_divide)
+    also have "sqrt \<dots> = R / 2"
+      using \<open>R > 0\<close> by simp
+    also from \<open>R > 0\<close> have "\<dots> < R" by simp
+    finally have "y \<in> ball x R" by simp
+    with R show "y \<in> A" by blast
+  qed
+  thus ?thesis
+    using that[of "x - d" "x + d"] by (auto simp: algebra_simps d_def box_def)
+qed
+
+lemma open_contains_box:
+  fixes x :: "'a :: euclidean_space"
+  assumes "open A" "x \<in> A"
+  obtains a b where "box a b \<subseteq> A" "x \<in> box a b" "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
+  by (meson assms box_subset_cbox dual_order.trans open_contains_cbox)
+
+lemma inner_image_box:
+  assumes "(i :: 'a :: euclidean_space) \<in> Basis"
+  assumes "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
+  shows   "(\<lambda>x. x \<bullet> i) ` box a b = {a \<bullet> i<..<b \<bullet> i}"
+proof safe
+  fix x assume x: "x \<in> {a \<bullet> i<..<b \<bullet> i}"
+  let ?y = "(\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) *\<^sub>R j)"
+  from x assms have "?y \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` box a b"
+    by (intro imageI) (auto simp: box_def algebra_simps)
+  also have "?y \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) * (j \<bullet> i))"
+    by (simp add: inner_sum_left)
+  also have "\<dots> = (\<Sum>j\<in>Basis. if i = j then x else 0)"
+    by (intro sum.cong) (auto simp: inner_not_same_Basis assms)
+  also have "\<dots> = x" using assms by simp
+  finally show "x \<in> (\<lambda>x. x \<bullet> i) ` box a b"  .
+qed (insert assms, auto simp: box_def)
+
+lemma inner_image_cbox:
+  assumes "(i :: 'a :: euclidean_space) \<in> Basis"
+  assumes "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
+  shows   "(\<lambda>x. x \<bullet> i) ` cbox a b = {a \<bullet> i..b \<bullet> i}"
+proof safe
+  fix x assume x: "x \<in> {a \<bullet> i..b \<bullet> i}"
+  let ?y = "(\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) *\<^sub>R j)"
+  from x assms have "?y \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` cbox a b"
+    by (intro imageI) (auto simp: cbox_def)
+  also have "?y \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) * (j \<bullet> i))"
+    by (simp add: inner_sum_left)
+  also have "\<dots> = (\<Sum>j\<in>Basis. if i = j then x else 0)"
+    by (intro sum.cong) (auto simp: inner_not_same_Basis assms)
+  also have "\<dots> = x" using assms by simp
+  finally show "x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b"  .
+qed (insert assms, auto simp: cbox_def)
 
 subsection \<open>General Intervals\<close>
 

--- a/src/HOL/Archimedean_Field.thy	Thu Mar 02 11:34:54 2023 +0000
+++ b/src/HOL/Archimedean_Field.thy	Thu Mar 02 17:17:18 2023 +0000
@@ -417,33 +417,7 @@
 
 lemma floor_divide_of_nat_eq: "\<lfloor>of_nat m / of_nat n\<rfloor> = of_nat (m div n)"
   for m n :: nat
-proof (cases "n = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  then have *: "\<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> = 0"
-    by (auto intro: floor_unique)
-  have "(of_nat m :: 'a) = of_nat (m div n * n + m mod n)"
-    by simp
-  also have "\<dots> = (of_nat (m div n) + of_nat (m mod n) / of_nat n) * of_nat n"
-    using False by (simp only: of_nat_add) (simp add: field_simps)
-  finally have "(of_nat m / of_nat n :: 'a) = \<dots> / of_nat n"
-    by simp
-  then have "(of_nat m / of_nat n :: 'a) = of_nat (m div n) + of_nat (m mod n) / of_nat n"
-    using False by (simp only:) simp
-  then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\<rfloor>"
-    by simp
-  then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m mod n) / of_nat n + of_nat (m div n) :: 'a\<rfloor>"
-    by (simp add: ac_simps)
-  moreover have "(of_nat (m div n) :: 'a) = of_int (of_nat (m div n))"
-    by simp
-  ultimately have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> =
-      \<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> + of_nat (m div n)"
-    by (simp only: floor_add_int)
-  with * show ?thesis
-    by simp
-qed
+    by (metis floor_divide_of_int_eq of_int_of_nat_eq unique_euclidean_semiring_with_nat_class.of_nat_div)
 
 lemma floor_divide_lower:
   fixes q :: "'a::floor_ceiling"

--- a/src/HOL/Library/Landau_Symbols.thy	Thu Mar 02 11:34:54 2023 +0000
+++ b/src/HOL/Library/Landau_Symbols.thy	Thu Mar 02 17:17:18 2023 +0000
@@ -2052,6 +2052,17 @@
   shows   "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"
   using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)
 
+lemma asymp_equivD_strong:
+  assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<noteq> 0 \<or> g x \<noteq> 0) F"
+  shows   "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"
+proof -
+  from assms(1) have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
+    by (rule asymp_equivD)
+  also have "?this \<longleftrightarrow> ?thesis"
+    by (intro filterlim_cong eventually_mono[OF assms(2)]) auto
+  finally show ?thesis .
+qed
+
 lemma asymp_equiv_compose [asymp_equiv_intros]:
   assumes "f \<sim>[G] g" "filterlim h G F"
   shows   "f \<circ> h \<sim>[F] g \<circ> h"

--- a/src/HOL/Real.thy	Thu Mar 02 11:34:54 2023 +0000
+++ b/src/HOL/Real.thy	Thu Mar 02 17:17:18 2023 +0000
@@ -1067,11 +1067,7 @@
   by (metis floor_divide_of_nat_eq of_int_floor_le of_int_of_nat_eq)
 
 lemma real_of_nat_div3: "real n / real x - real (n div x) \<le> 1" for n x :: nat
-proof (cases "x = 0")
-  case False
-  then show ?thesis
-    by (metis of_int_of_nat_eq real_of_int_div3 zdiv_int)
-qed auto
+  by (metis of_int_of_nat_eq real_of_int_div3 of_nat_div)
 
 lemma real_of_nat_div4: "real (n div x) \<le> real n / real x" for n x :: nat
   using real_of_nat_div2 [of n x] by simp

--- a/src/HOL/Transcendental.thy	Thu Mar 02 11:34:54 2023 +0000
+++ b/src/HOL/Transcendental.thy	Thu Mar 02 17:17:18 2023 +0000
@@ -2492,6 +2492,9 @@
       for a x :: "'a::{ln,real_normed_field}"
   by (simp add: divide_inverse powr_minus)
 
+lemma powr_sum: "x \<noteq> 0 \<Longrightarrow> finite A \<Longrightarrow> x powr sum f A = (\<Prod>y\<in>A. x powr f y)"
+  by (simp add: powr_def exp_sum sum_distrib_right)
+
 lemma divide_powr_uminus: "a / b powr c = a * b powr (- c)"
   for a b c :: real
   by (simp add: powr_minus_divide)