equal
deleted
inserted
replaced
1382 |
1382 |
1383 declare has_field_derivative_rGamma_complex'[THEN DERIV_chain2, derivative_intros] |
1383 declare has_field_derivative_rGamma_complex'[THEN DERIV_chain2, derivative_intros] |
1384 |
1384 |
1385 |
1385 |
1386 lemma complex_differentiable_Polygamma: |
1386 lemma complex_differentiable_Polygamma: |
|
1387 fixes z::complex |
|
1388 shows |
1387 "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Polygamma n complex_differentiable (at z within A)" |
1389 "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Polygamma n complex_differentiable (at z within A)" |
1388 using has_field_derivative_Polygamma[of z n] unfolding complex_differentiable_def by auto |
1390 using has_field_derivative_Polygamma[of z n] unfolding complex_differentiable_def by auto |
1389 |
1391 |
1390 lemma holomorphic_on_Polygamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Polygamma n holomorphic_on A" |
1392 lemma holomorphic_on_Polygamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Polygamma n holomorphic_on A" |
1391 unfolding holomorphic_on_def by (auto intro!: complex_differentiable_Polygamma) |
1393 unfolding holomorphic_on_def by (auto intro!: complex_differentiable_Polygamma) |