--- 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
--- 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>
--- 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:
--- 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"
--- 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
--- 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}"
--- 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"
--- 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"
--- 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)"