# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1659008000 -3600
# Node ID 32d45952c12d16bdbab4427806c1e1816add4730
# Parent  e174568d52d24ed5933715a8356ae871c4ffee90
a few new theorems

diff -r e174568d52d2 -r 32d45952c12d src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Wed Jul 27 13:17:32 2022 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy	Thu Jul 28 12:33:20 2022 +0100
@@ -145,6 +145,30 @@
     by blast
 qed (auto simp: prod_defs)
 
+lemma raw_has_prod_norm:
+  fixes a :: "'a ::real_normed_field"
+  assumes "raw_has_prod f M a"
+  shows "raw_has_prod (\<lambda>n. norm (f n)) M (norm a)"
+  using assms by (auto simp: raw_has_prod_def prod_norm tendsto_norm)
+
+lemma has_prod_norm:
+  fixes a :: "'a ::real_normed_field"
+  assumes f: "f has_prod a" 
+  shows "(\<lambda>n. norm (f n)) has_prod (norm a)"
+  using f [unfolded has_prod_def]
+proof (elim disjE exE conjE)
+  assume f0: "raw_has_prod f 0 a"
+  then show "(\<lambda>n. norm (f n)) has_prod norm a"
+    using has_prod_def raw_has_prod_norm by blast
+next
+  fix i p
+  assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p"
+  then have "Ex (raw_has_prod (\<lambda>n. norm (f n)) (Suc i))"
+    using raw_has_prod_norm by blast
+  then show ?thesis
+    by (metis \<open>a = 0\<close> \<open>f i = 0\<close> has_prod_0_iff norm_zero)
+qed
+
 
 subsection\<open>Absolutely convergent products\<close>
 
diff -r e174568d52d2 -r 32d45952c12d src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Wed Jul 27 13:17:32 2022 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Jul 28 12:33:20 2022 +0100
@@ -267,6 +267,10 @@
   "infinite S \<Longrightarrow> enumerate S m < enumerate S n \<longleftrightarrow> m < n"
   by (metis enumerate_mono less_asym less_linear)
 
+lemma enumerate_mono_le_iff [simp]:
+  "infinite S \<Longrightarrow> enumerate S m \<le> enumerate S n \<longleftrightarrow> m \<le> n"
+  by (meson enumerate_mono_iff not_le)
+
 lemma le_enumerate:
   assumes S: "infinite S"
   shows "n \<le> enumerate S n"