Theory PNT_Complex_Analysis_Lemmas
theory PNT_Complex_Analysis_Lemmas
imports
"PNT_Remainder_Library"
begin
unbundle pnt_notation
section ‹Some basic theorems in complex analysis›
subsection ‹Introduction rules for holomorphic functions and analytic functions›
lemma holomorphic_on_shift [holomorphic_intros]:
assumes "f holomorphic_on ((λz. s + z) ` A)"
shows "(λz. f (s + z)) holomorphic_on A"
proof -
have "(f ∘ (λz. s + z)) holomorphic_on A"
using assms by (intro holomorphic_on_compose holomorphic_intros)
thus ?thesis unfolding comp_def by auto
qed
lemma holomorphic_logderiv [holomorphic_intros]:
assumes "f holomorphic_on A" "open A" "⋀z. z ∈ A ⟹ f z ≠ 0"
shows "(λs. logderiv f s) holomorphic_on A"
using assms unfolding logderiv_def by (intro holomorphic_intros)
lemma holomorphic_glue_to_analytic:
assumes o: "open S" "open T"
and hf: "f holomorphic_on S"
and hg: "g holomorphic_on T"
and hI: "⋀z. z ∈ S ⟹ z ∈ T ⟹ f z = g z"
and hU: "U ⊆ S ∪ T"
obtains h
where "h analytic_on U"
"⋀z. z ∈ S ⟹ h z = f z"
"⋀z. z ∈ T ⟹ h z = g z"
proof -
define h where "h z ≡ if z ∈ S then f z else g z" for z
show ?thesis proof
have "h holomorphic_on S ∪ T"
unfolding h_def by (rule holomorphic_on_If_Un) (use assms in auto)
thus "h analytic_on U"
by (subst analytic_on_holomorphic) (use hU o in auto)
next
fix z assume *:"z ∈ S"
show "h z = f z" unfolding h_def using * by auto
next
fix z assume *:"z ∈ T"
show "h z = g z" unfolding h_def using * hI by auto
qed
qed
lemma analytic_on_powr_right [analytic_intros]:
assumes "f analytic_on s"
shows "(λz. w powr f z) analytic_on s"
proof (cases "w = 0")
case False
with assms show ?thesis
unfolding analytic_on_def holomorphic_on_def field_differentiable_def
by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
qed simp
subsection ‹Factorization of analytic function on compact region›
definition not_zero_on (infixr "not'_zero'_on" 46)
where "f not_zero_on S ≡ ∃z ∈ S. f z ≠ 0"
lemma not_zero_on_obtain:
assumes "f not_zero_on S" and "S ⊆ T"
obtains t where "f t ≠ 0" and "t ∈ T"
using assms unfolding not_zero_on_def by auto
lemma analytic_on_holomorphic_connected:
assumes hf: "f analytic_on S"
and con: "connected A"
and ne: "ξ ∈ A" and AS: "A ⊆ S"
obtains T T' where
"f holomorphic_on T" "f holomorphic_on T'"
"open T" "open T'" "A ⊆ T" "S ⊆ T'" "connected T"
proof -
obtain T'
where oT': "open T'" and sT': "S ⊆ T'"
and holf': "f holomorphic_on T'"
using analytic_on_holomorphic hf by blast
define T where "T ≡ connected_component_set T' ξ"
have TT': "T ⊆ T'" unfolding T_def by (rule connected_component_subset)
hence holf: "f holomorphic_on T" using holf' by auto
have opT: "open T" unfolding T_def using oT' by (rule open_connected_component)
have conT: "connected T" unfolding T_def by (rule connected_connected_component)
have "A ⊆ T'" using AS sT' by blast
hence AT: "A ⊆ T" unfolding T_def using ne con by (intro connected_component_maximal)
show ?thesis using holf holf' opT oT' AT sT' conT that by blast
qed
lemma analytic_factor_zero:
assumes hf: "f analytic_on S"
and KS: "K ⊆ S" and con: "connected K"
and ξK: "ξ ∈ K" and ξz: "f ξ = 0"
and nz: "f not_zero_on K"
obtains g r n
where "0 < n" "0 < r"
"g analytic_on S" "g not_zero_on K"
"⋀z. z ∈ S ⟹ f z = (z - ξ)^n * g z"
"⋀z. z ∈ ball ξ r ⟹ g z ≠ 0"
proof -
have "f analytic_on S" "connected K"
"ξ ∈ K" "K ⊆ S" using assms by auto
then obtain T T'
where holf: "f holomorphic_on T"
and holf': "f holomorphic_on T'"
and opT: "open T" and oT': "open T'"
and KT: "K ⊆ T" and ST': "S ⊆ T'"
and conT: "connected T"
by (rule analytic_on_holomorphic_connected)
obtain η where fη: "f η ≠ 0" and ηK: "η ∈ K"
using nz by (rule not_zero_on_obtain, blast)
hence ξT: "ξ ∈ T" and ξT': "ξ ∈ T'"
and ηT: "η ∈ T" using ξK ηK KT KS ST' by blast+
hence nc: "¬ f constant_on T" using fη ξz unfolding constant_on_def by fastforce
obtain g r n
where 1: "0 < n" and 2: "0 < r"
and bT: "ball ξ r ⊆ T"
and hg: "g holomorphic_on ball ξ r"
and fw: "⋀z. z ∈ ball ξ r ⟹ f z = (z - ξ) ^ n * g z"
and gw: "⋀z. z ∈ ball ξ r ⟹ g z ≠ 0"
by (rule holomorphic_factor_zero_nonconstant, (rule holf opT conT ξT ξz nc)+, blast)
have sT: "S ⊆ T' - {ξ} ∪ ball ξ r" using 2 ST' by auto
have hz: "(λz. f z / (z - ξ) ^ n) holomorphic_on (T' - {ξ})"
using holf' by ((intro holomorphic_intros)+, auto)
obtain h
where 3: "h analytic_on S"
and hf: "⋀z. z ∈ T' - {ξ} ⟹ h z = f z / (z - ξ) ^ n"
and hb: "⋀z. z ∈ ball ξ r ⟹ h z = g z"
by (rule holomorphic_glue_to_analytic
[where f = "λz. f z / (z - ξ) ^ n" and
g = g and S = "T' - {ξ}" and T = "ball ξ r" and U = S])
(use oT' 2 ST' hg fw hz in ‹auto simp add: holomorphic_intros›)
have "ξ ∈ ball ξ r" using 2 by auto
hence "h ξ ≠ 0" using hb gw 2 by auto
hence 4: "h not_zero_on K" unfolding not_zero_on_def using ξK by auto
have 5: "f z = (z - ξ)^n * h z" if *: "z ∈ S" for z
proof -
consider "z = ξ" | "z ∈ S - {ξ}" using * by auto
thus ?thesis proof cases
assume *: "z = ξ"
show ?thesis using ξz 1 by (subst (1 2) *, auto)
next
assume *: "z ∈ S - {ξ}"
show ?thesis using hf ST' * by (auto simp add: field_simps)
qed
qed
have 6: "⋀w. w ∈ ball ξ r ⟹ h w ≠ 0" using hb gw by auto
show ?thesis by ((standard; rule 1 2 3 4 5 6), blast+)
qed
lemma analytic_compact_finite_zeros:
assumes af: "f analytic_on S"
and KS: "K ⊆ S"
and con: "connected K"
and cm: "compact K"
and nz: "f not_zero_on K"
shows "finite {z ∈ K. f z = 0}"
proof (cases "f constant_on K")
assume *: "f constant_on K"
have "⋀z. z ∈ K ⟹ f z ≠ 0" using nz * unfolding not_zero_on_def constant_on_def by auto
hence **: "{z ∈ K. f z = 0} = {}" by auto
thus ?thesis by (subst **, auto)
next
assume *: "¬ f constant_on K"
obtain ξ where ne: "ξ ∈ K" using not_zero_on_obtain nz by blast
obtain T T' where opT: "open T" and conT: "connected T"
and ST: "K ⊆ T" and holf: "f holomorphic_on T"
and "f holomorphic_on T'"
by (metis af KS con ne analytic_on_holomorphic_connected)
have "¬ f constant_on T" using ST * unfolding constant_on_def by blast
thus ?thesis using holf opT conT cm ST by (intro holomorphic_compact_finite_zeros)
qed
subsubsection ‹Auxiliary propositions for theorem ‹analytic_factorization››
definition analytic_factor_p' where
‹analytic_factor_p' f S K ≡
∃g n. ∃α :: nat ⇒ complex.
g analytic_on S
∧ (∀z ∈ K. g z ≠ 0)
∧ (∀z ∈ S. f z = g z * (∏k<n. z - α k))
∧ α ` {..<n} ⊆ K›
definition analytic_factor_p where
‹analytic_factor_p F ≡
∀f S K. f analytic_on S
⟶ K ⊆ S
⟶ connected K
⟶ compact K
⟶ f not_zero_on K
⟶ {z ∈ K. f z = 0} = F
⟶ analytic_factor_p' f S K›
lemma analytic_factorization_E:
shows "analytic_factor_p {}"
unfolding analytic_factor_p_def
proof (intro conjI allI impI)
fix f S K
assume af: "f analytic_on S"
and KS: "K ⊆ S"
and con: "connected K"
and cm: "compact K"
and nz: "{z ∈ K. f z = 0} = {}"
show "analytic_factor_p' f S K"
unfolding analytic_factor_p'_def
proof (intro ballI conjI exI)
show "f analytic_on S" "⋀z. z ∈ K ⟹ f z ≠ 0"
"⋀z. z ∈ S ⟹ f z = f z * (∏k<(0 :: nat). z - (λ_. 0) k)"
by (rule af, use nz in auto)
show "(λk :: nat. 0) ` {..<0} ⊆ K" by auto
qed
qed
lemma analytic_factorization_I:
assumes ind: "analytic_factor_p F"
and ξni: "ξ ∉ F"
shows "analytic_factor_p (insert ξ F)"
unfolding analytic_factor_p_def
proof (intro allI impI)
fix f S K
assume af: "f analytic_on S"
and KS: "K ⊆ S"
and con: "connected K"
and nz: "f not_zero_on K"
and cm: "compact K"
and zr: "{z ∈ K. f z = 0} = insert ξ F"
show "analytic_factor_p' f S K"
proof -
have "f analytic_on S" "K ⊆ S" "connected K"
"ξ ∈ K" "f ξ = 0" "f not_zero_on K"
using af KS con zr nz by auto
then obtain h r k
where "0 < k" and "0 < r" and ah: "h analytic_on S"
and nh: "h not_zero_on K"
and f_z: "⋀z. z ∈ S ⟹ f z = (z - ξ) ^ k * h z"
and ball: "⋀z. z ∈ ball ξ r ⟹ h z ≠ 0"
by (rule analytic_factor_zero) blast
hence hξ: "h ξ ≠ 0" using ball by auto
hence "⋀z. z ∈ K ⟹ h z = 0 ⟷ f z = 0 ∧ z ≠ ξ" by (subst f_z) (use KS in auto)
hence "{z ∈ K. h z = 0} = {z ∈ K. f z = 0} - {ξ}" by auto
also have "… = F" by (subst zr, intro Diff_insert_absorb ξni)
finally have "{z ∈ K. h z = 0} = F" .
hence "analytic_factor_p' h S K"
using ind ah KS con cm nh
unfolding analytic_factor_p_def by auto
then obtain g n and α :: "nat ⇒ complex"
where ag: "g analytic_on S" and
ng: "⋀z. z ∈ K ⟹ g z ≠ 0" and
h_z: "⋀z. z ∈ S ⟹ h z = g z * (∏k<n. z - α k)" and
Imα: "α ` {..<n} ⊆ K"
unfolding analytic_factor_p'_def by fastforce
define β where "β j ≡ if j < n then α j else ξ" for j
show ?thesis
unfolding analytic_factor_p'_def
proof (intro ballI conjI exI)
show "g analytic_on S" "⋀z. z ∈ K ⟹ g z ≠ 0"
by (rule ag, rule ng)
next
fix z assume *: "z ∈ S"
show "f z = g z * (∏j<n+k. z - β j)"
proof -
have "(∏j<n. z - β j) = (∏j<n. z - α j)"
"(∏j=n..<n+k. z - β j) = (z - ξ) ^ k"
unfolding β_def by auto
moreover have "(∏j<n+k. z - β j) = (∏j<n. z - β j) * (∏j=n..<n+k. z - β j)"
by (metis Metric_Arith.nnf_simps(8) atLeast0LessThan
not_add_less1 prod.atLeastLessThan_concat zero_order(1))
ultimately have "(∏j<n+k. z - β j) = (z - ξ) ^ k * (∏j<n. z - α j)" by auto
moreover have "f z = g z * ((z - ξ) ^ k * (∏j<n. z - α j))"
by (subst f_z; (subst h_z)?, use * in auto)
ultimately show ?thesis by auto
qed
next
show "β ` {..<n + k} ⊆ K" unfolding β_def using Imα ‹ξ ∈ K› by auto
qed
qed
qed
text ‹A nontrivial analytic function on connected compact region can
be factorized as a everywhere-non-zero function and linear terms $z - s_0$
for all zeros $s_0$. Note that the connected assumption of $K$ may be
removed, but we remain it just for simplicity of proof.›
theorem analytic_factorization:
assumes af: "f analytic_on S"
and KS: "K ⊆ S"
and con: "connected K"
and "compact K"
and "f not_zero_on K"
obtains g n and α :: "nat ⇒ complex" where
"g analytic_on S"
"⋀z. z ∈ K ⟹ g z ≠ 0"
"⋀z. z ∈ S ⟹ f z = g z * (∏k<n. (z - α k))"
"α ` {..<n} ⊆ K"
proof -
have ‹finite {z ∈ K. f z = 0}› using assms by (rule analytic_compact_finite_zeros)
moreover have ‹finite F ⟹ analytic_factor_p F› for F
by (induct rule: finite_induct; rule analytic_factorization_E analytic_factorization_I)
ultimately have "analytic_factor_p {z ∈ K. f z = 0}" by auto
hence "analytic_factor_p' f S K" unfolding analytic_factor_p_def using assms by auto
thus ?thesis unfolding analytic_factor_p'_def using assms that by metis
qed
subsection ‹Schwarz theorem in complex analysis›
lemma Schwarz_Lemma1:
fixes f :: "complex ⇒ complex"
and ξ :: "complex"
assumes "f holomorphic_on ball 0 1"
and "f 0 = 0"
and "⋀z. ∥z∥ < 1 ⟹ ∥f z∥ ≤ 1"
and "∥ξ∥ < 1"
shows "∥f ξ∥ ≤ ∥ξ∥"
proof (cases "f constant_on ball 0 1")
assume "f constant_on ball 0 1"
thus ?thesis unfolding constant_on_def
using assms by auto
next
assume nc: "¬f constant_on ball 0 1"
have "⋀z. ∥z∥ < 1 ⟹ ∥f z∥ < 1"
proof -
fix z :: complex assume *: "∥z∥ < 1"
have "∥f z∥ ≠ 1"
proof
assume "∥f z∥ = 1"
hence "⋀w. w ∈ ball 0 1 ⟹ ∥f w∥ ≤ ∥f z∥"
using assms(3) by auto
hence "f constant_on ball 0 1"
by (intro maximum_modulus_principle [where U = "ball 0 1" and ξ = z])
(use * assms(1) in auto)
thus False using nc by blast
qed
with assms(3) [OF *] show "∥f z∥ < 1" by auto
qed
thus "∥f ξ∥ ≤ ∥ξ∥" by (intro Schwarz_Lemma(1), use assms in auto)
qed
theorem Schwarz_Lemma2:
fixes f :: "complex ⇒ complex"
and ξ :: "complex"
assumes holf: "f holomorphic_on ball 0 R"
and hR: "0 < R" and nz: "f 0 = 0"
and bn: "⋀z. ∥z∥ < R ⟹ ∥f z∥ ≤ 1"
and ξR: "∥ξ∥ < R"
shows "∥f ξ∥ ≤ ∥ξ∥ / R"
proof -
define φ where "φ z ≡ f (R * z)" for z :: complex
have "∥ξ / R∥ < 1" using ξR hR by (subst nonzero_norm_divide, auto)
moreover have "f holomorphic_on (*) (R :: complex) ` ball 0 1"
by (rule holomorphic_on_subset, rule holf)
(use hR in ‹auto simp: norm_mult›)
hence "(f ∘ (λz. R * z)) holomorphic_on ball 0 1"
by (auto intro: holomorphic_on_compose)
moreover have "φ 0 = 0" unfolding φ_def using nz by auto
moreover have "⋀z. ∥z∥ < 1 ⟹ ∥φ z∥ ≤ 1"
proof -
fix z :: complex assume *: "∥z∥ < 1"
have "∥R*z∥ < R" using hR * by (fold scaleR_conv_of_real) auto
thus "∥φ z∥ ≤ 1" unfolding φ_def using bn by auto
qed
ultimately have "∥φ (ξ / R)∥ ≤ ∥ξ / R∥"
unfolding comp_def by (fold φ_def, intro Schwarz_Lemma1)
thus ?thesis unfolding φ_def using hR by (subst (asm) nonzero_norm_divide, auto)
qed
subsection ‹Borel-Carathedory theorem›
text ‹Borel-Carathedory theorem, from book
‹Theorem 5.5, The Theory of Functions, E. C. Titchmarsh››
lemma Borel_Caratheodory1:
assumes hr: "0 < R" "0 < r" "r < R"
and f0: "f 0 = 0"
and hf: "⋀z. ∥z∥ < R ⟹ Re (f z) ≤ A"
and holf: "f holomorphic_on (ball 0 R)"
and zr: "∥z∥ ≤ r"
shows "∥f z∥ ≤ 2*r/(R-r) * A"
proof -
have A_ge_0: "A ≥ 0"
using f0 hf by (metis hr(1) norm_zero zero_complex.simps(1))
then consider "A = 0" | "A > 0" by linarith
thus "∥f z∥ ≤ 2 * r/(R-r) * A"
proof (cases)
assume *: "A = 0"
have 1: "⋀w. w ∈ ball 0 R ⟹ ∥exp (f w)∥ ≤ ∥exp (f 0)∥" using hf f0 * by auto
have 2: "exp ∘ f constant_on (ball 0 R)"
by (rule maximum_modulus_principle [where f = "exp ∘ f" and U = "ball 0 R"])
(use 1 hr(1) in ‹auto intro: holomorphic_on_compose holf holomorphic_on_exp›)
have "f constant_on (ball 0 R)"
proof (rule classical)
assume *: "¬ f constant_on ball 0 R"
have "open (f ` (ball 0 R))"
by (rule open_mapping_thm [where S = "ball 0 R"], use holf * in auto)
then obtain e where "e > 0" and "cball 0 e ⊆ f ` (ball 0 R)"
by (metis hr(1) f0 centre_in_ball imageI open_contains_cball)
then obtain w
where hw: "w ∈ ball 0 R" "f w = e"
by (metis abs_of_nonneg imageE less_eq_real_def mem_cball_0 norm_of_real subset_eq)
have "exp e = exp (f w)"
using hw(2) by (fold exp_of_real) auto
also have "… = exp (f 0)"
using hw(1) 2 hr(1) unfolding constant_on_def comp_def by auto
also have "… = exp (0 :: real)" by (subst f0) auto
finally have "e = 0" by auto
with ‹e > 0› show ?thesis by blast
qed
hence "f z = 0" using f0 hr zr unfolding constant_on_def by auto
hence "∥f z∥ = 0" by auto
also have "… ≤ 2 * r/(R-r) * A" using hr ‹A ≥ 0› by auto
finally show ?thesis .
next
assume A_gt_0: "A > 0"
define φ where "φ z ≡ (f z)/(2*A - f z)" for z :: complex
have φ_bound: "∥φ z∥ ≤ 1" if *: "∥z∥ < R" for z
proof -
define u v where "u ≡ Re (f z)" and "v ≡ Im (f z)"
hence "u ≤ A" unfolding u_def using hf * by blast
hence "u⇧2 ≤ (2*A-u)⇧2" using A_ge_0 by (simp add: sqrt_ge_absD)
hence "u⇧2 + v⇧2 ≤ (2*A-u)⇧2 + (-v)⇧2" by auto
moreover have "2*A - f z = Complex (2*A-u) (-v)" by (simp add: complex_eq_iff u_def v_def)
hence "∥f z∥⇧2 = u⇧2 + v⇧2"
"∥2*A - f z∥⇧2 = (2*A-u)⇧2 + (-v)⇧2"
unfolding u_def v_def using cmod_power2 complex.sel by presburger+
ultimately have "∥f z∥⇧2 ≤ ∥2*A - f z∥⇧2" by auto
hence "∥f z∥ ≤ ∥2*A - f z∥" by auto
thus ?thesis unfolding φ_def by (subst norm_divide) (simp add: divide_le_eq_1)
qed
moreover have nz: "⋀z :: complex. z ∈ ball 0 R ⟹ 2*A - f z ≠ 0"
proof
fix z :: complex
assume *: "z ∈ ball 0 R"
and eq: "2*A - f z = 0"
hence "Re (f z) ≤ A" using hf by auto
moreover have "Re (f z) = 2*A"
by (metis eq Re_complex_of_real right_minus_eq)
ultimately show False using A_gt_0 by auto
qed
ultimately have "φ holomorphic_on ball 0 R"
unfolding φ_def comp_def by (intro holomorphic_intros holf)
moreover have "φ 0 = 0" unfolding φ_def using f0 by auto
ultimately have *: "∥φ z∥ ≤ ∥z∥ / R"
using hr(1) φ_bound zr hr Schwarz_Lemma2 by auto
also have "... < 1" using zr hr by auto
finally have hφ: "∥φ z∥ ≤ r / R" "∥φ z∥ < 1" "1 + φ z ≠ 0"
proof (safe)
show "∥φ z∥ ≤ r / R" using * zr hr(1)
by (metis divide_le_cancel dual_order.trans nle_le)
next
assume "1 + φ z = 0"
hence "φ z = -1" using add_eq_0_iff by blast
thus "∥φ z∥ < 1 ⟹ False" by auto
qed
have "2*A - f z ≠ 0" using nz hr(3) zr by auto
hence "f z = 2*A*φ z / (1 + φ z)"
using hφ(3) unfolding φ_def by (auto simp add: field_simps)
hence "∥f z∥ = 2*A*∥φ z∥ / ∥1 + φ z∥"
by (auto simp add: norm_divide norm_mult A_ge_0)
also have "… ≤ 2*A*(∥φ z∥ / (1 - ∥φ z∥))"
proof -
have "∥1 + φ z∥ ≥ 1 - ∥φ z∥"
by (metis norm_diff_ineq norm_one)
thus ?thesis
by (simp, rule divide_left_mono, use A_ge_0 in auto)
(intro mult_pos_pos, use hφ(2) in auto)
qed
also have "… ≤ 2*A*((r/R) / (1 - r/R))"
proof -
have *: "a / (1 - a) ≤ b / (1 - b)"
if "a < 1" "b < 1" "a ≤ b" for a b :: real
using that by (auto simp add: field_simps)
have "∥φ z∥ / (1 - ∥φ z∥) ≤ (r/R) / (1 - r/R)"
by (rule *; (intro hφ)?) (use hr in auto)
thus ?thesis by (rule mult_left_mono, use A_ge_0 in auto)
qed
also have "… = 2*r/(R-r) * A" using hr(1) by (auto simp add: field_simps)
finally show ?thesis .
qed
qed
lemma Borel_Caratheodory2:
assumes hr: "0 < R" "0 < r" "r < R"
and hf: "⋀z. ∥z∥ < R ⟹ Re (f z - f 0) ≤ A"
and holf: "f holomorphic_on (ball 0 R)"
and zr: "∥z∥ ≤ r"
shows "∥f z - f 0∥ ≤ 2*r/(R-r) * A"
proof -
define g where "g z ≡ f z - f 0" for z
show ?thesis
by (fold g_def, rule Borel_Caratheodory1)
(unfold g_def, insert assms, auto intro: holomorphic_intros)
qed
theorem Borel_Caratheodory3:
assumes hr: "0 < R" "0 < r" "r < R"
and hf: "⋀w. w ∈ ball s R ⟹ Re (f w - f s) ≤ A"
and holf: "f holomorphic_on (ball s R)"
and zr: "z ∈ ball s r"
shows "∥f z - f s∥ ≤ 2*r/(R-r) * A"
proof -
define g where "g w ≡ f (s + w)" for w
have "⋀w. ∥w∥ < R ⟹ Re (f (s + w) - f s) ≤ A"
by (intro hf) (auto simp add: dist_complex_def)
hence "∥g (z - s) - g 0∥ ≤ 2*r/(R-r) * A"
by (intro Borel_Caratheodory2, unfold g_def, insert assms)
(auto intro: holomorphic_intros simp add: dist_complex_def norm_minus_commute)
thus ?thesis unfolding g_def by auto
qed
subsection ‹Lemma 3.9›
text‹These lemmas is referred to the following material: Theorem 3.9,
‹The Theory of the Riemann Zeta-Function, E. C. Titchmarsh, D. R. Heath-Brown›.›
lemma lemma_3_9_beta1:
fixes f M r s⇩0
assumes zl: "0 < r" "0 ≤ M"
and hf: "f holomorphic_on ball 0 r"
and ne: "⋀z. z ∈ ball 0 r ⟹ f z ≠ 0"
and bn: "⋀z. z ∈ ball 0 r ⟹ ∥f z / f 0∥ ≤ exp M"
shows "∥logderiv f 0∥ ≤ 4 * M / r"
and "∀s∈cball 0 (r / 4). ∥logderiv f s∥ ≤ 8 * M / r"
proof (goal_cases)
obtain g
where holg: "g holomorphic_on ball 0 r"
and exp_g: "⋀x. x ∈ ball 0 r ⟹ exp (g x) = f x"
by (rule holomorphic_logarithm_exists [of "ball 0 r" f 0])
(use zl(1) ne hf in auto)
have f0: "exp (g 0) = f 0" using exp_g zl(1) by auto
have "Re (g z - g 0) ≤ M" if *: "∥z∥ < r" for z
proof -
have "exp (Re (g z - g 0)) = ∥exp (g z - g 0)∥"
by (rule norm_exp_eq_Re [symmetric])
also have "… = ∥f z / f 0∥"
by (subst exp_diff, subst f0, subst exp_g)
(use * in auto)
also have "… ≤ exp M" by (rule bn) (use * in auto)
finally show ?thesis by auto
qed
hence "∥g z - g 0∥ ≤ 2 * (r / 2) / (r - r / 2) * M"
if *: "∥z∥ ≤ r / 2" for z
by (intro Borel_Caratheodory2 [where f = g])
(use zl(1) holg * in auto)
also have "… = 2 * M" using zl(1) by auto
finally have hg: "⋀z. ∥z∥ ≤ r / 2 ⟹ ∥g z - g 0∥ ≤ 2 * M" .
have result: "∥logderiv f s∥ ≤ 2 * M / r'"
when "cball s r' ⊆ cball 0 (r / 2)" "0 < r'" "∥s∥ < r / 2" for s r'
proof -
have contain: "⋀z. ∥s - z∥ ≤ r' ⟹ ∥z∥ ≤ r / 2"
using that by (auto simp add: cball_def subset_eq dist_complex_def)
have contain': "∥z∥ < r" when "∥s - z∥ ≤ r'" for z
using zl(1) contain [of z] that by auto
have s_in_ball: "s ∈ ball 0 r" using that(3) zl(1) by auto
have "deriv f s = deriv (λx. exp (g x)) s"
by (rule deriv_cong_ev, subst eventually_nhds)
(rule exI [where x = "ball 0 (r / 2)"], use exp_g zl(1) that(3) in auto)
also have "… = exp (g s) * deriv g s"
by (intro DERIV_fun_exp [THEN DERIV_imp_deriv] field_differentiable_derivI)
(meson holg open_ball s_in_ball holomorphic_on_imp_differentiable_at)
finally have df: "logderiv f s = deriv g s"
proof -
assume "deriv f s = exp (g s) * deriv g s"
moreover have "f s ≠ 0" by (intro ne s_in_ball)
ultimately show ?thesis
unfolding logderiv_def using exp_g [OF s_in_ball] by auto
qed
have "⋀z. ∥s - z∥ = r' ⟹ ∥g z - g 0∥ ≤ 2 * M"
using contain by (intro hg) auto
moreover have "(λz. g z - g 0) holomorphic_on cball s r'"
by (rule holomorphic_on_subset [where s="ball 0 r"], insert holg)
(auto intro: holomorphic_intros contain' simp add: dist_complex_def)
moreover hence "continuous_on (cball s r') (λz. g z - g 0)"
by (rule holomorphic_on_imp_continuous_on)
ultimately have "∥(deriv ^^ 1) (λz. g z - g 0) s∥ ≤ fact 1 * (2 * M) / r' ^ 1"
using that(2) by (intro Cauchy_inequality) auto
also have "… = 2 * M / r'" by auto
also have "deriv g s = deriv (λz. g z - g 0) s"
by (subst deriv_diff, auto)
(rule holomorphic_on_imp_differentiable_at, use holg s_in_ball in auto)
hence "∥deriv g s∥ = ∥(deriv ^^ 1) (λz. g z - g 0) s∥"
by (auto simp add: derivative_intros)
ultimately show ?thesis by (subst df) auto
qed
case 1 show ?case using result [of 0 "r / 2"] zl(1) by auto
case 2 show ?case proof safe
fix s :: complex assume hs: "s ∈ cball 0 (r / 4)"
hence "z ∈ cball s (r / 4) ⟹ ∥z∥ ≤ r / 2" for z
using norm_triangle_sub [of "z" "s"]
by (auto simp add: dist_complex_def norm_minus_commute)
hence "∥logderiv f s∥ ≤ 2 * M / (r / 4)"
by (intro result) (use zl(1) hs in auto)
also have "… = 8 * M / r" by auto
finally show "∥logderiv f s∥ ≤ 8 * M / r" .
qed
qed
lemma lemma_3_9_beta1':
fixes f M r s⇩0
assumes zl: "0 < r" "0 ≤ M"
and hf: "f holomorphic_on ball s r"
and ne: "⋀z. z ∈ ball s r ⟹ f z ≠ 0"
and bn: "⋀z. z ∈ ball s r ⟹ ∥f z / f s∥ ≤ exp M"
and hs: "z ∈ cball s (r / 4)"
shows "∥logderiv f z∥ ≤ 8 * M / r"
proof -
define g where "g z ≡ f (s + z)" for z
have "∀z ∈ cball 0 (r / 4). ∥logderiv g z∥ ≤ 8 * M / r"
by (intro lemma_3_9_beta1 assms, unfold g_def)
(auto simp add: dist_complex_def intro!: assms holomorphic_on_shift)
note bspec [OF this, of "z - s"]
moreover have "f field_differentiable at z"
by (rule holomorphic_on_imp_differentiable_at [where ?s = "ball s r"])
(insert hs zl(1), auto intro: hf simp add: dist_complex_def)
ultimately show ?thesis unfolding g_def using hs
by (auto simp add: dist_complex_def logderiv_shift)
qed
lemma lemma_3_9_beta2:
fixes f M r
assumes zl: "0 < r" "0 ≤ M"
and af: "f analytic_on cball 0 r"
and f0: "f 0 ≠ 0"
and rz: "⋀z. z ∈ cball 0 r ⟹ Re z > 0 ⟹ f z ≠ 0"
and bn: "⋀z. z ∈ cball 0 r ⟹ ∥f z / f 0∥ ≤ exp M"
and hg: "Γ ⊆ {z ∈ cball 0 (r / 2). f z = 0 ∧ Re z ≤ 0}"
shows "- Re (logderiv f 0) ≤ 8 * M / r + Re (∑z∈Γ. 1 / z)"
proof -
have nz': "f not_zero_on cball 0 (r / 2)"
unfolding not_zero_on_def using f0 zl(1) by auto
hence fin_zeros: "finite {z ∈ cball 0 (r / 2). f z = 0}"
by (intro analytic_compact_finite_zeros [where S = "cball 0 r"])
(use af zl in auto)
obtain g n and α :: "nat ⇒ complex"
where ag: "g analytic_on cball 0 r"
and ng: "⋀z. z ∈ cball 0 (r / 2) ⟹ g z ≠ 0"
and fac: "⋀z. z ∈ cball 0 r ⟹ f z = g z * (∏k<n. (z - α k))"
and Imα: "α ` {..<n} ⊆ cball 0 (r / 2)"
by (rule analytic_factorization [
where K = "cball 0 (r / 2)"
and S = "cball 0 r" and f = f])
(use zl(1) af nz' in auto)
have g0: "∥g 0∥ ≠ 0" using ng zl(1) by auto
hence "g holomorphic_on cball 0 r"
"(λz. g z / g 0) holomorphic_on cball 0 r"
using ag by (auto simp add: analytic_intros intro: analytic_imp_holomorphic)
hence holg:
"g holomorphic_on ball 0 r"
"(λz. g z / g 0) holomorphic_on ball 0 r"
"continuous_on (cball 0 r) (λz. g z / g 0)"
by (auto intro!: holomorphic_on_imp_continuous_on
holomorphic_on_subset [where t = "ball 0 r"])
have nz_α: "⋀k. k < n ⟹ α k ≠ 0" using zl(1) f0 fac by auto
have "∥g z / g 0∥ ≤ exp M" if *: "z ∈ sphere 0 r" for z
proof -
let ?p = "∥(∏k<n. (z - α k)) / (∏k<n. (0 - α k))∥"
have 1: "∥f z / f 0∥ ≤ exp M" using bn * by auto
have 2: "∥f z / f 0∥ = ∥g z / g 0∥ * ?p"
by (subst norm_mult [symmetric], subst (1 2) fac)
(use that zl(1) in auto)
have "?p = (∏k<n. (∥z - α k∥ / ∥0 - α k∥))"
by (auto simp add: prod_norm [symmetric] norm_divide prod_dividef)
also have "∥z - α k∥ ≥ ∥0 - α k∥" if "k < n" for k
proof (rule ccontr)
assume **: "¬ ∥z - α k∥ ≥ ∥0 - α k∥"
have "r = ∥z∥" using * by auto
also have "... ≤ ∥0 - α k∥ + ∥z - α k∥" by (simp add: norm_triangle_sub)
also have "... < 2 * ∥α k∥" using ** by auto
also have "α k ∈ cball 0 (r / 2)" using Imα that by blast
hence "2 * ∥α k∥ ≤ r" by auto
finally show False by linarith
qed
hence "⋀k. k < n ⟹ ∥z - α k∥ / ∥0 - α k∥ ≥ 1"
using nz_α by (subst le_divide_eq_1_pos) auto
hence "(∏k<n. (∥z - α k∥ / ∥0 - α k∥)) ≥ 1" by (rule prod_ge_1) simp
finally have 3: "?p ≥ 1" .
have rule1: "b = a * c ⟹ a ≥ 0 ⟹ c ≥ 1 ⟹ a ≤ b" for a b c :: real
by (metis landau_omega.R_mult_left_mono more_arith_simps(6))
have "∥g z / g 0∥ ≤ ∥f z / f 0∥"
by (rule rule1) (rule 2 3 norm_ge_zero)+
thus ?thesis using 1 by linarith
qed
hence "⋀z. z ∈ cball 0 r ⟹ ∥g z / g 0∥ ≤ exp M"
using holg
by (auto intro: maximum_modulus_frontier
[where f = "λz. g z / g 0" and S = "cball 0 r"])
hence bn': "⋀z. z ∈ cball 0 (r / 2) ⟹ ∥g z / g 0∥ ≤ exp M" using zl(1) by auto
have ag': "g analytic_on cball 0 (r / 2)"
by (rule analytic_on_subset [where S = "cball 0 r"])
(use ag zl(1) in auto)
have "∥logderiv g 0∥ ≤ 4 * M / (r / 2)"
by (rule lemma_3_9_beta1(1) [where f = g])
(use zl ng bn' holg in auto)
also have "… = 8 * M / r" by auto
finally have bn_g: "∥logderiv g 0∥ ≤ 8 * M / r" unfolding logderiv_def by auto
let ?P = "λw. ∏k<n. (w - α k)"
let ?S' = "∑k<n. logderiv (λz. z - α k) 0"
let ?S = "∑k<n. - (1 / α k)"
have "g field_differentiable at 0" using holg zl(1)
by (auto intro!: holomorphic_on_imp_differentiable_at)
hence ld_g: "g log_differentiable 0" unfolding log_differentiable_def using g0 by auto
have "logderiv ?P 0 = ?S'" and ld_P: "?P log_differentiable 0"
by (auto intro!: logderiv_linear nz_α logderiv_prod)
note this(1)
also have "?S' = ?S"
by (rule sum.cong)
(use nz_α in "auto cong: logderiv_linear(1)")
finally have cd_P: "logderiv ?P 0 = ?S" .
have "logderiv f 0 = logderiv (λz. g z * ?P z) 0"
by (rule logderiv_cong_ev, subst eventually_nhds)
(intro exI [where x = "ball 0 r"], use fac zl(1) in auto)
also have "… = logderiv g 0 + logderiv ?P 0"
by (subst logderiv_mult) (use ld_g ld_P in auto)
also have "… = logderiv g 0 + ?S" using cd_P by auto
finally have "Re (logderiv f 0) = Re (logderiv g 0) + Re ?S" by simp
moreover have "- Re (∑z∈Γ. 1 / z) ≤ Re ?S"
proof -
have "- Re (∑z∈Γ. 1 / z) = (∑z∈Γ. Re (- (1 / z)))" by (auto simp add: sum_negf)
also have "… ≤ (∑k<n. Re (- (1 / α k)))"
proof (rule sum_le_included)
show "∀z∈Γ. ∃k∈{..<n}. α k = z ∧ Re (- (1 / z)) ≤ Re (- (1 / α k))"
(is "Ball _ ?P")
proof
fix z assume hz: "z ∈ Γ"
have "∃k∈{..<n}. α k = z"
proof (rule ccontr)
assume ne_α: "¬ (∃k∈{..<n}. α k = z)"
have z_in: "z ∈ cball 0 (r / 2)" "z ∈ cball 0 r" using hg hz zl(1) by auto
hence "g z ≠ 0" using ng by auto
moreover have "(∏k<n. (z - α k)) ≠ 0" using ne_α hz by auto
ultimately have "f z ≠ 0" using fac z_in by auto
moreover have "f z = 0" using hz hg by auto
ultimately show False by auto
qed
thus "?P z" by auto
qed
show "∀k∈{..<n}. 0 ≤ Re (- (1 / α k))" (is "Ball _ ?P")
proof
fix k assume *: "k∈{..<n}"
have 1: "α k ∈ cball 0 r" using Imα zl(1) * by auto
hence "(∏j<n. (α k - α j)) = 0"
by (subst prod_zero_iff) (use * in auto)
with 1 have "f (α k) = 0" by (subst fac) auto
hence "Re (α k) ≤ 0" using "1" rz f0 by fastforce
hence "Re (1 * cnj (α k)) ≤ 0" by auto
thus "?P k" using Re_complex_div_le_0 by auto
qed
show "finite {..<n}" by auto
have "Γ ⊆ {z ∈ cball 0 (r / 2). f z = 0}" using hg by auto
thus "finite Γ" using fin_zeros by (rule finite_subset)
qed
also have "… = Re ?S" by auto
finally show ?thesis .
qed
ultimately have "- Re (logderiv f 0) - Re (∑z∈Γ. 1 / z) ≤ Re (- logderiv g 0)" by auto
also have "… ≤ ∥- logderiv g 0∥" by (rule complex_Re_le_cmod)
also have "… ≤ 8 * M / r" by simp (rule bn_g)
finally show ?thesis by auto
qed
theorem lemma_3_9_beta3:
fixes f M r and s :: complex
assumes zl: "0 < r" "0 ≤ M"
and af: "f analytic_on cball s r"
and f0: "f s ≠ 0"
and rz: "⋀z. z ∈ cball s r ⟹ Re z > Re s ⟹ f z ≠ 0"
and bn: "⋀z. z ∈ cball s r ⟹ ∥f z / f s∥ ≤ exp M"
and hg: "Γ ⊆ {z ∈ cball s (r / 2). f z = 0 ∧ Re z ≤ Re s}"
shows "- Re (logderiv f s) ≤ 8 * M / r + Re (∑z∈Γ. 1 / (z - s))"
proof -
define g where "g ≡ f ∘ (λz. s + z)"
define Δ where "Δ ≡ (λz. z - s) ` Γ"
hence 1: "g analytic_on cball 0 r"
unfolding g_def using af
by (intro analytic_on_compose) (auto simp add: analytic_intros)
moreover have "g 0 ≠ 0" unfolding g_def using f0 by auto
moreover have "(Re z > 0 ⟶ g z ≠ 0) ∧ ∥g z / g 0∥ ≤ exp M"
if hz: "z ∈ cball 0 r" for z
proof (intro impI conjI)
assume hz': "0 < Re z"
thus "g z ≠ 0" unfolding g_def comp_def
using hz by (intro rz) (auto simp add: dist_complex_def)
next
show "∥g z / g 0∥ ≤ exp M"
unfolding g_def comp_def using hz
by (auto simp add: dist_complex_def intro!: bn)
qed
moreover have "Δ ⊆ {z ∈ cball 0 (r / 2). g z = 0 ∧ Re z ≤ 0}"
proof safe
fix z assume "z ∈ Δ"
hence "s + z ∈ Γ" unfolding Δ_def by auto
thus "g z = 0" "Re z ≤ 0" "z ∈ cball 0 (r / 2)"
unfolding g_def comp_def using hg by (auto simp add: dist_complex_def)
qed
ultimately have "- Re (logderiv g 0) ≤ 8 * M / r + Re (∑z∈Δ. 1 / z)"
by (intro lemma_3_9_beta2) (use zl in auto)
also have "… = 8 * M / r + Re (∑z∈Γ. 1 / (z - s))"
unfolding Δ_def by (subst sum.reindex) (unfold inj_on_def, auto)
finally show ?thesis
unfolding g_def comp_def using zl(1)
by (subst (asm) logderiv_shift)
(auto intro: analytic_on_imp_differentiable_at [OF af])
qed
unbundle no_pnt_notation
end