New library material; also fixed the spelling error powr_ge_pzero -> powr_ge_zero

--- a/src/HOL/Analysis/Bochner_Integration.thy	Tue Aug 06 18:14:45 2024 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Tue Aug 06 22:47:44 2024 +0100
@@ -2512,6 +2512,16 @@
     by (smt (verit) AE_I2 borel_measurable_count_space density_cong ennreal_neg point_measure_def)
 qed
 
+lemma integral_uniform_count_measure:
+  assumes "finite A" 
+  shows "integral\<^sup>L (uniform_count_measure A) f = sum f A / (card A)"
+proof -
+  have "integral\<^sup>L (uniform_count_measure A) f = (\<Sum>x\<in>A. f x / card A)" 
+    using assms by (simp add: uniform_count_measure_def lebesgue_integral_point_measure_finite)
+  with assms show ?thesis
+    by (simp add: sum_divide_distrib nn_integral_count_space_finite)
+qed
+
 subsection \<open>Lebesgue integration on \<^const>\<open>null_measure\<close>\<close>
 
 lemma has_bochner_integral_null_measure_iff[iff]:

--- a/src/HOL/Analysis/Convex.thy	Tue Aug 06 18:14:45 2024 +0100
+++ b/src/HOL/Analysis/Convex.thy	Tue Aug 06 22:47:44 2024 +0100
@@ -297,7 +297,6 @@
     unfolding convex_explicit by auto
 qed (auto simp: convex_explicit assms)
 
-
 subsection \<open>Convex Functions on a Set\<close>
 
 definition\<^marker>\<open>tag important\<close> convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
@@ -1153,6 +1152,58 @@
   finally show ?thesis .
 qed
 
+subsection \<open>Convexity of the generalised binomial\<close>
+
+lemma mono_on_mul:
+  fixes f::"'a::ord \<Rightarrow> 'b::ordered_semiring"
+  assumes "mono_on S f" "mono_on S g"
+  assumes fty: "f \<in> S \<rightarrow> {0..}" and gty: "g \<in> S \<rightarrow> {0..}"
+  shows "mono_on S (\<lambda>x. f x * g x)"
+  using assms by (auto simp: Pi_iff monotone_on_def intro!: mult_mono)
+
+lemma mono_on_prod:
+  fixes f::"'i \<Rightarrow> 'a::ord \<Rightarrow> 'b::linordered_idom"
+  assumes "\<And>i. i \<in> I \<Longrightarrow> mono_on S (f i)" 
+  assumes "\<And>i. i \<in> I \<Longrightarrow> f i \<in> S \<rightarrow> {0..}" 
+  shows "mono_on S (\<lambda>x. prod (\<lambda>i. f i x) I)"
+  using assms
+  by (induction I rule: infinite_finite_induct)
+     (auto simp: mono_on_const Pi_iff prod_nonneg mono_on_mul mono_onI)
+
+lemma convex_gchoose_aux: "convex_on {k-1..} (\<lambda>a. prod (\<lambda>i. a - of_nat i) {0..<k})"
+proof (induction k)
+  case 0
+  then show ?case 
+    by (simp add: convex_on_def)
+next
+  case (Suc k)
+  have "convex_on {real k..} (\<lambda>a. (\<Prod>i = 0..<k. a - real i) * (a - real k))"
+  proof (intro convex_on_mul convex_on_diff)
+    show "convex_on {real k..} (\<lambda>x. \<Prod>i = 0..<k. x - real i)"
+      using Suc convex_on_subset by fastforce
+    show "mono_on {real k..} (\<lambda>x. \<Prod>i = 0..<k. x - real i)"
+      by (force simp: monotone_on_def intro!: prod_mono)
+  next
+    show "(\<lambda>x. \<Prod>i = 0..<k. x - real i) \<in> {real k..} \<rightarrow> {0..}"
+      by (auto intro!: prod_nonneg)
+  qed (auto simp: convex_on_ident concave_on_const mono_onI)
+  then show ?case
+    by simp
+qed
+
+lemma convex_gchoose: "convex_on {k-1..} (\<lambda>x. x gchoose k)"
+  by (simp add: gbinomial_prod_rev convex_on_cdiv convex_gchoose_aux)
+
+lemma gbinomial_mono:
+  fixes k::nat and a::real
+  assumes "of_nat k \<le> a" "a \<le> b" shows "a gchoose k \<le> b gchoose k"
+  using assms
+  by (force simp: gbinomial_prod_rev intro!: divide_right_mono prod_mono)
+
+lemma gbinomial_is_prod: "(a gchoose k) = (\<Prod>i<k. (a - of_nat i) / (1 + of_nat i))"
+  unfolding gbinomial_prod_rev
+  by (induction k; simp add: divide_simps)
+
 subsection \<open>Some inequalities: Applications of convexity\<close>
 
 lemma Youngs_inequality_0:

--- a/src/HOL/Deriv.thy	Tue Aug 06 18:14:45 2024 +0100
+++ b/src/HOL/Deriv.thy	Tue Aug 06 22:47:44 2024 +0100
@@ -1960,10 +1960,10 @@
 qed
 
 
-proposition  deriv_nonneg_imp_mono: (*DELETE*)
-  assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
-  assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
-  assumes ab: "a \<le> b"
+proposition deriv_nonneg_imp_mono: 
+  assumes "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
+  assumes "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
+  assumes "a \<le> b"
   shows "g a \<le> g b"
   by (metis DERIV_nonneg_imp_nondecreasing atLeastAtMost_iff assms)
 

--- a/src/HOL/Library/Landau_Symbols.thy	Tue Aug 06 18:14:45 2024 +0100
+++ b/src/HOL/Library/Landau_Symbols.thy	Tue Aug 06 22:47:44 2024 +0100
@@ -1498,6 +1498,42 @@
   shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)"
   using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_bigo)
 
+lemma smallo_multiples:
+  assumes f: "f \<in> o(real)" and "k>0"
+  shows "(\<lambda>n. f (k * n)) \<in> o(real)"
+proof (clarsimp simp: smallo_def)
+  fix c::real
+  assume "c>0"
+  then have "c/k > 0"
+    by (simp add: assms)
+  with assms have "\<forall>\<^sub>F n in sequentially. \<bar>f n\<bar> \<le> c / real k * n"
+    by (force simp: smallo_def del: divide_const_simps)
+  then obtain N where "\<And>n. n\<ge>N \<Longrightarrow> \<bar>f n\<bar> \<le> c/k * n"
+    by (meson eventually_at_top_linorder)
+  then have "\<And>m. (k*m)\<ge>N \<Longrightarrow> \<bar>f (k*m)\<bar> \<le> c/k * (k*m)"
+    by blast
+  with \<open>k>0\<close> have "\<forall>\<^sub>F m in sequentially. \<bar>f (k*m)\<bar> \<le> c/k * (k*m)"
+    by (smt (verit, del_insts) One_nat_def Suc_leI eventually_at_top_linorderI mult_1_left mult_le_mono)
+  then show "\<forall>\<^sub>F n in sequentially. \<bar>f (k * n)\<bar> \<le> c * n"
+    by eventually_elim (use \<open>k>0\<close> in auto)
+qed
+
+lemma maxmin_in_smallo:
+  assumes "f \<in> o[F](h)" "g \<in> o[F](h)"
+  shows   "(\<lambda>k. max (f k) (g k)) \<in> o[F](h)" "(\<lambda>k. min (f k) (g k)) \<in> o[F](h)"
+proof -
+  { fix c::real
+    assume "c>0"
+    with assms smallo_def
+    have "\<forall>\<^sub>F x in F. norm (f x) \<le> c * norm(h x)" "\<forall>\<^sub>F x in F. norm(g x) \<le> c * norm(h x)"
+      by (auto simp: smallo_def)
+    then have "\<forall>\<^sub>F x in F. norm (max (f x) (g x)) \<le> c * norm(h x) \<and> norm (min (f x) (g x)) \<le> c * norm(h x)"
+      by (smt (verit) eventually_elim2 max_def min_def)
+  } with assms   
+  show "(\<lambda>x. max (f x) (g x)) \<in> o[F](h)" "(\<lambda>x. min (f x) (g x)) \<in> o[F](h)"
+    by (smt (verit) eventually_elim2 landau_o.smallI)+
+qed
+
 lemma le_imp_bigo_real:
   assumes "c \<ge> 0" "eventually (\<lambda>x. f x \<le> c * (g x :: real)) F" "eventually (\<lambda>x. 0 \<le> f x) F"
   shows   "f \<in> O[F](g)"

--- a/src/HOL/Transcendental.thy	Tue Aug 06 18:14:45 2024 +0100
+++ b/src/HOL/Transcendental.thy	Tue Aug 06 22:47:44 2024 +0100
@@ -2401,12 +2401,12 @@
   shows "(prod x I) powr r = (\<Prod>i\<in>I. x i powr r)"
   by (induction I rule: infinite_finite_induct) (auto simp add: powr_mult prod_nonneg)
 
-lemma powr_ge_pzero [simp]: "0 \<le> x powr y"
+lemma powr_ge_zero [simp]: "0 \<le> x powr y"
   for x y :: real
   by (simp add: powr_def)
 
 lemma powr_non_neg[simp]: "\<not> a powr x < 0" for a x::real
-  using powr_ge_pzero[of a x] by arith
+  using powr_ge_zero[of a x] by arith
 
 lemma inverse_powr: "\<And>y::real. inverse y powr a = inverse (y powr a)"
     by (simp add: exp_minus ln_inverse powr_def)
@@ -2978,7 +2978,7 @@
   by (simp add: powr_def root_powr_inverse sqrt_def)
 
 lemma powr_half_sqrt_powr: "0 \<le> x \<Longrightarrow> x powr (a/2) = sqrt(x powr a)"
-  by (metis divide_inverse mult.left_neutral powr_ge_pzero powr_half_sqrt powr_powr)
+  by (metis divide_inverse mult.left_neutral powr_ge_zero powr_half_sqrt powr_powr)
 
 lemma square_powr_half [simp]:
   fixes x::real shows "x\<^sup>2 powr (1/2) = \<bar>x\<bar>"