# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1625420157 -3600
# Node ID 3b76524f5a8525324275d03a57fc9b304b4bcfac
# Parent  5b5e015189a4c871dfda515753ced5f9c83e60c7
Imported lots of material from Stirling_Formula/Gamma_Asymptotics

diff -r 5b5e015189a4 -r 3b76524f5a85 NEWS
--- a/NEWS	Fri Jul 02 20:43:39 2021 +0100
+++ b/NEWS	Sun Jul 04 18:35:57 2021 +0100
@@ -146,6 +146,10 @@
 and some more small lemmas. Some theorems that were stated awkwardly
 before were corrected. Minor INCOMPATIBILITY.
 
+* Session "HOL-Analysis": the complex Arg function has been identified
+with the function "arg" of Complex_Main, renaming arg->Arg also in the
+names of arg_bounded. Minor INCOMPATIBILITY.
+
 * Theorems "antisym" and "eq_iff" in class "order" have been renamed to
 "order.antisym" and "order.eq_iff", to coexist locally with "antisym"
 and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant
diff -r 5b5e015189a4 -r 3b76524f5a85 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Fri Jul 02 20:43:39 2021 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Sun Jul 04 18:35:57 2021 +0100
@@ -3374,6 +3374,26 @@
              (\<lambda>x. \<bar>g' x\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S)"
   using has_absolute_integral_change_of_variables_1 [OF assms] by auto
 
+text \<open>when @{term "n=1"}\<close>
+lemma has_absolute_integral_change_of_variables_1':
+  fixes f :: "real \<Rightarrow> real" and g :: "real \<Rightarrow> real"
+  assumes S: "S \<in> sets lebesgue"
+    and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)"
+    and inj: "inj_on g S"
+  shows "(\<lambda>x. \<bar>g' x\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and>
+           integral S (\<lambda>x. \<bar>g' x\<bar> *\<^sub>R f(g x)) = b
+     \<longleftrightarrow> f absolutely_integrable_on (g ` S) \<and> integral (g ` S) f = b"
+proof -
+  have "(\<lambda>x. \<bar>g' x\<bar> *\<^sub>R vec (f(g x)) :: real ^ 1) absolutely_integrable_on S \<and>
+           integral S (\<lambda>x. \<bar>g' x\<bar> *\<^sub>R vec (f(g x))) = (vec b :: real ^ 1)
+         \<longleftrightarrow> (\<lambda>x. vec (f x) :: real ^ 1) absolutely_integrable_on (g ` S) \<and>
+           integral (g ` S) (\<lambda>x. vec (f x)) = (vec b :: real ^ 1)"
+    using assms unfolding has_field_derivative_iff_has_vector_derivative
+    by (intro has_absolute_integral_change_of_variables_1 assms) auto
+  thus ?thesis
+    by (simp add: absolutely_integrable_on_1_iff integral_on_1_eq)
+qed
+
 
 subsection\<open>Change of variables for integrals: special case of linear function\<close>
 
diff -r 5b5e015189a4 -r 3b76524f5a85 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Fri Jul 02 20:43:39 2021 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sun Jul 04 18:35:57 2021 +0100
@@ -1367,8 +1367,8 @@
   "continuous_on S f \<Longrightarrow> (\<And>z. z \<in> S \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S (\<lambda>x. Ln (f x))"
   by (rule continuous_on_compose2[OF continuous_on_Ln, of "UNIV - nonpos_Reals" S f]) auto
 
-lemma holomorphic_on_Ln [holomorphic_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on S"
-  by (simp add: field_differentiable_within_Ln holomorphic_on_def)
+lemma holomorphic_on_Ln [holomorphic_intros]: "S \<inter> \<real>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Ln holomorphic_on S"
+  by (simp add: disjoint_iff field_differentiable_within_Ln holomorphic_on_def)
 
 lemma holomorphic_on_Ln' [holomorphic_intros]:
   "(\<And>z. z \<in> A \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> f holomorphic_on A \<Longrightarrow> (\<lambda>z. Ln (f z)) holomorphic_on A"
@@ -1695,6 +1695,10 @@
   using mpi_less_Im_Ln Im_Ln_le_pi
   by (force simp: Ln_times)
 
+corollary\<^marker>\<open>tag unimportant\<close> Ln_times_of_nat:
+    "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(of_nat r * z :: complex) = ln (of_nat r) + Ln(z)"
+  using Ln_times_of_real[of "of_nat r" z] by simp
+
 corollary\<^marker>\<open>tag unimportant\<close> Ln_times_Reals:
     "\<lbrakk>r \<in> Reals; Re r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(r * z) = ln (Re r) + Ln(z)"
   using Ln_Reals_eq Ln_times_of_real by fastforce
@@ -1782,7 +1786,7 @@
 
 lemma Arg_eq_Im_Ln:
   assumes "z \<noteq> 0" shows "Arg z = Im (Ln z)"
-proof (rule arg_unique)
+proof (rule cis_Arg_unique)
   show "sgn z = cis (Im (Ln z))"
     by (metis assms exp_Ln exp_eq_polar nonzero_mult_div_cancel_left norm_eq_zero 
               norm_exp_eq_Re of_real_eq_0_iff sgn_eq)
@@ -1797,7 +1801,7 @@
   shows "Arg z = (if z = 0 then 0 else Im (Ln z))"
   by (simp add: Arg_eq_Im_Ln Arg_zero)
 
-lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)"
+lemma Arg_of_real [simp]: "Arg (of_real r) = (if r<0 then pi else 0)"
   by (simp add: Im_Ln_eq_pi Arg_def)
 
 lemma mpi_less_Arg: "-pi < Arg z"
@@ -2047,6 +2051,41 @@
   using unwinding_2pi by (simp add: exp_add)
 
 
+lemma arg_conv_arctan:
+  assumes "Re z > 0"
+  shows   "Arg z = arctan (Im z / Re z)"
+proof (rule cis_Arg_unique)
+  show "sgn z = cis (arctan (Im z / Re z))"
+  proof (rule complex_eqI)
+    have "Re (cis (arctan (Im z / Re z))) = 1 / sqrt (1 + (Im z)\<^sup>2 / (Re z)\<^sup>2)"
+      by (simp add: cos_arctan power_divide)
+    also have "1 + Im z ^ 2 / Re z ^ 2 = norm z ^ 2 / Re z ^ 2"
+      using assms by (simp add: cmod_def field_simps)
+    also have "1 / sqrt \<dots> = Re z / norm z"
+      using assms by (simp add: real_sqrt_divide)
+    finally show "Re (sgn z) = Re (cis (arctan (Im z / Re z)))"
+      by simp
+  next
+    have "Im (cis (arctan (Im z / Re z))) = Im z / (Re z * sqrt (1 + (Im z)\<^sup>2 / (Re z)\<^sup>2))"
+      by (simp add: sin_arctan field_simps)
+    also have "1 + Im z ^ 2 / Re z ^ 2 = norm z ^ 2 / Re z ^ 2"
+      using assms by (simp add: cmod_def field_simps)
+    also have "Im z / (Re z * sqrt \<dots>) = Im z / norm z"
+      using assms by (simp add: real_sqrt_divide)
+    finally show "Im (sgn z) = Im (cis (arctan (Im z / Re z)))"
+      by simp
+  qed
+next
+  show "arctan (Im z / Re z) > -pi"
+    by (rule le_less_trans[OF _ arctan_lbound]) auto
+next
+  have "arctan (Im z / Re z) < pi / 2"
+    by (rule arctan_ubound)
+  also have "\<dots> \<le> pi" by simp
+  finally show "arctan (Im z / Re z) \<le> pi"
+    by simp
+qed
+
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
 
 lemma Arg2pi_Ln:
diff -r 5b5e015189a4 -r 3b76524f5a85 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Fri Jul 02 20:43:39 2021 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Sun Jul 04 18:35:57 2021 +0100
@@ -1792,6 +1792,10 @@
   by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
      (auto simp: differentiable_def has_vector_derivative_def)
 
+lemma deriv_of_real [simp]: 
+  "at x within A \<noteq> bot \<Longrightarrow> vector_derivative of_real (at x within A) = 1"
+  by (auto intro!: vector_derivative_within derivative_eq_intros)
+
 lemma frechet_derivative_eq_vector_derivative:
   assumes "f differentiable (at x)"
     shows  "(frechet_derivative f (at x)) = (\<lambda>r. r *\<^sub>R vector_derivative f (at x))"
@@ -1825,6 +1829,18 @@
   apply (auto simp: Lim_ident_at eventually_at_filter elim: eventually_mono)
   done
 
+lemma vector_derivative_cong_eq:
+  assumes "eventually (\<lambda>x. x \<in> A \<longrightarrow> f x = g x) (nhds x)" "x = y" "A = B" "x \<in> A"
+  shows   "vector_derivative f (at x within A) = vector_derivative g (at y within B)"
+proof -
+  have "f x = g x"
+    using assms eventually_nhds_x_imp_x by blast
+  hence "(\<lambda>D. (f has_vector_derivative D) (at x within A)) = 
+           (\<lambda>D. (g has_vector_derivative D) (at x within A))" using assms
+    by (intro ext has_vector_derivative_cong_ev refl assms) simp_all
+  thus ?thesis by (simp add: vector_derivative_def assms)
+qed
+  
 lemma islimpt_closure_open:
   fixes s :: "'a::perfect_space set"
   assumes "open s" and t: "t = closure s" "x \<in> t"
@@ -2254,6 +2270,20 @@
   shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
   unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff)
 
+lemma DERIV_deriv_iff_field_differentiable:
+  "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
+  unfolding field_differentiable_def by (metis DERIV_imp_deriv)
+
+lemma vector_derivative_of_real_left:
+  assumes "f differentiable at x"
+  shows   "vector_derivative (\<lambda>x. of_real (f x)) (at x) = of_real (deriv f x)"
+  by (metis DERIV_deriv_iff_real_differentiable assms has_vector_derivative_of_real vector_derivative_at)
+  
+lemma vector_derivative_of_real_right:
+  assumes "f field_differentiable at (of_real x)"
+  shows   "vector_derivative (\<lambda>x. f (of_real x)) (at x) = deriv f (of_real x)"
+  by (metis DERIV_deriv_iff_field_differentiable assms has_vector_derivative_real_field vector_derivative_at)
+  
 lemma deriv_cong_ev:
   assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
   shows   "deriv f x = deriv g y"
@@ -2276,7 +2306,7 @@
       by eventually_elim (rule deriv_cong_ev, simp_all)
     thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps)
   qed auto
-  from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp
+  with \<open>x = y\<close> eventually_nhds_x_imp_x show ?thesis by blast 
 qed
 
 lemma real_derivative_chain:
@@ -2298,10 +2328,6 @@
   apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
   using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
 
-lemma DERIV_deriv_iff_field_differentiable:
-  "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
-  unfolding field_differentiable_def by (metis DERIV_imp_deriv)
-
 lemma deriv_chain:
   "f field_differentiable at x \<Longrightarrow> g field_differentiable at (f x)
     \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
diff -r 5b5e015189a4 -r 3b76524f5a85 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Fri Jul 02 20:43:39 2021 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Sun Jul 04 18:35:57 2021 +0100
@@ -1015,6 +1015,21 @@
   by (intro DERIV_imp_deriv has_field_derivative_ln_Gamma_complex assms)
 
 
+lemma higher_deriv_ln_Gamma_complex:
+  assumes "(x::complex) \<notin> \<real>\<^sub>\<le>\<^sub>0"
+  shows   "(deriv ^^ j) ln_Gamma x = (if j = 0 then ln_Gamma x else Polygamma (j - 1) x)"
+proof (cases j)
+  case (Suc j')
+  have "(deriv ^^ j') (deriv ln_Gamma) x = (deriv ^^ j') Digamma x"
+    using eventually_nhds_in_open[of "UNIV - \<real>\<^sub>\<le>\<^sub>0" x] assms
+    by (intro higher_deriv_cong_ev refl)
+       (auto elim!: eventually_mono simp: open_Diff deriv_ln_Gamma_complex)
+  also have "\<dots> = Polygamma j' x" using assms
+    by (subst higher_deriv_Polygamma)
+       (auto elim!: nonpos_Ints_cases simp: complex_nonpos_Reals_iff)
+  finally show ?thesis using Suc by (simp del: funpow.simps add: funpow_Suc_right)
+qed simp_all
+
 
 text \<open>
   We define a type class that captures all the fundamental properties of the inverse of the Gamma function
@@ -1695,6 +1710,27 @@
   shows   "deriv ln_Gamma z = Digamma (z :: real)"
   by (intro DERIV_imp_deriv has_field_derivative_ln_Gamma_real assms)
 
+lemma higher_deriv_ln_Gamma_real:
+  assumes "(x::real) > 0"
+  shows   "(deriv ^^ j) ln_Gamma x = (if j = 0 then ln_Gamma x else Polygamma (j - 1) x)"
+proof (cases j)
+  case (Suc j')
+  have "(deriv ^^ j') (deriv ln_Gamma) x = (deriv ^^ j') Digamma x"
+    using eventually_nhds_in_open[of "{0<..}" x] assms
+    by (intro higher_deriv_cong_ev refl)
+       (auto elim!: eventually_mono simp: open_Diff deriv_ln_Gamma_real)
+  also have "\<dots> = Polygamma j' x" using assms
+    by (subst higher_deriv_Polygamma)
+       (auto elim!: nonpos_Ints_cases simp: complex_nonpos_Reals_iff)
+  finally show ?thesis using Suc by (simp del: funpow.simps add: funpow_Suc_right)
+qed simp_all
+  
+lemma higher_deriv_ln_Gamma_complex_of_real:
+  assumes "(x :: real) > 0"
+  shows   "(deriv ^^ j) ln_Gamma (complex_of_real x) = of_real ((deriv ^^ j) ln_Gamma x)"
+    using assms
+    by (auto simp: higher_deriv_ln_Gamma_real higher_deriv_ln_Gamma_complex
+                   ln_Gamma_complex_of_real Polygamma_of_real)
 
 lemma has_field_derivative_rGamma_real' [derivative_intros]:
   "(rGamma has_field_derivative (if x \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>-x\<rfloor>) * fact (nat \<lfloor>-x\<rfloor>) else
diff -r 5b5e015189a4 -r 3b76524f5a85 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Jul 02 20:43:39 2021 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Jul 04 18:35:57 2021 +0100
@@ -4922,6 +4922,9 @@
     shows "negligible S"
 by (metis negligible_translation [OF assms, of "-c"] translation_galois)
 
+lemma negligible_atLeastAtMostI: "b \<le> a \<Longrightarrow> negligible {a..(b::real)}"
+  using negligible_insert by fastforce
+
 lemma has_integral_spike_set_eq:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes "negligible {x \<in> S - T. f x \<noteq> 0}" "negligible {x \<in> T - S. f x \<noteq> 0}"
diff -r 5b5e015189a4 -r 3b76524f5a85 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Fri Jul 02 20:43:39 2021 +0100
+++ b/src/HOL/Complex.thy	Sun Jul 04 18:35:57 2021 +0100
@@ -962,7 +962,7 @@
 lemma Arg_zero: "Arg 0 = 0"
   by (simp add: Arg_def)
 
-lemma arg_unique:
+lemma cis_Arg_unique:
   assumes "sgn z = cis x" and "-pi < x" and "x \<le> pi"
   shows "Arg z = x"
 proof -
@@ -990,7 +990,7 @@
     by (simp add: Arg_def)
 qed
 
-lemma arg_correct:
+lemma Arg_correct:
   assumes "z \<noteq> 0"
   shows "sgn z = cis (Arg z) \<and> -pi < Arg z \<and> Arg z \<le> pi"
 proof (simp add: Arg_def assms, rule someI_ex)
@@ -1016,10 +1016,10 @@
 qed
 
 lemma Arg_bounded: "- pi < Arg z \<and> Arg z \<le> pi"
-  by (cases "z = 0") (simp_all add: Arg_zero arg_correct)
+  by (cases "z = 0") (simp_all add: Arg_zero Arg_correct)
 
 lemma cis_Arg: "z \<noteq> 0 \<Longrightarrow> cis (Arg z) = sgn z"
-  by (simp add: arg_correct)
+  by (simp add: Arg_correct)
 
 lemma rcis_cmod_Arg: "rcis (cmod z) (Arg z) = z"
   by (cases "z = 0") (simp_all add: rcis_def cis_Arg sgn_div_norm of_real_def)
@@ -1032,10 +1032,10 @@
   using cis_Arg [of y] by (simp add: complex_eq_iff)
 
 lemma Arg_ii [simp]: "Arg \<i> = pi/2"
-  by (rule arg_unique; simp add: sgn_eq)
+  by (rule cis_Arg_unique; simp add: sgn_eq)
 
 lemma Arg_minus_ii [simp]: "Arg (-\<i>) = -pi/2"
-proof (rule arg_unique)
+proof (rule cis_Arg_unique)
   show "sgn (- \<i>) = cis (- pi / 2)"
     by (simp add: sgn_eq)
   show "- pi / 2 \<le> pi"
diff -r 5b5e015189a4 -r 3b76524f5a85 src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Fri Jul 02 20:43:39 2021 +0100
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Sun Jul 04 18:35:57 2021 +0100
@@ -400,6 +400,20 @@
       \<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
 by (metis (no_types, hide_lams) DERIV_deriv_iff_field_differentiable at_within_open comp_apply
          funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
+  
+lemma higher_deriv_cmult:
+  assumes "f holomorphic_on A" "x \<in> A" "open A"
+  shows   "(deriv ^^ j) (\<lambda>x. c * f x) x = c * (deriv ^^ j) f x"
+  using assms
+proof (induction j arbitrary: f x)
+  case (Suc j f x)
+  have "deriv ((deriv ^^ j) (\<lambda>x. c * f x)) x = deriv (\<lambda>x. c * (deriv ^^ j) f x) x"
+    using eventually_nhds_in_open[of A x] assms(2,3) Suc.prems
+    by (intro deriv_cong_ev refl) (auto elim!: eventually_mono simp: Suc.IH)
+  also have "\<dots> = c * deriv ((deriv ^^ j) f) x" using Suc.prems assms(2,3)
+    by (intro deriv_cmult holomorphic_on_imp_differentiable_at holomorphic_higher_deriv) auto
+  finally show ?case by simp
+qed simp_all
 
 lemma valid_path_compose_holomorphic:
   assumes "valid_path g" and holo:"f holomorphic_on S" and "open S" "path_image g \<subseteq> S"
diff -r 5b5e015189a4 -r 3b76524f5a85 src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Fri Jul 02 20:43:39 2021 +0100
+++ b/src/HOL/Library/Indicator_Function.thy	Sun Jul 04 18:35:57 2021 +0100
@@ -77,7 +77,12 @@
 lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)"
   by (auto split: split_indicator)
 
-lemma  (* FIXME unnamed!? *)
+lemma mult_indicator_cong:
+  fixes f g :: "_ \<Rightarrow> 'a :: semiring_1"
+  shows "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> indicator A x * f x = indicator A x * g x"
+  by (auto simp: indicator_def)
+  
+lemma  
   fixes f :: "'a \<Rightarrow> 'b::semiring_1"
   assumes "finite A"
   shows sum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"