New material about transcendental functions, polynomials, et cetera, thanks to Manuel Eberl

--- a/src/HOL/Computational_Algebra/Polynomial.thy	Mon Feb 19 14:12:29 2024 +0000
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Wed Feb 21 10:46:22 2024 +0000
@@ -464,7 +464,7 @@
   by (simp add: is_zero_def null_def)
 
 
-subsubsection \<open>Reconstructing the polynomial from the list\<close>
+text \<open>Reconstructing the polynomial from the list\<close>
   \<comment> \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>
 
 definition poly_of_list :: "'a::comm_monoid_add list \<Rightarrow> 'a poly"
@@ -1296,6 +1296,15 @@
   "lead_coeff (of_int k) = of_int k"
   by (simp add: of_int_poly)
 
+lemma poly_of_nat [simp]: "poly (of_nat n) x = of_nat n"
+  by (simp add: of_nat_poly)
+
+lemma poly_of_int [simp]: "poly (of_int n) x = of_int n"
+  by (simp add: of_int_poly) 
+
+lemma poly_numeral [simp]: "poly (numeral n) x = numeral n"
+  by (metis of_nat_numeral poly_of_nat)
+
 lemma numeral_poly: "numeral n = [:numeral n:]"
 proof -
   have "numeral n = of_nat (numeral n)"
@@ -1841,6 +1850,12 @@
     by simp
 qed
 
+lemma order_gt_0_iff: "p \<noteq> 0 \<Longrightarrow> order x p > 0 \<longleftrightarrow> poly p x = 0"
+  by (subst order_root) auto
+
+lemma order_eq_0_iff: "p \<noteq> 0 \<Longrightarrow> order x p = 0 \<longleftrightarrow> poly p x \<noteq> 0"
+  by (subst order_root) auto
+
 text \<open>Next three lemmas contributed by Wenda Li\<close>
 lemma order_1_eq_0 [simp]:"order x 1 = 0"
   by (metis order_root poly_1 zero_neq_one)
@@ -2176,6 +2191,68 @@
   qed
 qed
 
+lemma coeff_pcompose_monom_linear [simp]:
+  fixes p :: "'a :: comm_ring_1 poly"
+  shows "coeff (pcompose p (monom c (Suc 0))) k = c ^ k * coeff p k"
+  by (induction p arbitrary: k)
+     (auto simp: coeff_pCons coeff_monom_mult pcompose_pCons split: nat.splits)
+
+lemma of_nat_mult_conv_smult: "of_nat n * P = smult (of_nat n) P"
+  by (simp add: monom_0 of_nat_monom)
+
+lemma numeral_mult_conv_smult: "numeral n * P = smult (numeral n) P"
+  by (simp add: numeral_poly)
+
+lemma sum_order_le_degree:
+  assumes "p \<noteq> 0"
+  shows   "(\<Sum>x | poly p x = 0. order x p) \<le> degree p"
+  using assms
+proof (induction "degree p" arbitrary: p rule: less_induct)
+  case (less p)
+  show ?case
+  proof (cases "\<exists>x. poly p x = 0")
+    case False
+    thus ?thesis
+      by auto
+  next
+    case True
+    then obtain x where x: "poly p x = 0"
+      by auto
+    have "[:-x, 1:] ^ order x p dvd p"
+      by (simp add: order_1)
+    then obtain q where q: "p = [:-x, 1:] ^ order x p * q"
+      by (elim dvdE)
+    have [simp]: "q \<noteq> 0"
+      using q less.prems by auto
+    have "order x p = order x p + order x q"
+      by (subst q, subst order_mult) (auto simp: order_power_n_n)
+    hence "order x q = 0"
+      by auto
+    hence [simp]: "poly q x \<noteq> 0"
+      by (simp add: order_root)
+    have deg_p: "degree p = degree q + order x p"
+      by (subst q, subst degree_mult_eq) (auto simp: degree_power_eq)
+    moreover have "order x p > 0"
+      using x less.prems by (simp add: order_root)
+    ultimately have "degree q < degree p"
+      by linarith
+    hence "(\<Sum>x | poly q x = 0. order x q) \<le> degree q"
+      by (intro less.hyps) auto
+    hence "order x p + (\<Sum>x | poly q x = 0. order x q) \<le> degree p"
+      by (simp add: deg_p)
+    also have "{y. poly q y = 0} = {y. poly p y = 0} - {x}"
+      by (subst q) auto
+    also have "(\<Sum>y \<in> {y. poly p y = 0} - {x}. order y q) =
+               (\<Sum>y \<in> {y. poly p y = 0} - {x}. order y p)"
+      by (intro sum.cong refl, subst q)
+         (auto simp: order_mult order_power_n_n intro!: order_0I)
+    also have "order x p + \<dots> = (\<Sum>y \<in> insert x ({y. poly p y = 0} - {x}). order y p)"
+      using \<open>p \<noteq> 0\<close> by (subst sum.insert) (auto simp: poly_roots_finite)
+    also have "insert x ({y. poly p y = 0} - {x}) = {y. poly p y = 0}"
+      using \<open>poly p x = 0\<close> by auto
+    finally show ?thesis .
+  qed
+qed
 
 subsection \<open>Closure properties of coefficients\<close>
 
@@ -2858,6 +2935,12 @@
     by (simp add: rsquarefree_def order_root)
 qed
 
+lemma has_field_derivative_poly [derivative_intros]:
+  assumes "(f has_field_derivative f') (at x within A)"
+  shows   "((\<lambda>x. poly p (f x)) has_field_derivative
+             (f' * poly (pderiv p) (f x))) (at x within A)"
+  using DERIV_chain[OF poly_DERIV assms, of p] by (simp add: o_def mult_ac)
+
 
 subsection \<open>Algebraic numbers\<close>
 
@@ -5138,7 +5221,6 @@
     by (simp_all add: content_mult mult_ac)
 qed (auto simp: content_mult)
 
-
 no_notation cCons (infixr "##" 65)
 
 end

--- a/src/HOL/Real_Asymp/Multiseries_Expansion_Bounds.thy	Mon Feb 19 14:12:29 2024 +0000
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion_Bounds.thy	Wed Feb 21 10:46:22 2024 +0000
@@ -409,10 +409,6 @@
     and "\<forall>x. l x > 0 \<longrightarrow> f x \<in> {l x..u x} \<longrightarrow> g x \<le> 0 \<longrightarrow> f x powr g x \<in> {u x powr g x..l x powr g x}"
   by (auto intro: powr_mono2 powr_mono2')
 
-(* TODO Move *)
-lemma powr_mono': "a \<le> (b::real) \<Longrightarrow> x \<ge> 0 \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr b \<le> x powr a"
-  using powr_mono[of "-b" "-a" "inverse x"] by (auto simp: powr_def ln_inverse ln_div field_split_simps)
-
 qualified lemma powr_left_bounds:
   fixes f g :: "real \<Rightarrow> real"
   shows "\<forall>x. f x > 0 \<longrightarrow> g x \<in> {l x..u x} \<longrightarrow> f x \<ge> 1 \<longrightarrow> f x powr g x \<in> {f x powr l x..f x powr u x}"

--- a/src/HOL/Transcendental.thy	Mon Feb 19 14:12:29 2024 +0000
+++ b/src/HOL/Transcendental.thy	Wed Feb 21 10:46:22 2024 +0000
@@ -2996,6 +2996,14 @@
     shows "x powr a \<le> y powr b"
   by (meson assms order.trans powr_mono powr_mono2 zero_le_one)
 
+lemma powr_mono': "a \<le> (b::real) \<Longrightarrow> x \<ge> 0 \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr b \<le> x powr a"
+  using powr_mono[of "-b" "-a" "inverse x"] by (auto simp: powr_def ln_inverse ln_div field_split_simps)
+
+lemma powr_less_mono':
+  assumes "(x::real) > 0" "x < 1" "a < b"
+  shows   "x powr b < x powr a"
+  by (metis assms log_powr_cancel order.strict_iff_order powr_mono')
+
 lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
   for x :: real
   unfolding powr_def exp_inj_iff by simp
@@ -5512,6 +5520,35 @@
   unfolding filterlim_at_bot_mirror arctan_minus
   by (intro tendsto_minus tendsto_arctan_at_top)
 
+lemma sin_multiple_reduce:
+  "sin (x * numeral n :: 'a :: {real_normed_field, banach}) = 
+     sin x * cos (x * of_nat (pred_numeral n)) + cos x * sin (x * of_nat (pred_numeral n))"
+proof -
+  have "numeral n = of_nat (pred_numeral n) + (1 :: 'a)"
+    by (metis add.commute numeral_eq_Suc of_nat_Suc of_nat_numeral)
+  also have "sin (x * \<dots>) = sin (x * of_nat (pred_numeral n) + x)"
+    unfolding of_nat_Suc by (simp add: ring_distribs)
+  finally show ?thesis
+    by (simp add: sin_add)
+qed
+
+lemma cos_multiple_reduce:
+  "cos (x * numeral n :: 'a :: {real_normed_field, banach}) =
+     cos (x * of_nat (pred_numeral n)) * cos x - sin (x * of_nat (pred_numeral n)) * sin x"
+proof -
+  have "numeral n = of_nat (pred_numeral n) + (1 :: 'a)"
+    by (metis add.commute numeral_eq_Suc of_nat_Suc of_nat_numeral)
+  also have "cos (x * \<dots>) = cos (x * of_nat (pred_numeral n) + x)"
+    unfolding of_nat_Suc by (simp add: ring_distribs)
+  finally show ?thesis
+    by (simp add: cos_add)
+qed
+
+lemma arccos_eq_pi_iff: "x \<in> {-1..1} \<Longrightarrow> arccos x = pi \<longleftrightarrow> x = -1"
+  by (metis arccos arccos_minus_1 atLeastAtMost_iff cos_pi)
+
+lemma arccos_eq_0_iff: "x \<in> {-1..1} \<Longrightarrow> arccos x = 0 \<longleftrightarrow> x = 1"
+  by (metis arccos arccos_1 atLeastAtMost_iff cos_zero)
 
 subsection \<open>Prove Totality of the Trigonometric Functions\<close>
 
@@ -7211,6 +7248,133 @@
   finally show ?thesis .
 qed
 
+lemma cosh_double_cosh: "cosh (2 * x :: 'a :: {banach, real_normed_field}) = 2 * (cosh x)\<^sup>2 - 1"
+  using cosh_double[of x] by (simp add: sinh_square_eq)
+
+lemma sinh_multiple_reduce:
+  "sinh (x * numeral n :: 'a :: {real_normed_field, banach}) = 
+     sinh x * cosh (x * of_nat (pred_numeral n)) + cosh x * sinh (x * of_nat (pred_numeral n))"
+proof -
+  have "numeral n = of_nat (pred_numeral n) + (1 :: 'a)"
+    by (metis add.commute numeral_eq_Suc of_nat_Suc of_nat_numeral)
+  also have "sinh (x * \<dots>) = sinh (x * of_nat (pred_numeral n) + x)"
+    unfolding of_nat_Suc by (simp add: ring_distribs)
+  finally show ?thesis
+    by (simp add: sinh_add)
+qed
+
+lemma cosh_multiple_reduce:
+  "cosh (x * numeral n :: 'a :: {real_normed_field, banach}) =
+     cosh (x * of_nat (pred_numeral n)) * cosh x + sinh (x * of_nat (pred_numeral n)) * sinh x"
+proof -
+  have "numeral n = of_nat (pred_numeral n) + (1 :: 'a)"
+    by (metis add.commute numeral_eq_Suc of_nat_Suc of_nat_numeral)
+  also have "cosh (x * \<dots>) = cosh (x * of_nat (pred_numeral n) + x)"
+    unfolding of_nat_Suc by (simp add: ring_distribs)
+  finally show ?thesis
+    by (simp add: cosh_add)
+qed
+
+lemma cosh_arcosh_real [simp]:
+  assumes "x \<ge> (1 :: real)"
+  shows   "cosh (arcosh x) = x"
+proof -
+  have "eventually (\<lambda>t::real. cosh t \<ge> x) at_top"
+    using cosh_real_at_top by (simp add: filterlim_at_top)
+  then obtain t where "t \<ge> 1" "cosh t \<ge> x"
+    by (metis eventually_at_top_linorder linorder_not_le order_le_less)
+  moreover have "isCont cosh (y :: real)" for y
+    by (intro continuous_intros)
+  ultimately obtain y where "y \<ge> 0" "x = cosh y"
+    using IVT[of cosh 0 x t] assms by auto
+  thus ?thesis
+    by (simp add: arcosh_cosh_real)
+qed
+
+lemma arcosh_eq_0_iff_real [simp]: "x \<ge> 1 \<Longrightarrow> arcosh x = 0 \<longleftrightarrow> x = (1 :: real)"
+  using cosh_arcosh_real by fastforce
+
+lemma arcosh_nonneg_real [simp]:
+  assumes "x \<ge> 1"
+  shows   "arcosh (x :: real) \<ge> 0"
+proof -
+  have "1 + 0 \<le> x + (x\<^sup>2 - 1) powr (1 / 2)"
+    using assms by (intro add_mono) auto
+  thus ?thesis unfolding arcosh_def by simp
+qed
+
+lemma arcosh_real_strict_mono:
+  fixes x y :: real
+  assumes "1 \<le> x" "x < y"
+  shows   "arcosh x < arcosh y"
+proof -
+  have "cosh (arcosh x) < cosh (arcosh y)"
+    by (subst (1 2) cosh_arcosh_real) (use assms in auto)
+  thus ?thesis
+    using assms by (subst (asm) cosh_real_nonneg_less_iff) auto
+qed
+
+lemma arcosh_less_iff_real [simp]:
+  fixes x y :: real
+  assumes "1 \<le> x" "1 \<le> y"
+  shows   "arcosh x < arcosh y \<longleftrightarrow> x < y"
+  using arcosh_real_strict_mono[of x y] arcosh_real_strict_mono[of y x] assms
+  by (cases x y rule: linorder_cases) auto
+
+lemma arcosh_real_gt_1_iff [simp]: "x \<ge> 1 \<Longrightarrow> arcosh x > 0 \<longleftrightarrow> x \<noteq> (1 :: real)"
+  using arcosh_less_iff_real[of 1 x] by (auto simp del: arcosh_less_iff_real)
+
+lemma sinh_arcosh_real: "x \<ge> 1 \<Longrightarrow> sinh (arcosh x) = sqrt (x\<^sup>2 - 1)"
+  by (rule sym, rule real_sqrt_unique) (auto simp: sinh_square_eq)
+
+
+lemma sinh_arsinh_real [simp]: "sinh (arsinh x :: real) = x"
+proof -
+  have "eventually (\<lambda>t::real. sinh t \<ge> x) at_top"
+    using sinh_real_at_top by (simp add: filterlim_at_top)
+  then obtain t where "sinh t \<ge> x"
+    by (metis eventually_at_top_linorder linorder_not_le order_le_less)
+  moreover have "eventually (\<lambda>t::real. sinh t \<le> x) at_bot"
+    using sinh_real_at_bot by (simp add: filterlim_at_bot)
+  then obtain t' where "t' \<le> t" "sinh t' \<le> x"
+    by (metis eventually_at_bot_linorder nle_le)
+  moreover have "isCont sinh (y :: real)" for y
+    by (intro continuous_intros)
+  ultimately obtain y where "x = sinh y"
+    using IVT[of sinh t' x t] by auto
+  thus ?thesis
+    by (simp add: arsinh_sinh_real)
+qed
+
+lemma arsinh_real_strict_mono:
+  fixes x y :: real
+  assumes "x < y"
+  shows   "arsinh x < arsinh y"
+proof -
+  have "sinh (arsinh x) < sinh (arsinh y)"
+    by (subst (1 2) sinh_arsinh_real) (use assms in auto)
+  thus ?thesis
+    using assms by (subst (asm) sinh_real_less_iff) auto
+qed
+
+lemma arsinh_less_iff_real [simp]:
+  fixes x y :: real
+  shows "arsinh x < arsinh y \<longleftrightarrow> x < y"
+  using arsinh_real_strict_mono[of x y] arsinh_real_strict_mono[of y x]
+  by (cases x y rule: linorder_cases) auto
+
+lemma arsinh_real_eq_0_iff [simp]: "arsinh x = 0 \<longleftrightarrow> x = (0 :: real)"
+  by (metis arsinh_0 sinh_arsinh_real)
+
+lemma arsinh_real_pos_iff [simp]: "arsinh x > 0 \<longleftrightarrow> x > (0 :: real)"
+  using arsinh_less_iff_real[of 0 x] by (simp del: arsinh_less_iff_real)
+
+lemma arsinh_real_neg_iff [simp]: "arsinh x < 0 \<longleftrightarrow> x < (0 :: real)"
+  using arsinh_less_iff_real[of x 0] by (simp del: arsinh_less_iff_real)
+
+lemma cosh_arsinh_real: "cosh (arsinh x) = sqrt (x\<^sup>2 + 1)"
+  by (rule sym, rule real_sqrt_unique) (auto simp: cosh_square_eq)
+
 lemma continuous_on_arsinh [continuous_intros]: "continuous_on A (arsinh :: real \<Rightarrow> real)"
   by (rule DERIV_continuous_on derivative_intros)+