Theory Complex_Analytic
section ‹Complex Analyticity and the Complexification of Real-Analytic Functions›
text ‹
Connections with complex analysis: a Cauchy--Riemann criterion for holomorphy;
holomorphic functions are ‹C⇧∞›; and a real function is real-analytic at a point iff
it extends holomorphically to a complex ball around that point.
›
theory Complex_Analytic
imports "HOL-Analysis.Real_Analytic" Cauchy_Integral_Formula
begin
subsection ‹A CR-linear self-map of the plane is multiplication by a scalar›
definition CR_linear :: "(complex ⇒ complex) ⇒ bool" where
"CR_linear L ⟷ bounded_linear L ∧ (∀v. L (𝗂 * v) = 𝗂 * L v)"
lemma CR_linear_is_mult:
assumes "CR_linear L"
shows "∃a. ∀v. L v = a * v"
proof -
from assms have bl: "bounded_linear L" and cr: "⋀v. L (𝗂 * v) = 𝗂 * L v"
by (auto simp: CR_linear_def)
interpret bounded_linear L by (rule bl)
have Lof: "L (complex_of_real r) = complex_of_real r * L 1" for r
proof -
have "L (complex_of_real r) = L (r *⇩R 1)"
by (simp add: scaleR_conv_of_real)
also have "… = r *⇩R L 1"
by (rule scaleR)
also have "… = complex_of_real r * L 1"
by (simp add: scaleR_conv_of_real)
finally show ?thesis .
qed
have "L v = L 1 * v" for v
proof -
have decomp: "v = complex_of_real (Re v) + 𝗂 * complex_of_real (Im v)"
by (simp add: complex_eq_iff)
have "L v = L (complex_of_real (Re v) + 𝗂 * complex_of_real (Im v))"
using decomp by simp
also have "… = L (complex_of_real (Re v)) + L (𝗂 * complex_of_real (Im v))"
by (rule add)
also have "… = L (complex_of_real (Re v)) + 𝗂 * L (complex_of_real (Im v))"
using cr by simp
also have "… = complex_of_real (Re v) * L 1 + 𝗂 * (complex_of_real (Im v) * L 1)"
by (simp add: Lof)
also have "… = L 1 * (complex_of_real (Re v) + 𝗂 * complex_of_real (Im v))"
by (simp add: algebra_simps)
also have "… = L 1 * v"
using decomp by simp
finally show ?thesis .
qed
thus ?thesis by blast
qed
subsection ‹Several-variable Cauchy--Riemann criterion›
theorem CauchyRiemann_imp_holomorphic:
fixes f :: "complex ⇒ complex"
assumes Sopen: "open S"
and diff: "⋀x. x ∈ S ⟹ (f has_derivative (L x)) (at x)"
and CR: "⋀x. x ∈ S ⟹ CR_linear (L x)"
shows "f holomorphic_on S"
proof -
have "f field_differentiable (at x)" if xS: "x ∈ S" for x
proof -
from CR[OF xS] obtain a where a: "⋀v. L x v = a * v"
using CR_linear_is_mult by blast
from diff[OF xS] have "(f has_derivative (L x)) (at x)" .
moreover have "L x = (*) a"
using a by auto
ultimately have "(f has_derivative (*) a) (at x)" by simp
hence "(f has_field_derivative a) (at x)"
by (simp add: has_field_derivative_def mult.commute)
thus ?thesis
using field_differentiable_def by blast
qed
thus ?thesis
using Sopen by (simp add: holomorphic_on_open field_differentiable_def)
qed
text ‹A constant multiple of a holomorphic function is ‹C⇧k› at each point, for every ‹k›.›
lemma holomorphic_const_mult_Ck_at:
fixes f :: "complex ⇒ complex"
assumes "f holomorphic_on U" and "open U" and "x ∈ U"
shows "Ck_at k (λy. c * f y) x"
using assms
proof (induction k arbitrary: f x c)
case 0
have "continuous (at x) (λy. c * f y)"
proof -
have "continuous_on U f"
using 0 holomorphic_on_imp_continuous_on by blast
hence "continuous (at x) f"
using 0 by (simp add: continuous_on_eq_continuous_at)
thus ?thesis by (intro continuous_intros)
qed
thus ?case by simp
next
case (Suc k)
note holf = Suc.prems(1) and openU = Suc.prems(2) and xU = Suc.prems(3)
have holcf: "(λy. c * f y) holomorphic_on U"
using holf by (intro holomorphic_intros)
have nbhd: "∃A. open A ∧ x ∈ A ∧ (∀y∈A. Ck_at k (λy. c * f y) y)"
proof (intro exI[of _ U] conjI ballI)
fix y assume "y ∈ U"
show "Ck_at k (λz. c * f z) y"
using Suc.IH[OF holf openU ‹y ∈ U›] .
qed (use openU xU in auto)
have diff: "(λy. c * f y) differentiable (at x)"
using holomorphic_imp_differentiable_real[OF holcf openU xU] .
have derivs: "∀v. Ck_at k (λy. frechet_derivative (λz. c * f z) (at y) v) x"
proof
fix v
have eqd: "⋀y. y ∈ U ⟹
frechet_derivative (λz. c * f z) (at y) v = (c * v) * deriv f y"
proof -
fix y assume yU: "y ∈ U"
have "frechet_derivative (λz. c * f z) (at y) v = deriv (λz. c * f z) y * v"
using frechet_derivative_holomorphic[OF holcf openU yU] by simp
also have "deriv (λz. c * f z) y = c * deriv f y"
using holf openU yU
by (simp add: deriv_cmult holomorphic_on_imp_differentiable_at)
finally show "frechet_derivative (λz. c * f z) (at y) v = (c * v) * deriv f y"
by (simp add: algebra_simps)
qed
have holderiv: "deriv f holomorphic_on U"
using holf openU by (rule holomorphic_deriv)
have base: "Ck_at k (λy. (c * v) * deriv f y) x"
using Suc.IH[OF holderiv openU xU] .
show "Ck_at k (λy. frechet_derivative (λz. c * f z) (at y) v) x"
by (rule Ck_at_transfer_open[OF openU xU _ base]) (simp add: eqd)
qed
show ?case
unfolding Ck_at.simps(2)
using nbhd diff derivs by blast
qed
theorem holomorphic_imp_Cinfinity_on:
assumes "f holomorphic_on U" and "open U"
shows "Cinfinity_on f U"
unfolding Cinfinity_on_def Cinfinity_at_def
proof (intro conjI ballI allI)
show "open U" by (rule assms(2))
next
fix x :: complex and k assume xU: "x ∈ U"
have "Ck_at k (λy. 1 * f y) x"
using holomorphic_const_mult_Ck_at[OF assms(1) assms(2) xU] .
thus "Ck_at k f x" by simp
qed
subsection ‹Real analyticity via holomorphic extension›
definition has_holo_extension_at :: "(real ⇒ real) ⇒ real ⇒ bool" where
"has_holo_extension_at f c ⟷
(∃r>0. ∃g. g holomorphic_on ball (complex_of_real c) r
∧ (∀x. ¦x - c¦ < r ⟶ g (complex_of_real x) = complex_of_real (f x)))"
lemma real_analytic_at_1d_imp_holo_extension:
fixes f :: "real ⇒ real"
assumes "real_analytic_at_1d f c"
shows "has_holo_extension_at f c"
proof -
from assms obtain r where r: "0 < r"
and TS: "⋀x. ¦x - c¦ < r ⟹
(λn. (deriv ^^ n) f c / fact n * (x - c) ^ n) sums f x"
unfolding real_analytic_at_1d_def by blast
define b :: "nat ⇒ complex" where "b = (λn. complex_of_real ((deriv ^^ n) f c / fact n))"
define g :: "complex ⇒ complex" where
"g = (λw. ∑n. b n * (w - complex_of_real c) ^ n)"
have summ_complex: "summable (λn. b n * (w - complex_of_real c) ^ n)"
if w: "w ∈ ball (complex_of_real c) r" for w
proof -
have nw: "norm (w - complex_of_real c) < r"
using w by (simp add: dist_norm norm_minus_commute)
define s where "s = (norm (w - complex_of_real c) + r) / 2"
have s_pos: "0 < s"
proof -
have "0 < norm (w - complex_of_real c) + r"
using r norm_ge_zero[of "w - complex_of_real c"] by linarith
thus ?thesis by (simp add: s_def)
qed
have s_lt_r: "s < r" using nw by (simp add: s_def)
have nw_lt_s: "norm (w - complex_of_real c) < s"
using nw by (simp add: s_def)
have "¦(c + s) - c¦ < r" using s_pos s_lt_r by simp
from TS[OF this] have realsum:
"summable (λn. (deriv ^^ n) f c / fact n * ((c + s) - c) ^ n)"
by (rule sums_summable)
have realsum': "summable (λn. (deriv ^^ n) f c / fact n * s ^ n)"
using realsum by simp
have cast: "summable (λn. b n * (complex_of_real s) ^ n)"
proof -
have "(λn. of_real ((deriv ^^ n) f c / fact n * s ^ n) :: complex)
= (λn. b n * (complex_of_real s) ^ n)"
by (simp only: b_def of_real_mult of_real_power)
moreover have "summable (λn. of_real ((deriv ^^ n) f c / fact n * s ^ n) :: complex)"
using realsum' by (rule summable_of_real)
ultimately show ?thesis by simp
qed
have "norm (w - complex_of_real c) < norm (complex_of_real s)"
using nw_lt_s s_pos by simp
from powser_inside[OF cast this]
show ?thesis .
qed
have sums_g: "(λn. b n * (w - complex_of_real c) ^ n) sums g w"
if w: "w ∈ ball (complex_of_real c) r" for w
using summ_complex[OF w] by (simp add: g_def summable_sums)
have holo: "g holomorphic_on ball (complex_of_real c) r"
proof (rule power_series_holomorphic)
fix w :: complex assume "w ∈ ball (complex_of_real c) r"
thus "(λn. b n * (w - complex_of_real c) ^ n) sums g w"
by (rule sums_g)
qed
have realaxis: "g (complex_of_real x) = complex_of_real (f x)"
if x: "¦x - c¦ < r" for x
proof -
have wball: "complex_of_real x ∈ ball (complex_of_real c) r"
using x by (simp add: dist_norm norm_minus_commute flip: of_real_diff)
have "(λn. b n * (complex_of_real x - complex_of_real c) ^ n) sums g (complex_of_real x)"
by (rule sums_g[OF wball])
moreover have
"(λn. b n * (complex_of_real x - complex_of_real c) ^ n)
= (λn. complex_of_real ((deriv ^^ n) f c / fact n * (x - c) ^ n))"
by (simp only: b_def of_real_mult of_real_power flip: of_real_diff)
ultimately have
"(λn. complex_of_real ((deriv ^^ n) f c / fact n * (x - c) ^ n))
sums g (complex_of_real x)" by simp
moreover have
"(λn. complex_of_real ((deriv ^^ n) f c / fact n * (x - c) ^ n))
sums complex_of_real (f x)"
using TS[OF x] by (rule sums_of_real)
ultimately show ?thesis by (rule sums_unique2)
qed
show ?thesis
unfolding has_holo_extension_at_def
using r holo realaxis by blast
qed
text ‹A real function with a holomorphic extension around ‹c› is real-analytic
at ‹c›.›
lemma holo_extension_imp_real_analytic_at_1d:
fixes f :: "real ⇒ real"
assumes "has_holo_extension_at f c"
shows "real_analytic_at_1d f c"
proof -
from assms obtain r g where r: "0 < r"
and holo: "g holomorphic_on ball (complex_of_real c) r"
and onaxis: "⋀x. ¦x - c¦ < r ⟹ g (complex_of_real x) = complex_of_real (f x)"
unfolding has_holo_extension_at_def by blast
define A :: "nat ⇒ complex" where
"A = (λn. (deriv ^^ n) g (complex_of_real c) / fact n)"
define a :: "nat ⇒ real" where "a = (λn. Re (A n))"
have PS: "(λn. a n * (x - c) ^ n) sums f x" if x: "¦x - c¦ < r" for x
proof -
have wball: "complex_of_real x ∈ ball (complex_of_real c) r"
using x by (simp add: dist_norm norm_minus_commute flip: of_real_diff)
have cseries: "(λn. A n * (complex_of_real x - complex_of_real c) ^ n)
sums g (complex_of_real x)"
unfolding A_def by (rule holomorphic_power_series[OF holo wball])
have eqf: "g (complex_of_real x) = complex_of_real (f x)" by (rule onaxis[OF x])
have term_eq: "A n * (complex_of_real x - complex_of_real c) ^ n
= complex_of_real (a n * (x - c) ^ n)
+ 𝗂 * complex_of_real (Im (A n) * (x - c) ^ n)" for n
proof -
have pw: "(complex_of_real x - complex_of_real c) ^ n
= complex_of_real ((x - c) ^ n)"
by (simp flip: of_real_diff of_real_power)
have "A n * (complex_of_real x - complex_of_real c) ^ n
= A n * complex_of_real ((x - c) ^ n)" by (simp only: pw)
also have "… = complex_of_real (Re (A n) * (x - c) ^ n)
+ 𝗂 * complex_of_real (Im (A n) * (x - c) ^ n)"
by (simp add: complex_eq_iff)
finally show ?thesis by (simp add: a_def)
qed
have cseries': "(λn. complex_of_real (a n * (x - c) ^ n)
+ 𝗂 * complex_of_real (Im (A n) * (x - c) ^ n))
sums complex_of_real (f x)"
using cseries by (simp add: term_eq eqf)
have "(λn. Re (complex_of_real (a n * (x - c) ^ n)
+ 𝗂 * complex_of_real (Im (A n) * (x - c) ^ n)))
sums Re (complex_of_real (f x))"
by (rule sums_Re[OF cseries'])
thus ?thesis by simp
qed
show ?thesis by (rule real_powser_imp_real_analytic_at_1d[OF r PS])
qed
theorem real_analytic_at_1d_iff_holo_extension:
fixes f :: "real ⇒ real"
shows "real_analytic_at_1d f c ⟷ has_holo_extension_at f c"
using real_analytic_at_1d_imp_holo_extension holo_extension_imp_real_analytic_at_1d
by blast
end