Two new theorems

--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Tue Feb 06 18:08:43 2024 +0000
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Feb 07 22:39:42 2024 +0000
@@ -524,7 +524,8 @@
       have "\<And>i. i \<in> subA \<Longrightarrow> e / real (card subA) \<le> 1 \<and> 1 - e / real (card subA) < ff i x"
         using e \<open>B \<subseteq> S\<close> ff subA(1) x by (force simp: field_split_simps)
       then show ?thesis
-        using prod_mono_strict [where f = "\<lambda>x. 1 - e / card subA"] subA(2) by (force simp add: pff_def)
+        using prod_mono_strict[of _ subA "\<lambda>x. 1 - e / card subA" ] subA
+        unfolding pff_def by (smt (verit, best) UN_E assms(3) subsetD)
     qed
     finally have "1 - e < pff x" .
   }

--- a/src/HOL/Binomial.thy	Tue Feb 06 18:08:43 2024 +0000
+++ b/src/HOL/Binomial.thy	Wed Feb 07 22:39:42 2024 +0000
@@ -21,6 +21,15 @@
 definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat"  (infixl "choose" 65)
   where "n choose k = card {K\<in>Pow {0..<n}. card K = k}"
 
+lemma binomial_mono:
+  assumes "m \<le> n" shows "m choose k \<le> n choose k"
+proof -
+  have "{K. K \<subseteq> {0..<m} \<and> card K = k} \<subseteq> {K. K \<subseteq> {0..<n} \<and> card K = k}"
+    using assms by auto
+  then show ?thesis
+    by (simp add: binomial_def card_mono)
+qed
+
 theorem n_subsets:
   assumes "finite A"
   shows "card {B. B \<subseteq> A \<and> card B = k} = card A choose k"

--- a/src/HOL/Groups_Big.thy	Tue Feb 06 18:08:43 2024 +0000
+++ b/src/HOL/Groups_Big.thy	Wed Feb 07 22:39:42 2024 +0000
@@ -1606,16 +1606,23 @@
   "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i \<le> g i) \<Longrightarrow> prod f A \<le> prod g A"
   by (induct A rule: infinite_finite_induct) (force intro!: prod_nonneg mult_mono)+
 
+text \<open>Only one needs to be strict\<close>
 lemma prod_mono_strict:
-  assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
-  shows "prod f A < prod g A"
-  using assms
-proof (induct A rule: finite_induct)
-  case empty
-  then show ?case by simp
-next
-  case insert
-  then show ?case by (force intro: mult_strict_mono' prod_nonneg)
+  assumes "i \<in> A" "f i < g i"
+  assumes "finite A"
+  assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i \<le> g i"
+  assumes "\<And>i. i \<in> A \<Longrightarrow> 0 < g i"
+  shows   "prod f A < prod g A"
+proof -
+  have "prod f A = f i * prod f (A - {i})"
+    using assms by (intro prod.remove)
+  also have "\<dots> \<le> f i * prod g (A - {i})"
+    using assms by (intro mult_left_mono prod_mono) auto
+  also have "\<dots> < g i * prod g (A - {i})"
+    using assms by (intro mult_strict_right_mono prod_pos) auto
+  also have "\<dots> = prod g A"
+    using assms by (intro prod.remove [symmetric])
+  finally show ?thesis .
 qed
 
 lemma prod_le_power:
@@ -1742,4 +1749,24 @@
   finally show ?case .
 qed
 
+lemma (in linordered_semidom) prod_mono_strict':
+  assumes "i \<in> A"
+  assumes "finite A"
+  assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i \<le> g i"
+  assumes "\<And>i. i \<in> A \<Longrightarrow> 0 < g i"
+  assumes "f i < g i"
+  shows   "prod f A < prod g A"
+proof -
+  have "prod f A = f i * prod f (A - {i})"
+    using assms by (intro prod.remove)
+  also have "\<dots> \<le> f i * prod g (A - {i})"
+    using assms by (intro mult_left_mono prod_mono) auto
+  also have "\<dots> < g i * prod g (A - {i})"
+    using assms by (intro mult_strict_right_mono prod_pos) auto
+  also have "\<dots> = prod g A"
+    using assms by (intro prod.remove [symmetric])
+  finally show ?thesis .
+qed
+
+
 end