equal
deleted
inserted
replaced
3 text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close> |
3 text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close> |
4 |
4 |
5 theory Complex_Transcendental |
5 theory Complex_Transcendental |
6 imports |
6 imports |
7 Complex_Analysis_Basics |
7 Complex_Analysis_Basics |
8 Summation |
8 Summation_Tests |
9 begin |
9 begin |
10 |
10 |
11 (* TODO: Figure out what to do with Möbius transformations *) |
11 (* TODO: Figure out what to do with Möbius transformations *) |
12 definition "moebius a b c d = (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))" |
12 definition "moebius a b c d = (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))" |
13 |
13 |
1645 unfolding holomorphic_on_def field_differentiable_def |
1645 unfolding holomorphic_on_def field_differentiable_def |
1646 by (metis (full_types) DERIV_chain' has_field_derivative_powr_right) |
1646 by (metis (full_types) DERIV_chain' has_field_derivative_powr_right) |
1647 |
1647 |
1648 lemma norm_powr_real_powr: |
1648 lemma norm_powr_real_powr: |
1649 "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z" |
1649 "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z" |
1650 by (cases "w = 0") (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 |
1650 by (cases "w = 0") (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 |
1651 complex_is_Real_iff in_Reals_norm complex_eq_iff) |
1651 complex_is_Real_iff in_Reals_norm complex_eq_iff) |
1652 |
1652 |
1653 lemma tendsto_ln_complex [tendsto_intros]: |
1653 lemma tendsto_ln_complex [tendsto_intros]: |
1654 assumes "(f \<longlongrightarrow> a) F" "a \<notin> \<real>\<^sub>\<le>\<^sub>0" |
1654 assumes "(f \<longlongrightarrow> a) F" "a \<notin> \<real>\<^sub>\<le>\<^sub>0" |
1655 shows "((\<lambda>z. ln (f z :: complex)) \<longlongrightarrow> ln a) F" |
1655 shows "((\<lambda>z. ln (f z :: complex)) \<longlongrightarrow> ln a) F" |