Theory Meromorphic_Upper_Half_Plane
section ‹The type of meromorphic functions in the upper half plane›
theory Meromorphic_Upper_Half_Plane
imports
"HOL-Complex_Analysis.Complex_Analysis"
"HOL-Library.Going_To_Filter"
"Polynomial_Interpolation.Ring_Hom"
"Elliptic_Functions.Modular_Fundamental_Region"
Modular_Forms_Library
begin
definition is_mero_uhp :: "(complex ⇒ complex) ⇒ bool" where
"is_mero_uhp f ⟷
f nicely_meromorphic_on {z. Im z > 0} ∧
(∀z. Im z ≤ 0 ∨ is_pole f z ⟶ f z = 0)"
typedef mero_uhp =
"{f :: complex ⇒ complex. is_mero_uhp f}"
morphisms eval_mero_uhp Abs_mero_uhp
by (rule exI[of _ "λ_. 0"])
(auto intro: meromorphic_intros simp: is_mero_uhp_def nicely_meromorphic_on_def)
setup_lifting type_definition_mero_uhp
lemma nicely_meromorphic_on_cong:
assumes "⋀z. z ∈ A ⟹ f z = g z" "open A"
assumes "A = B"
shows "f nicely_meromorphic_on A ⟷ g nicely_meromorphic_on B"
proof -
have *: "eventually (λz. f z = g z) (at z)"
if f: "f meromorphic_on A" and z: "z ∈ A"
and fg: "⋀z. z ∈ A ⟹ ¬is_pole f z ⟹ f z = g z" for z f g
proof -
have "eventually (λz. ¬is_pole f z) (at z)"
using f z by (metis eventually_not_pole meromorphic_onE)
moreover have "eventually (λz. z ∈ A) (at z)"
by (intro eventually_at_in_open' assms z)
ultimately show "eventually (λz. f z = g z) (at z)"
by eventually_elim (use fg in auto)
qed
show ?thesis
proof
assume "f nicely_meromorphic_on A"
hence mero: "f meromorphic_on A"
by (auto simp: nicely_meromorphic_on_def)
have ev: "eventually (λz. f z = g z) (at z)" if "z ∈ A" for z
by (rule *[OF mero that]) (use assms in auto)
show "g nicely_meromorphic_on B"
unfolding nicely_meromorphic_on_def assms(3) [symmetric]
proof (intro ballI conjI impI)
have "f meromorphic_on A ⟷ g meromorphic_on A"
by (intro meromorphic_on_cong ev refl)
with mero show "g meromorphic_on A"
by auto
next
fix z assume z: "z ∈ A"
have pole_iff: "is_pole f z ⟷ is_pole g z"
using ev z by (intro is_pole_cong refl) auto
show "is_pole g z ∧ g z = 0 ∨ g ─z→ g z"
proof (cases "is_pole g z")
case False
with pole_iff have "f ─z→ g z"
using ‹f nicely_meromorphic_on A› z assms by (auto simp: nicely_meromorphic_on_def)
also have "?this ⟷ g ─z→ g z"
by (intro tendsto_cong ev z)
finally show ?thesis
by blast
next
case True
hence "is_pole f z"
by (simp add: pole_iff)
hence "f z = 0"
using ‹f nicely_meromorphic_on A›
by (metis nicely_meromorphic_on_def remove_sings_at_pole remove_sings_eqI z)
thus ?thesis using True assms z by auto
qed
qed
next
assume "g nicely_meromorphic_on B"
hence mero: "g meromorphic_on A"
by (auto simp: nicely_meromorphic_on_def ‹A = B›)
have ev: "eventually (λz. g z = f z) (at z)" if "z ∈ A" for z
by (rule *[OF mero that]) (use assms in ‹auto simp: eq_commute›)
show "f nicely_meromorphic_on A"
unfolding nicely_meromorphic_on_def assms(3) [symmetric]
proof (intro ballI conjI impI)
have "g meromorphic_on A ⟷ f meromorphic_on A"
by (intro meromorphic_on_cong ev refl)
with mero show "f meromorphic_on A"
by auto
next
fix z assume z: "z ∈ A"
have pole_iff: "is_pole f z ⟷ is_pole g z"
using ev z by (intro is_pole_cong refl) (auto simp: eq_commute)
show "is_pole f z ∧ f z = 0 ∨ f ─z→ f z"
proof (cases "is_pole f z")
case False
with pole_iff have "g ─z→ f z"
using ‹g nicely_meromorphic_on B› z assms by (auto simp: nicely_meromorphic_on_def)
also have "?this ⟷ f ─z→ f z"
by (intro ev tendsto_cong z)
finally show ?thesis
by blast
next
case True
hence "is_pole g z"
by (simp add: pole_iff)
hence "g z = 0"
using ‹g nicely_meromorphic_on B›
by (metis remove_sings_at_pole remove_sings_eqI
assms(3) nicely_meromorphic_on_def z)
thus ?thesis using True assms z by auto
qed
qed
qed
qed
lift_definition mero_uhp :: "(complex ⇒ complex) ⇒ mero_uhp" is
"λf. if f meromorphic_on {z. Im z > 0}
then (λz. if Im z > 0 ∧ ¬is_pole f z then remove_sings f z else 0)
else (λ_. 0)"
proof goal_cases
case (1 f)
show ?case
proof (cases "f meromorphic_on {z. Im z > 0}")
case False
thus ?thesis
by (auto simp: is_mero_uhp_def nicely_meromorphic_on_def intro!: meromorphic_intros)
next
case True
have *: "is_pole (λz. if 0 < Im z ∧ ¬ is_pole f z then remove_sings f z else 0) z ⟷
is_pole f z" if z: "Im z > 0" for z
proof -
have "eventually (λz. z ∈ {z. Im z > 0}) (at z)"
using z by (intro eventually_at_in_open') (auto intro!: open_halfspace_Im_gt)
moreover have "eventually (λz. remove_sings f z = f z) (at z)" using z
using eventually_remove_sings_eq_at meromorphic_on_isolated_singularity True
meromorphic_on_subset by auto
moreover have "eventually (λz. ¬is_pole f z) (at z)"
by (metis True eventually_not_pole mem_Collect_eq meromorphic_onE z)
ultimately have "eventually (λz. (if 0 < Im z ∧ ¬ is_pole f z then remove_sings f z else 0) = f z) (at z)"
by eventually_elim auto
thus ?thesis
by (intro is_pole_cong) auto
qed
have "remove_sings f nicely_meromorphic_on {z. 0 < Im z}"
by (intro remove_sings_nicely_meromorphic True)
also have "?this ⟷ (λz. if Im z > 0 ∧ ¬is_pole f z then remove_sings f z else 0)
nicely_meromorphic_on {z. 0 < Im z}"
by (intro nicely_meromorphic_on_cong) (auto simp: open_halfspace_Im_gt)
finally show ?thesis unfolding is_mero_uhp_def using True
by (auto simp: *)
qed
qed
lemma mero_uhp_cong_weak: "(⋀z. Im z > 0 ⟹ f z = g z) ⟹ mero_uhp f = mero_uhp g"
by (transfer, intro if_cong meromorphic_on_cong ext refl conj_cong arg_cong[of _ _ Not]
is_pole_cong remove_sings_cong
eventually_mono[OF eventually_at_in_open[OF open_halfspace_Im_gt[of 0]]]) auto
lemma eval_mero_uhp_outside: "Im z ≤ 0 ⟹ eval_mero_uhp f z = 0"
by transfer (auto simp: is_mero_uhp_def)
lemma eval_mero_uhp_pole: "is_pole (eval_mero_uhp f) z ⟹ eval_mero_uhp f z = 0"
by transfer (auto simp: is_mero_uhp_def)
lemma eval_mero_uhp_mero_uhp_eq:
assumes "f meromorphic_on {z. Im z > 0}" "Im z > 0"
shows "eval_mero_uhp (mero_uhp f) z = remove_sings f z"
using assms by transfer auto
lemma eval_mero_uhp_mero_uhp:
assumes "f meromorphic_on {z. Im z > 0}" "f analytic_on {z}" "Im z > 0"
shows "eval_mero_uhp (mero_uhp f) z = f z"
using assms by transfer (auto dest: analytic_at_imp_no_pole)
lemma eval_mero_uhp_meromorphic:
"eval_mero_uhp f meromorphic_on {z. Im z > 0}"
by transfer (auto simp: is_mero_uhp_def nicely_meromorphic_on_def intro: meromorphic_on_subset)
lemma eval_mero_uhp_meromorphic':
"A ⊆ {z. Im z > 0} ⟹ eval_mero_uhp f meromorphic_on A"
by transfer (auto simp: is_mero_uhp_def nicely_meromorphic_on_def intro: meromorphic_on_subset)
lemma eventually_eval_mero_uhp_mero_uhp_eq:
assumes "f meromorphic_on {z. Im z > 0}" "Im z > 0"
shows "eventually (λw. eval_mero_uhp (mero_uhp f) w = f w) (at z)"
proof -
have "isolated_singularity_at f z"
using assms meromorphic_on_isolated_singularity meromorphic_on_subset by blast
hence "eventually (λw. f analytic_on {w}) (at z)"
by (simp add: isolated_singularity_at_altdef)
moreover have "eventually (λw. w ∈ {w. Im w > 0}) (at z)"
using assms(2) by (intro eventually_at_in_open' open_halfspace_Im_gt) auto
ultimately show ?thesis
by eventually_elim (rule eval_mero_uhp_mero_uhp, use assms in auto)
qed
lemma is_pole_eval_mero_uhp_mero_uhp_iff:
assumes "f meromorphic_on {z. Im z > 0}" "Im z > 0"
shows "is_pole (eval_mero_uhp (mero_uhp f)) z ⟷ is_pole f z"
by (intro is_pole_cong eventually_eval_mero_uhp_mero_uhp_eq assms refl)
lemma eval_mero_uhp_nicely_meromorphic:
"A ⊆ {z. Im z > 0} ⟹ eval_mero_uhp f nicely_meromorphic_on A"
by transfer (auto simp: is_mero_uhp_def nicely_meromorphic_on_def intro: meromorphic_on_subset)
lemma eval_mero_uhp_analytic:
assumes "¬is_pole (eval_mero_uhp f) z" "Im z > 0"
shows "eval_mero_uhp f analytic_on {z}"
proof -
have "eval_mero_uhp f nicely_meromorphic_on {z}"
by (rule eval_mero_uhp_nicely_meromorphic) (use assms(2) in auto)
thus ?thesis
using assms nicely_meromorphic_on_imp_analytic_at by blast
qed
lemma not_is_pole_eval_mero_uhp_outside:
assumes "Im z ≤ 0"
shows "¬is_pole (eval_mero_uhp f) z"
proof
assume "is_pole (eval_mero_uhp f) z"
moreover have "LIM x at_right 0. z - complex_of_real x * 𝗂 :> at z"
proof (rule filterlim_atI)
show "((λx. z - complex_of_real x * 𝗂) ⤏ z) (at_right 0)"
by (auto intro!: tendsto_eq_intros)
next
have "eventually (λx::real. x ≠ 0) (at_right 0)"
by (intro eventually_neq_at_within)
thus "∀⇩F x in at_right 0. z - complex_of_real x * 𝗂 ≠ z"
by eventually_elim auto
qed
ultimately have "filterlim (eval_mero_uhp f ∘ (λx. z - of_real x * 𝗂)) at_infinity (at_right 0)"
unfolding is_pole_def o_def by (rule filterlim_compose)
moreover {
have "eventually (λx::real. x > 0) (at_right 0)"
by (auto simp: eventually_at_topological)
hence "eventually (λx. (eval_mero_uhp f ∘ (λx. z - of_real x * 𝗂)) x = 0) (at_right 0)"
by eventually_elim (use assms in ‹auto simp: eval_mero_uhp_outside›)
hence "((eval_mero_uhp f ∘ (λx. z - of_real x * 𝗂)) ⤏ 0) (at_right 0)"
using tendsto_eventually by blast
}
moreover have "at_right (0 :: real) ≠ bot"
by simp
ultimately show False
using not_tendsto_and_filterlim_at_infinity by blast
qed
lemma meromorphic_on_eval_mero_uhp' [meromorphic_intros]:
assumes "g analytic_on A" "⋀z. z ∈ A ⟹ Im (g z) > 0"
shows "(λw. eval_mero_uhp f (g w)) meromorphic_on A"
by (rule meromorphic_on_compose[OF eval_mero_uhp_meromorphic'[OF order.refl] assms(1)])
(use assms(2) in auto)
lemma analytic_on_eval_mero_uhp [analytic_intros]:
"(⋀z. z ∈ A ⟹ Im z > 0) ⟹ (⋀z. z ∈ A ⟹ ¬is_pole (eval_mero_uhp f) z) ⟹
eval_mero_uhp f analytic_on A"
using eval_mero_uhp_analytic analytic_on_analytic_at by blast
lemma holomorphic_on_eval_mero_uhp [holomorphic_intros]:
"(⋀z. z ∈ A ⟹ Im z > 0) ⟹ (⋀z. z ∈ A ⟹ ¬is_pole (eval_mero_uhp f) z) ⟹
eval_mero_uhp f holomorphic_on A"
by (intro analytic_imp_holomorphic analytic_intros)
lemma analytic_on_eval_mero_uhp' [analytic_intros]:
assumes "g analytic_on A" "⋀z. z ∈ A ⟹ Im (g z) > 0 ∧ ¬is_pole (eval_mero_uhp f) (g z)"
shows "(λw. eval_mero_uhp f (g w)) analytic_on A"
by (rule analytic_on_compose[OF assms(1) analytic_on_eval_mero_uhp, unfolded o_def])
(use assms(2) in auto)
lemma holomorphic_on_eval_mero_uhp' [holomorphic_intros]:
assumes "g holomorphic_on A" "⋀z. z ∈ A ⟹ Im (g z) > 0 ∧ ¬is_pole (eval_mero_uhp f) (g z)"
shows "(λw. eval_mero_uhp f (g w)) holomorphic_on A"
by (rule holomorphic_on_compose[OF assms(1) holomorphic_on_eval_mero_uhp, unfolded o_def])
(use assms(2) in auto)
definition const_mero_uhp :: "complex ⇒ mero_uhp" where
"const_mero_uhp c = mero_uhp (λ_. c)"
lemma eval_const_mero_uhp [simp]: "Im z > 0 ⟹ eval_mero_uhp (const_mero_uhp c) z = c"
unfolding const_mero_uhp_def
by (rule eval_mero_uhp_mero_uhp) auto
lemma not_pole_const_mero_uhp [simp]: "Im z > 0 ⟹ ¬is_pole (eval_mero_uhp (const_mero_uhp c)) z"
unfolding const_mero_uhp_def by (subst is_pole_eval_mero_uhp_mero_uhp_iff) auto
declare [[coercion eval_mero_uhp]]
lemma not_essential_frequently_0_imp_eventually_0':
fixes f :: "complex ⇒ complex"
assumes sing: "isolated_singularity_at f z" "not_essential f z"
assumes freq: "frequently (λz. f z = 0) (at z within A)"
shows "eventually (λz. f z = 0) (at z within B)"
proof -
from freq have "frequently (λz. f z = 0) (at z)"
unfolding frequently_def by (auto simp: eventually_at_topological)
from not_essential_frequently_0_imp_eventually_0[OF sing this] show ?thesis
by (metis UNIV_I eventually_at_topological)
qed
lemma frequently_eq_at_imp_eq_at:
assumes "frequently (λz. f z = g z) (at z within A)"
assumes "f analytic_on {z}" "g analytic_on {z}"
shows "f z = g z"
proof -
have "(λz. f z - g z) analytic_on {z}"
by (intro analytic_intros assms)
hence "isolated_singularity_at (λz. f z - g z) z" "not_essential (λz. f z - g z) z"
using isolated_singularity_at_analytic not_essential_analytic by blast+
moreover have "∃⇩F z in at z within A. f z - g z = 0"
using assms(1) by simp
ultimately have ev: "eventually (λz. f z - g z = 0) (at z)"
by (rule not_essential_frequently_0_imp_eventually_0')
have "filterlim (λz. f z - g z) (nhds (f z - g z)) (at z)"
by (intro isContD analytic_at_imp_isCont assms analytic_intros)
also have "?this ⟷ filterlim (λz. 0) (nhds (f z - g z)) (at z)"
by (intro tendsto_cong eventually_mono[OF ev]) auto
finally have lim1: "((λz. 0) ⤏ f z - g z) (at z)"
by simp
moreover have lim2: "((λz. 0) ⤏ 0) (at z)"
by simp
show ?thesis
using tendsto_unique[OF _ lim1 lim2] by (auto simp: trivial_limit_within)
qed
lemma mero_uhp_eqI_strong:
fixes f g :: mero_uhp
assumes "frequently (λz. eval_mero_uhp f z = eval_mero_uhp g z) (cosparse {z. Im z > 0})"
shows "f = g"
proof -
let ?f = "eval_mero_uhp f" and ?g = "eval_mero_uhp g"
let ?h = "λz. ?f z - ?g z"
have "(∀⇩≈z | Im z > 0. ?h z = 0) ∨ (∀⇩≈z | Im z > 0. ?h z ≠ 0)"
proof (rule meromorphic_imp_constant_or_avoid)
show "?h meromorphic_on {z. Im z > 0}"
by (intro meromorphic_intros) auto
qed (auto intro: open_halfspace_Im_gt connected_halfspace_Im_gt)
with assms have ev: "∀⇩≈z | Im z > 0. ?h z = 0"
by (auto simp: frequently_def)
have pole_iff: "is_pole ?f z ⟷ is_pole ?g z" if "Im z > 0" for z
using that ev
by (intro is_pole_cong) (auto simp: eventually_cosparse_open_eq open_halfspace_Im_gt)
have "?f z = ?g z" for z
proof -
consider "Im z ≤ 0" | "Im z > 0" "is_pole ?f z" | "Im z > 0" "¬is_pole ?f z"
by linarith
thus ?thesis
proof cases
assume "Im z > 0" "is_pole ?f z"
thus "?f z = ?g z"
using pole_iff[of z] by (simp add: eval_mero_uhp_pole)
next
assume "Im z > 0" "¬is_pole ?f z"
hence ana: "?f analytic_on {z}" "?g analytic_on {z}"
using eval_mero_uhp_analytic pole_iff by blast+
have "∃⇩F z in at z. eval_mero_uhp f z = eval_mero_uhp g z"
by (intro eventually_frequently)
(use ev ‹Im z > 0› in ‹auto simp: eventually_cosparse_open_eq open_halfspace_Im_gt›)
from this and ana show "?f z = ?g z"
by (rule frequently_eq_at_imp_eq_at)
qed (auto simp: eval_mero_uhp_outside)
qed
hence "eval_mero_uhp f = eval_mero_uhp g"
by blast
thus "f = g"
using eval_mero_uhp_inject by blast
qed
lemma mero_uhp_eqI_strong':
fixes f g :: mero_uhp
assumes "frequently (λz. eval_mero_uhp f z = eval_mero_uhp g z) (at z0)" "Im z0 > 0"
shows "f = g"
proof (rule mero_uhp_eqI_strong)
show "∃⇩F z in cosparse {z. 0 < Im z}. eval_mero_uhp f z = eval_mero_uhp g z"
using assms unfolding frequently_def
by (subst eventually_cosparse_open_eq) (auto simp: open_halfspace_Im_gt)
qed
lemma mero_uhp_eqI:
fixes f g :: mero_uhp
assumes "eventually (λz. eval_mero_uhp f z = eval_mero_uhp g z) (cosparse {z. Im z > 0})"
shows "f = g"
by (intro mero_uhp_eqI_strong eventually_frequently assms) (auto intro: exI[of _ 𝗂])
lemma mero_uhp_eqI_weak:
fixes f g :: mero_uhp
assumes "⋀z. Im z > 0 ⟹ eval_mero_uhp f z = eval_mero_uhp g z"
shows "f = g"
proof -
have "eval_mero_uhp f = eval_mero_uhp g"
proof
fix z show "eval_mero_uhp f z = eval_mero_uhp g z"
by (cases "Im z > 0") (use assms in ‹auto simp: eval_mero_uhp_outside›)
qed
thus ?thesis
by (simp only: eval_mero_uhp_inject)
qed
lemma frequently_eval_mero_uhp_eq_imp_const:
assumes "frequently (λw. eval_mero_uhp f w = c) (at z)" "Im z > 0"
shows "f = const_mero_uhp c"
proof (rule mero_uhp_eqI_strong')
have ev: "eventually (λz. z ∈ {z. Im z > 0}) (at z)"
by (intro eventually_at_in_open' open_halfspace_Im_gt) (use assms(2) in auto)
show "∃⇩F z in at z. eval_mero_uhp f z = eval_mero_uhp (const_mero_uhp c) z"
by (rule frequently_elim1[OF frequently_eventually_frequently[OF assms(1) ev]]) auto
qed fact+
lemma eventually_neq_eval_mero_uhp:
assumes "f ≠ const_mero_uhp c" "Im z > 0"
shows "eventually (λz. eval_mero_uhp f z ≠ c) (at z)"
using frequently_eval_mero_uhp_eq_imp_const[of f c z] assms by (auto simp: frequently_def)
definition mero_uhp_rel where
"mero_uhp_rel f g ⟷ eventually (λz. f z = g z) (cosparse {z. Im z > 0})"
named_theorems mero_uhp_rel_intros
lemma mero_uhp_rel_refl [simp, intro]: "mero_uhp_rel f f"
by (simp add: mero_uhp_rel_def)
lemma mero_uhp_rel_sym: "mero_uhp_rel f g ⟹ mero_uhp_rel g f"
by (simp add: mero_uhp_rel_def eq_commute)
lemma mero_uhp_rel_sym_eq: "mero_uhp_rel f g ⟷ mero_uhp_rel g f"
by (simp add: mero_uhp_rel_def eq_commute)
lemma mero_uhp_rel_trans [trans]: "mero_uhp_rel f g ⟹ mero_uhp_rel g h ⟹ mero_uhp_rel f h"
unfolding mero_uhp_rel_def by (erule (1) eventually_elim2) simp_all
lemma mero_uhp_relI_weak:
assumes "⋀z. Im z > 0 ⟹ f z = g z"
shows "mero_uhp_rel f g"
proof -
have "eventually (λz. z ∈ {z. Im z > 0}) (cosparse {z. Im z > 0})"
by (intro eventually_in_cosparse open_halfspace_Im_gt order.refl)
thus ?thesis
unfolding mero_uhp_rel_def by eventually_elim (use assms in auto)
qed
lemma mero_uhp_rel_mero_uhp [mero_uhp_rel_intros]:
assumes "f meromorphic_on {z. Im z > 0}"
shows "mero_uhp_rel (eval_mero_uhp (mero_uhp f)) f"
unfolding mero_uhp_rel_def
by (subst eventually_cosparse_open_eq[OF open_halfspace_Im_gt])
(use eventually_eval_mero_uhp_mero_uhp_eq assms in blast)
lemma mero_uhp_rel_imp_eq_mero_uhp:
"mero_uhp_rel (eval_mero_uhp f) (eval_mero_uhp g) ⟹ f = g"
unfolding mero_uhp_rel_def by (rule mero_uhp_eqI)
definition deriv_mero_uhp :: "mero_uhp ⇒ mero_uhp" where
"deriv_mero_uhp f = mero_uhp (deriv f)"
lemma mero_uhp_rel_unop:
assumes "mero_uhp_rel f f'"
shows "mero_uhp_rel (λz. h (f z)) (λz. h (f' z))"
using assms unfolding mero_uhp_rel_def by eventually_elim auto
lemma mero_uhp_rel_binop:
assumes "mero_uhp_rel f f'" "mero_uhp_rel g g'"
shows "mero_uhp_rel (λz. h (f z) (g z)) (λz. h (f' z) (g' z))"
using assms unfolding mero_uhp_rel_def by eventually_elim auto
named_theorems mero_uhp_rel_cong
lemmas mero_uhp_rel_cong_uminus [mero_uhp_rel_cong] = mero_uhp_rel_unop[where h = "λx. -x"]
lemmas mero_uhp_rel_cong_inverse [mero_uhp_rel_cong] = mero_uhp_rel_unop[where h = "inverse"]
lemmas mero_uhp_rel_cong_add [mero_uhp_rel_cong] = mero_uhp_rel_binop[where h = "(+)"]
lemmas mero_uhp_rel_cong_diff [mero_uhp_rel_cong] = mero_uhp_rel_binop[where h = "(-)"]
lemmas mero_uhp_rel_cong_mult [mero_uhp_rel_cong] = mero_uhp_rel_binop[where h = "(*)"]
lemmas mero_uhp_rel_cong_divide [mero_uhp_rel_cong] = mero_uhp_rel_binop[where h = "(/)"]
lemmas mero_uhp_rel_cong_power [mero_uhp_rel_cong] = mero_uhp_rel_unop[where h = "λz. z ^ n" for n]
lemmas mero_uhp_rel_cong_powi [mero_uhp_rel_cong] = mero_uhp_rel_unop[where h = "λz. z powi n" for n]
lemma mero_uhp_rel_cong_sum [mero_uhp_rel_cong]:
"(⋀x. x ∈ A ⟹ mero_uhp_rel (f x) (f' x)) ⟹
mero_uhp_rel (λz. sum (λx. f x z) A) (λz. sum (λx. f' x z) A)"
by (induction A rule: infinite_finite_induct) (auto intro!: mero_uhp_rel_cong)
lemma mero_uhp_rel_cong_prod [mero_uhp_rel_cong]:
"(⋀x. x ∈ A ⟹ mero_uhp_rel (f x) (f' x)) ⟹
mero_uhp_rel (λz. prod (λx. f x z) A) (λz. prod (λx. f' x z) A)"
by (induction A rule: infinite_finite_induct) (auto intro!: mero_uhp_rel_cong)
lemma sparse_in_union':
assumes "pts1 sparse_in D" "pts2 sparse_in D"
shows "(pts1 ∪ pts2) sparse_in D"
using sparse_in_union[OF assms, of D] by simp
lemma mero_uhp_rel_cong_deriv [mero_uhp_rel_cong]:
assumes "mero_uhp_rel f g"
shows "mero_uhp_rel (deriv f) (deriv g)"
proof -
define pts where "pts = {z. f z ≠ g z}"
have "pts sparse_in {z. Im z > 0}"
using assms unfolding pts_def by (auto simp: mero_uhp_rel_def eventually_cosparse)
hence ev: "eventually (λz. z ∉ pts) (cosparse {z. Im z > 0})"
by (simp add: eventually_cosparse)
have "eventually (λz. z ∈ {z. Im z > 0}) (cosparse {z. Im z > 0})"
by (metis dual_order.refl eventually_in_cosparse open_halfspace_Im_gt)
hence "eventually (λz. deriv f z = deriv g z) (cosparse {z. Im z > 0})"
using ev
proof eventually_elim
case z: (elim z)
have "eventually (λz. z ∉ pts) (at z)"
using ev z by (subst (asm) eventually_cosparse_open_eq[OF open_halfspace_Im_gt]) auto
with z(2) have "eventually (λz. z ∉ pts) (nhds z)"
using eventually_nhds_conv_at by blast
hence "eventually (λz. f z = g z) (nhds z)"
by eventually_elim (auto simp: pts_def)
thus "deriv f z = deriv g z"
by (intro deriv_cong_ev refl)
qed
thus ?thesis
by (simp add: mero_uhp_rel_def)
qed
lemma mero_uhp_rel_cong_higher_deriv [mero_uhp_rel_cong]:
"mero_uhp_rel f g ⟹ mero_uhp_rel ((deriv ^^ n) f) ((deriv ^^ n) g)"
by (induction n) (auto intro: mero_uhp_rel_cong_deriv)
lemma mero_uhp_rel_simpI: "mero_uhp_rel f h ⟹ mero_uhp_rel g h' ⟹ h = h' ⟹ mero_uhp_rel f g"
using mero_uhp_rel_sym mero_uhp_rel_trans by blast
lemma mero_uhp_rel_eval_mero_uhp_const [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (const_mero_uhp c)) (λ_. c)"
unfolding const_mero_uhp_def by (intro mero_uhp_rel_intros) auto
lemma eval_deriv_mero_uhp:
assumes "Im z > 0" "¬is_pole (eval_mero_uhp f) z"
shows "eval_mero_uhp (deriv_mero_uhp f) z = deriv (eval_mero_uhp f) z"
unfolding deriv_mero_uhp_def
by (rule eval_mero_uhp_mero_uhp) (use assms in ‹auto intro!: meromorphic_intros analytic_intros›)
lemma is_pole_deriv_mero_uhp_iff:
assumes "Im z > 0"
shows "is_pole (eval_mero_uhp (deriv_mero_uhp f)) z ⟷ is_pole (eval_mero_uhp f) z"
proof -
have "is_pole (eval_mero_uhp (deriv_mero_uhp f)) z ⟷ is_pole (deriv (eval_mero_uhp f)) z"
unfolding deriv_mero_uhp_def
using assms by (intro is_pole_eval_mero_uhp_mero_uhp_iff meromorphic_intros) auto
also have "… ⟷ is_pole (eval_mero_uhp f) z"
by (intro is_pole_deriv_iff meromorphic_on_isolated_singularity meromorphic_on_not_essential
meromorphic_intros) (use assms in auto)
finally show ?thesis .
qed
lemma mero_uhp_rel_imp_eval_mero_uhp_eq:
assumes "mero_uhp_rel (eval_mero_uhp f) g"
assumes "g analytic_on {z}" "Im z > 0"
shows "eval_mero_uhp f z = g z"
proof -
from assms have ev: "eventually (λz. f z = g z) (at z)"
by (auto simp: mero_uhp_rel_def eventually_cosparse_open_eq open_halfspace_Im_gt)
with assms have "f analytic_on {z}"
using analytic_at_imp_no_pole eval_mero_uhp_analytic is_pole_cong by blast
hence "f ─z→ f z"
by (intro isContD analytic_at_imp_isCont)
also have "?this ⟷ g ─z→ f z"
by (intro tendsto_cong ev)
finally have "g ─z→ f z" .
moreover from assms(2) have "g ─z→ g z"
by (intro isContD analytic_at_imp_isCont)
ultimately show ?thesis
using LIM_unique by blast
qed
lemma mero_uhp_rel_const_refl: "mero_uhp_rel (λ_. c) (λ_. c)"
by (rule mero_uhp_rel_refl)
method_setup mero_uhp_rel = ‹
let
fun tac ctxt simp =
let
fun rtac ctxt thms = DETERM o resolve_tac ctxt thms
val raw_intros =
Named_Theorems.get ctxt @{named_theorems mero_uhp_rel_intros}
val extra_intros =
maps (Named_Theorems.get ctxt)
[@{named_theorems mero_uhp_rel_cong},
@{named_theorems meromorphic_intros},
@{named_theorems analytic_intros}] @ @{thms eval_mero_uhp_meromorphic}
val intros = map (fn thm => thm RS @{thm mero_uhp_rel_trans}) raw_intros
val intros = intros @ extra_intros
val tac' =
TRY o REPEAT_ALL_NEW (rtac ctxt (@{thm mero_uhp_rel_const_refl} :: intros))
THEN_ALL_NEW TRY o rtac ctxt @{thms mero_uhp_rel_refl}
in SELECT_GOAL (
HEADGOAL (rtac ctxt @{thms mero_uhp_rel_imp_eq_mero_uhp[OF mero_uhp_rel_simpI] mero_uhp_rel_simpI})
THEN HEADGOAL (RANGE [tac', tac', if simp then simp_tac ctxt THEN_ALL_NEW K no_tac else K all_tac])
)
end
val parser = Scan.optional (Args.parens (Args.$$$ "nosimp" >> K false)) true
in
Scan.lift parser >> (fn simp => fn ctxt => SIMPLE_METHOD' (tac ctxt simp))
end
›
lemma mero_uhp_eval_mero_uhp [simp]: "mero_uhp (eval_mero_uhp f) = f"
by mero_uhp_rel auto
lemma mero_uhp_rel_deriv [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (deriv_mero_uhp f)) (deriv (eval_mero_uhp f))"
unfolding deriv_mero_uhp_def by mero_uhp_rel auto
lemma mero_uhp_rel_higher_deriv [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp ((deriv_mero_uhp ^^ n) f)) ((deriv ^^ n) (eval_mero_uhp f))"
proof (induction n)
case [mero_uhp_rel_intros]: (Suc n)
show ?case
unfolding funpow.simps o_def by mero_uhp_rel
qed auto
lemma has_field_derivative_deriv_mero_uhp [derivative_intros]:
assumes "Im z > 0" "¬is_pole (eval_mero_uhp f) z"
shows "(eval_mero_uhp f has_field_derivative eval_mero_uhp (deriv_mero_uhp f) z) (at z)"
proof -
have "eval_mero_uhp f analytic_on {z}"
using assms eval_mero_uhp_analytic by blast
hence "(eval_mero_uhp f has_field_derivative deriv (eval_mero_uhp f) z) (at z)"
using analytic_at_two holomorphic_derivI by blast
also have "deriv (eval_mero_uhp f) z = deriv_mero_uhp f z"
unfolding deriv_mero_uhp_def using assms
by (subst eval_mero_uhp_mero_uhp) (auto intro!: meromorphic_intros analytic_intros)
finally show ?thesis .
qed
lemma has_field_derivative_deriv_mero_uhp' [derivative_intros]:
assumes "(g has_field_derivative g') (at z within A)"
assumes "Im (g z) > 0" "¬is_pole (eval_mero_uhp f) (g z)"
shows "((λz. eval_mero_uhp f (g z)) has_field_derivative
eval_mero_uhp (deriv_mero_uhp f) (g z) * g') (at z within A)"
using DERIV_chain[OF has_field_derivative_deriv_mero_uhp[of _ f] assms(1)] assms(2,3)
by (auto simp: o_def)
instantiation mero_uhp :: comm_ring_1
begin
definition zero_mero_uhp where "zero_mero_uhp = const_mero_uhp 0"
definition one_mero_uhp where "one_mero_uhp = const_mero_uhp 1"
definition plus_mero_uhp :: "mero_uhp ⇒ mero_uhp ⇒ mero_uhp" where
"f + g = mero_uhp (λz. eval_mero_uhp f z + eval_mero_uhp g z)"
definition uminus_mero_uhp :: "mero_uhp ⇒ mero_uhp" where
"-f = mero_uhp (λz. -eval_mero_uhp f z)"
definition minus_mero_uhp :: "mero_uhp ⇒ mero_uhp ⇒ mero_uhp" where
"f - g = mero_uhp (λz. eval_mero_uhp f z - eval_mero_uhp g z)"
definition times_mero_uhp :: "mero_uhp ⇒ mero_uhp ⇒ mero_uhp" where
"f * g = mero_uhp (λz. eval_mero_uhp f z * eval_mero_uhp g z)"
lemma mero_uhp_rel_eval_mero_uhp_0 [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp 0) (λ_. 0)"
and mero_uhp_rel_eval_mero_uhp_1 [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp 1) (λ_. 1)"
and mero_uhp_rel_eval_mero_uhp_minus [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (-f)) (λz. -eval_mero_uhp f z)"
and mero_uhp_rel_eval_mero_uhp_add [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (f + g)) (λz. eval_mero_uhp f z + eval_mero_uhp g z)"
and mero_uhp_rel_eval_mero_uhp_diff [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (f - g)) (λz. eval_mero_uhp f z - eval_mero_uhp g z)"
and mero_uhp_rel_eval_mero_uhp_times [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (f * g)) (λz. eval_mero_uhp f z * eval_mero_uhp g z)"
unfolding zero_mero_uhp_def one_mero_uhp_def uminus_mero_uhp_def
plus_mero_uhp_def minus_mero_uhp_def times_mero_uhp_def
by (mero_uhp_rel; simp; fail)+
lemma eval_mero_uhp_0 [simp]: "eval_mero_uhp 0 = (λ_. 0)"
proof
show "eval_mero_uhp 0 z = 0" for z
by (cases "Im z > 0") (auto simp: zero_mero_uhp_def eval_mero_uhp_outside)
qed
lemma eval_mero_uhp_1 [simp]: "Im z > 0 ⟹ eval_mero_uhp 1 z = 1"
unfolding one_mero_uhp_def by (cases "Im z > 0") (auto simp: eval_mero_uhp_outside)
lemma not_pole_0_mero_uhp [simp]: "Im z > 0 ⟹ ¬is_pole (eval_mero_uhp 0) z"
and not_pole_1_mero_uhp [simp]: "Im z > 0 ⟹ ¬is_pole (eval_mero_uhp 1) z"
unfolding zero_mero_uhp_def one_mero_uhp_def by auto
lemma
assumes "Im z > 0" "¬is_pole (eval_mero_uhp f) z" "¬is_pole (eval_mero_uhp g) z"
shows eval_mero_uhp_add [simp]: "eval_mero_uhp (f + g) z = eval_mero_uhp f z + eval_mero_uhp g z"
and eval_mero_uhp_diff [simp]: "eval_mero_uhp (f - g) z = eval_mero_uhp f z - eval_mero_uhp g z"
and eval_mero_uhp_mult [simp]: "eval_mero_uhp (f * g) z = eval_mero_uhp f z * eval_mero_uhp g z"
using assms
unfolding plus_mero_uhp_def minus_mero_uhp_def times_mero_uhp_def
by (subst eval_mero_uhp_mero_uhp; force intro!: meromorphic_intros analytic_intros)+
instance proof -
have "eval_mero_uhp 0 𝗂 = 0" "eval_mero_uhp 1 𝗂 ≠ 0"
by auto
hence "0 ≠ (1 :: mero_uhp)"
by force
show "OFCLASS(mero_uhp, comm_ring_1_class)"
by standard (fact | mero_uhp_rel (nosimp), simp add: algebra_simps)+
qed
end
lemma eval_mero_uhp_cmult [simp]:
"eval_mero_uhp (const_mero_uhp c * f) z = c * eval_mero_uhp f z"
proof (cases "c = 0")
case True
thus ?thesis by (simp flip: zero_mero_uhp_def)
next
case [simp]: False
have [simp]: "eval_mero_uhp (const_mero_uhp c * f) z = c * eval_mero_uhp f z"
if "¬is_pole f z" for z
proof (cases "Im z > 0")
case True
thus ?thesis
unfolding times_mero_uhp_def using that
by (subst eval_mero_uhp_mero_uhp; force intro!: meromorphic_intros analytic_intros)+
qed (auto simp: eval_mero_uhp_outside)
show ?thesis
proof (cases "Im z > 0")
case True
have ev: "eventually (λz. z ∈ {z. Im z > 0}) (at z)"
using True by (intro eventually_at_in_open' open_halfspace_Im_gt) auto
moreover have "eventually (λz. ¬is_pole f z) (at z)"
by (metis True eval_mero_uhp_meromorphic eventually_not_pole mem_Collect_eq meromorphic_onE)
ultimately have "eventually (λz. eval_mero_uhp (const_mero_uhp c * f) z = c * eval_mero_uhp f z) (at z)"
by eventually_elim auto
hence "is_pole (eval_mero_uhp (const_mero_uhp c * f)) z ⟷ is_pole (λz. c * f z) z"
by (intro is_pole_cong) auto
thus ?thesis
by (cases "is_pole f z") (auto simp: eval_mero_uhp_pole)
qed (auto simp: eval_mero_uhp_outside)
qed
lemma eval_mero_uhp_cmult' [simp]:
"eval_mero_uhp (f * const_mero_uhp c) z = eval_mero_uhp f z * c"
using eval_mero_uhp_cmult[of c f z] by (simp only: mult.commute)
lemma const_mero_uhp_eq_iff [simp]: "const_mero_uhp c = const_mero_uhp c' ⟷ c = c'"
proof
assume "const_mero_uhp c = const_mero_uhp c'"
hence "eval_mero_uhp (const_mero_uhp c) 𝗂 = eval_mero_uhp (const_mero_uhp c') 𝗂"
by (simp only: )
thus "c = c'"
by simp
qed auto
lemma const_mero_uhp_eq_0_iff [simp]: "const_mero_uhp c = 0 ⟷ c = 0"
unfolding zero_mero_uhp_def by simp
lemma const_mero_uhp_eq_1_iff [simp]: "const_mero_uhp c = 1 ⟷ c = 1"
unfolding one_mero_uhp_def by simp
interpretation const_mero_uhp: comm_ring_hom const_mero_uhp
by standard mero_uhp_rel+
lemma eval_mero_uhp_minus [simp]: "eval_mero_uhp (-f) z = -eval_mero_uhp f z"
using eval_mero_uhp_cmult[of "-1" f z] by (simp del: eval_mero_uhp_cmult add: hom_distribs)
lemma of_nat_mero_uhp: "of_nat n = const_mero_uhp (of_nat n)"
by (induction n) (simp_all add: const_mero_uhp.hom_add)
lemma of_int_mero_uhp: "of_int n = const_mero_uhp (of_int n)"
by (metis const_mero_uhp.hom_uminus int_cases2 of_int_minus of_int_of_nat_eq of_nat_mero_uhp)
lemma numeral_mero_uhp: "numeral n = const_mero_uhp (numeral n)"
by (subst of_nat_numeral [symmetric], subst of_nat_mero_uhp) simp
lemma mero_uhp_rel_of_nat [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (of_nat n)) (λ_. of_nat n)"
unfolding of_nat_mero_uhp by mero_uhp_rel
lemma mero_uhp_rel_of_int [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (of_int n)) (λ_. of_int n)"
unfolding of_int_mero_uhp by mero_uhp_rel
lemma mero_uhp_rel_numeral [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (numeral n)) (λ_. numeral n)"
unfolding numeral_mero_uhp by mero_uhp_rel
lemma mero_uhp_rel_sum [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (∑x∈A. f x)) (λz. ∑x∈A. eval_mero_uhp (f x) z)"
proof (induction A rule: infinite_finite_induct)
case (insert x A)
note [mero_uhp_rel_intros] = insert.IH
show ?case
using insert.hyps by simp mero_uhp_rel
qed (simp; mero_uhp_rel; fail)+
lemma mero_uhp_rel_prod [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (∏x∈A. f x)) (λz. ∏x∈A. eval_mero_uhp (f x) z)"
proof (induction A rule: infinite_finite_induct)
case (insert x A)
note [mero_uhp_rel_intros] = insert.IH
show ?case
using insert.hyps by simp mero_uhp_rel
qed (simp; mero_uhp_rel; fail)+
lemma mero_uhp_rel_power [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (f ^ n)) (λz. eval_mero_uhp f z ^ n)"
proof (induction n)
case 0
show ?case by simp mero_uhp_rel
next
case (Suc n)
have "mero_uhp_rel (eval_mero_uhp (f ^ Suc n)) (λz. eval_mero_uhp f z * eval_mero_uhp (f ^ n) z)"
unfolding power_Suc by mero_uhp_rel
also have "mero_uhp_rel … (λz. eval_mero_uhp f z ^ Suc n)"
unfolding power_Suc by (intro mero_uhp_rel_cong mero_uhp_rel_refl Suc)
finally show ?case .
qed
instantiation mero_uhp :: field_char_0
begin
definition inverse_mero_uhp :: "mero_uhp ⇒ mero_uhp" where
"inverse f = mero_uhp (λz. inverse (eval_mero_uhp f z))"
definition divide_mero_uhp :: "mero_uhp ⇒ mero_uhp ⇒ mero_uhp" where
"divide_mero_uhp f g = f * inverse g"
lemma mero_uhp_rel_eval_mero_uhp_inverse [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (inverse f)) (λz. inverse (eval_mero_uhp f z))"
unfolding inverse_mero_uhp_def by mero_uhp_rel auto
lemma mero_uhp_rel_eval_mero_uhp_divide [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (f div g)) (λz. eval_mero_uhp f z / eval_mero_uhp g z)"
unfolding divide_mero_uhp_def by (mero_uhp_rel (nosimp)) (simp add: field_simps)
lemma eval_mero_uhp_inverse [simp]:
assumes "Im z > 0"
shows "eval_mero_uhp (inverse f) z = inverse (eval_mero_uhp f z)"
proof (cases "is_pole (eval_mero_uhp f) z")
case True
hence [simp]: "eval_mero_uhp f z = 0"
using assms(1) eval_mero_uhp_pole by blast
have "filterlim (λw. inverse (eval_mero_uhp f w)) (at 0) (at z)"
unfolding filterlim_inverse_at_iff using True by (simp add: is_pole_def)
hence *: "(λw. inverse (eval_mero_uhp f w)) ─z→ 0"
using filterlim_at by blast
have "eval_mero_uhp (inverse f) z = remove_sings (λw. inverse (eval_mero_uhp f w)) z"
unfolding inverse_mero_uhp_def
by (intro eval_mero_uhp_mero_uhp_eq meromorphic_intros assms) auto
also have "… = 0"
using * by blast
finally show ?thesis
by simp
next
case no_pole: False
show ?thesis
proof (cases "eval_mero_uhp f z = 0")
case False
show ?thesis
using assms False no_pole
unfolding inverse_mero_uhp_def
by (subst eval_mero_uhp_mero_uhp) (force intro!: meromorphic_intros analytic_intros)+
next
case True
show ?thesis
proof (cases "f = 0")
case True
have "mero_uhp (λz. inverse (eval_mero_uhp 0 z)) = mero_uhp (λ_. 0)"
by (rule mero_uhp_cong_weak) auto
also have "… = 0"
by (simp add: zero_mero_uhp_def const_mero_uhp_def)
finally have "inverse f = 0" using True
unfolding inverse_mero_uhp_def by simp
thus ?thesis
using assms True by auto
next
case False
have "filterlim (eval_mero_uhp f) (at 0) (at z)"
proof (rule filterlim_atI)
have "eval_mero_uhp f analytic_on {z}"
using assms eval_mero_uhp_analytic no_pole by blast
have "eval_mero_uhp f ─z→ eval_mero_uhp f z"
by (rule isContD analytic_at_imp_isCont)+ fact
with True show "eval_mero_uhp f ─z→ 0"
by simp
next
show "∀⇩F x in at z. eval_mero_uhp f x ≠ 0"
using False assms(1) eventually_neq_eval_mero_uhp zero_mero_uhp_def by metis
qed
hence pole: "is_pole (λz. inverse (eval_mero_uhp f z)) z"
unfolding is_pole_def by (rule filterlim_compose[OF filterlim_inverse_at_infinity])
have "eval_mero_uhp (inverse f) z = remove_sings (λz. inverse (eval_mero_uhp f z)) z"
unfolding inverse_mero_uhp_def
by (rule eval_mero_uhp_mero_uhp_eq) (auto intro!: meromorphic_intros ‹Im z > 0›)
also have "… = 0"
using pole by (rule remove_sings_at_pole)
finally show ?thesis
by (simp add: True)
qed
qed
qed
instance proof
show "inverse (0 :: mero_uhp) = 0"
by (mero_uhp_rel (nosimp)) simp
show "inverse f * f = (1 :: mero_uhp)" if "f ≠ 0" for f
proof -
let ?f = "eval_mero_uhp f"
have "mero_uhp_rel (inverse f * f) (λz. inverse (?f z) * ?f z)"
by mero_uhp_rel
also have "eventually (λz. ?f z ≠ 0) (cosparse {z. Im z > 0})"
using ‹f ≠ 0› eventually_neq_eval_mero_uhp unfolding zero_mero_uhp_def
by (subst eventually_cosparse_open_eq[OF open_halfspace_Im_gt]) auto
hence "mero_uhp_rel (λz. inverse (?f z) * ?f z) (λ_. 1)"
unfolding mero_uhp_rel_def by eventually_elim auto
also have "mero_uhp_rel (λ_. 1) (eval_mero_uhp 1)"
by mero_uhp_rel
finally show ?thesis
by (rule mero_uhp_rel_imp_eq_mero_uhp)
qed
show "f div g = f * inverse g" for f g :: mero_uhp
by (simp add: divide_mero_uhp_def)
show "inj (of_nat :: nat ⇒ mero_uhp)"
by (rule injI) (simp add: of_nat_mero_uhp)
qed
end
lemma eval_mero_uhp_divide [simp]:
assumes "Im z > 0" "¬is_pole (eval_mero_uhp f) z" "¬isolated_zero (eval_mero_uhp g) z"
shows "eval_mero_uhp (f / g) z = eval_mero_uhp f z / eval_mero_uhp g z"
proof -
have "is_pole (eval_mero_uhp (inverse g)) z ⟷ is_pole (λz. inverse (eval_mero_uhp g z)) z"
proof (rule is_pole_cong)
have "eventually (λz. z ∈ {z. Im z > 0}) (at z)"
by (intro eventually_at_in_open') (use assms(1) in ‹auto simp: open_halfspace_Im_gt›)
thus "∀⇩F x in at z. eval_mero_uhp (inverse g) x = inverse (eval_mero_uhp g x)"
by eventually_elim auto
qed auto
with assms(3) have *: "¬is_pole (eval_mero_uhp (inverse g)) z"
by (simp add: is_pole_inverse_iff)
have "eval_mero_uhp (f / g) z = eval_mero_uhp (f * inverse g) z"
by (simp add: field_simps)
also have "… = eval_mero_uhp f z * eval_mero_uhp (inverse g) z"
by (subst eval_mero_uhp_mult) (use assms * in auto)
also have "… = eval_mero_uhp f z / eval_mero_uhp g z"
by (subst eval_mero_uhp_inverse) (use assms in ‹auto simp: field_simps›)
finally show ?thesis .
qed
interpretation const_mero_uhp: comm_ring_hom const_mero_uhp
by standard mero_uhp_rel+
interpretation const_mero_uhp: field_char_0_hom const_mero_uhp
by standard
lemma mero_uhp_rel_power_int [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (f powi n)) (λz. eval_mero_uhp f z powi n)"
by (cases "n ≥ 0") (simp_all add: power_int_def, mero_uhp_rel+)
instantiation mero_uhp :: real_field
begin
definition scaleR_mero_uhp :: "real ⇒ mero_uhp ⇒ mero_uhp"
where "scaleR_mero_uhp x f = const_mero_uhp x * f"
instance
by standard
(auto simp: algebra_simps scaleR_mero_uhp_def const_mero_uhp.hom_mult const_mero_uhp.hom_add)
end
lemma of_real_mero_uhp: "of_real x = const_mero_uhp (of_real x)"
by (simp add: of_real_def scaleR_mero_uhp_def)
lemma mero_uhp_rel_of_real [mero_uhp_rel_intros]:
"mero_uhp_rel (eval_mero_uhp (of_real x)) (λ_. of_real x)"
unfolding of_real_mero_uhp by mero_uhp_rel
lemma of_rat_mero_uhp: "of_rat x = const_mero_uhp (of_rat x)"
using of_real_mero_uhp[of "of_rat x"]
by (cases x) (auto simp: of_rat_rat)
text ‹
Pre-modular forms are a complex vector space:
›
interpretation mero_uhp: vector_space "λ(x::complex) y. const_mero_uhp x * y"