diff --git a/thys/Cotangent_PFD_Formula/Cotangent_PFD_Formula.thy b/thys/Cotangent_PFD_Formula/Cotangent_PFD_Formula.thy
new file mode 100644
--- /dev/null
+++ b/thys/Cotangent_PFD_Formula/Cotangent_PFD_Formula.thy
@@ -0,0 +1,800 @@
+(*
+ File: Cotangent_PFD_Formula.thy
+ Author: Manuel Eberl, University of Innsbruck
+
+ A proof of the "partial fraction decomposition"-style sum formula for the contangent function.
+*)
+section \The Partial-Fraction Formula for the Cotangent Function\
+theory Cotangent_PFD_Formula
+ imports "HOL-Complex_Analysis.Complex_Analysis" "HOL-Real_Asymp.Real_Asymp"
+begin
+
+subsection \Auxiliary lemmas\
+
+(* TODO Move *)
+text \
+ The following variant of the comparison test for showing summability allows us to use
+ a `Big-O' estimate, which works well together with Isabelle's automation for real asymptotics.
+\
+lemma summable_comparison_test_bigo:
+ fixes f :: "nat \ real"
+ assumes "summable (\n. norm (g n))" "f \ O(g)"
+ shows "summable f"
+proof -
+ from \f \ O(g)\ obtain C where C: "eventually (\x. norm (f x) \ C * norm (g x)) at_top"
+ by (auto elim: landau_o.bigE)
+ thus ?thesis
+ by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult)
+qed
+
+lemma uniformly_on_image:
+ "uniformly_on (f ` A) g = filtercomap (\h. h \ f) (uniformly_on A (g \ f))"
+ unfolding uniformly_on_def by (simp add: filtercomap_INF)
+
+lemma uniform_limit_image:
+ "uniform_limit (f ` A) g h F \ uniform_limit A (\x y. g x (f y)) (\x. h (f x)) F"
+ by (simp add: uniformly_on_image filterlim_filtercomap_iff o_def)
+
+lemma Ints_add_iff1 [simp]: "x \ \ \ x + y \ \ \ y \ \"
+ by (metis Ints_add Ints_diff add.commute add_diff_cancel_right')
+
+lemma Ints_add_iff2 [simp]: "y \ \ \ x + y \ \ \ x \ \"
+ by (metis Ints_add Ints_diff add_diff_cancel_right')
+
+text \
+ If a set is discrete (i.e. the difference between any two points is bounded from below),
+ it has no limit points:
+\
+lemma discrete_imp_not_islimpt:
+ assumes e: "0 < e"
+ and d: "\x \ S. \y \ S. dist y x < e \ y = x"
+ shows "\x islimpt S"
+proof
+ assume "x islimpt S"
+ hence "x islimpt S - {x}"
+ by (meson islimpt_punctured)
+ moreover from assms have "closed (S - {x})"
+ by (intro discrete_imp_closed) auto
+ ultimately show False
+ unfolding closed_limpt by blast
+qed
+
+text \
+ In particular, the integers have no limit point:
+\
+lemma Ints_not_limpt: "\((x :: 'a :: real_normed_algebra_1) islimpt \)"
+ by (rule discrete_imp_not_islimpt[of 1]) (auto elim!: Ints_cases simp: dist_of_int)
+
+text \
+ The following lemma allows evaluating telescoping sums of the form
+ \[\sum\limits_{n=0}^\infty \left(f(n) - f(n + k)\right)\]
+ where $f(n) \longrightarrow 0$, i.e.\ where all terms except for the first \k\ are
+ cancelled by later summands.
+\
+lemma sums_long_telescope:
+ fixes f :: "nat \ 'a :: {topological_group_add, topological_comm_monoid_add, ab_group_add}"
+ assumes lim: "f \ 0"
+ shows "(\n. f n - f (n + c)) sums (\kN. ?S - (\n ?S - 0"
+ by (intro tendsto_intros tendsto_null_sum filterlim_compose[OF assms]; real_asymp)
+ hence "(\N. ?S - (\n ?S"
+ by simp
+ moreover have "eventually (\N. ?S - (\nnnnnnn\{.. {c.. = (\nn\{c..nn\{c..n. n - c" "\n. n + c"]) auto
+ also have "\ = (\n\{c..{N.. = (\n\{c..n\{N..n\{N..nn. n + N" "\n. n - N"]) auto
+ finally show ?case
+ by simp
+ qed
+ ultimately show ?thesis
+ unfolding sums_def by (rule Lim_transform_eventually)
+qed
+
+
+subsection \Definition of auxiliary function\
+
+text \
+ The following function is the infinite sum appearing on the right-hand side of the
+ cotangent formula. It can be written either as
+ \[\sum_{n=1}^\infty\left(\frac{1}{x + n} + \frac{1}{x - n}\right)\]
+ or as
+ \[2x \sum_{n=1}^\infty \frac{1}{x^2 - n^2}\ .\]
+\
+definition cot_pfd :: "'a :: {real_normed_field, banach} \ 'a" where
+ "cot_pfd x = (\n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))"
+
+text \
+ The sum in the definition of \<^const>\cot_pfd\ converges uniformly on compact sets.
+ This implies, in particular, that \<^const>\cot_pfd\ is holomorphic (and thus also continuous).
+\
+lemma uniform_limit_cot_pfd_complex:
+ assumes "R \ 0"
+ shows "uniform_limit (cball 0 R :: complex set)
+ (\N x. \nN. of_nat (N + 1) > R) at_top"
+ by real_asymp
+ thus "\\<^sub>F N in sequentially. \(x::complex)\cball 0 R. norm (2 * x / (x ^ 2 - of_nat (Suc N) ^ 2)) \
+ 2 * R / (real (N + 1) ^ 2 - R ^ 2)"
+ proof eventually_elim
+ case (elim N)
+ show ?case
+ proof safe
+ fix x :: complex assume x: "x \ cball 0 R"
+ have "(1 + real N)\<^sup>2 - R\<^sup>2 \ norm ((1 + of_nat N :: complex) ^ 2) - norm (x ^ 2)"
+ using x by (auto intro: power_mono simp: norm_power simp flip: of_nat_Suc)
+ also have "\ \ norm (x\<^sup>2 - (1 + of_nat N :: complex)\<^sup>2)"
+ by (metis norm_minus_commute norm_triangle_ineq2)
+ finally show "norm (2 * x / (x\<^sup>2 - (of_nat (Suc N))\<^sup>2)) \ 2 * R / (real (N + 1) ^ 2 - R ^ 2)"
+ unfolding norm_mult norm_divide using \R \ 0\ x elim
+ by (intro mult_mono frac_le) (auto intro: power_strict_mono)
+ qed
+ qed
+next
+ show "summable (\N. 2 * R / (real (N + 1) ^ 2 - R ^ 2))"
+ proof (rule summable_comparison_test_bigo)
+ show "(\N. 2 * R / (real (N + 1) ^ 2 - R ^ 2)) \ O(\N. 1 / real N ^ 2)"
+ by real_asymp
+ next
+ show "summable (\n. norm (1 / real n ^ 2))"
+ using inverse_power_summable[of 2] by (simp add: field_simps)
+ qed
+qed
+
+lemma sums_cot_pfd_complex:
+ fixes x :: complex
+ shows "(\n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) sums cot_pfd x"
+ using tendsto_uniform_limitI[OF uniform_limit_cot_pfd_complex[of "norm x"], of x]
+ by (simp add: sums_def)
+
+lemma sums_cot_pfd_complex':
+ fixes x :: complex
+ assumes "x \ \"
+ shows "(\n. 1 / (x + of_nat (Suc n)) + 1 / (x - of_nat (Suc n))) sums cot_pfd x"
+proof -
+ have "(\n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) sums cot_pfd x"
+ by (rule sums_cot_pfd_complex)
+ also have "(\n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) =
+ (\n. 1 / (x + of_nat (Suc n)) + 1 / (x - of_nat (Suc n)))" (is "?lhs = ?rhs")
+ proof
+ fix n :: nat
+ have neq1: "x + of_nat (Suc n) \ 0"
+ using assms by (metis Ints_0 Ints_add_iff2 Ints_of_nat)
+ have neq2: "x - of_nat (Suc n) \ 0"
+ using assms by force
+ have neq3: "x ^ 2 - of_nat (Suc n) ^ 2 \ 0"
+ using assms by (metis Ints_of_nat eq_iff_diff_eq_0 minus_in_Ints_iff power2_eq_iff)
+ show "?lhs n = ?rhs n" using neq1 neq2 neq3
+ by (simp add: divide_simps del: of_nat_Suc) (auto simp: power2_eq_square algebra_simps)
+ qed
+ finally show ?thesis .
+qed
+
+lemma summable_cot_pfd_complex:
+ fixes x :: complex
+ shows "summable (\n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))"
+ using sums_cot_pfd_complex[of x] by (simp add: sums_iff)
+
+lemma summable_cot_pfd_real:
+ fixes x :: real
+ shows "summable (\n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))"
+proof -
+ have "summable (\n. complex_of_real (2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)))"
+ using summable_cot_pfd_complex[of "of_real x"] by simp
+ also have "?this \ ?thesis"
+ by (rule summable_of_real_iff)
+ finally show ?thesis .
+qed
+
+lemma sums_cot_pfd_real:
+ fixes x :: real
+ shows "(\n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) sums cot_pfd x"
+ using summable_cot_pfd_real[of x] by (simp add: cot_pfd_def sums_iff)
+
+lemma cot_pfd_complex_of_real [simp]: "cot_pfd (complex_of_real x) = of_real (cot_pfd x)"
+ using sums_of_real[OF sums_cot_pfd_real[of x], where ?'a = complex]
+ sums_cot_pfd_complex[of "of_real x"] sums_unique2 by auto
+
+lemma uniform_limit_cot_pfd_real:
+ assumes "R \ 0"
+ shows "uniform_limit (cball 0 R :: real set)
+ (\N x. \nN x. Re (\nx. Re (cot_pfd x)) sequentially"
+ by (intro uniform_limit_intros uniform_limit_cot_pfd_complex assms)
+ hence "uniform_limit (of_real ` cball 0 R)
+ (\N x. Re (\nx. Re (cot_pfd x)) sequentially"
+ by (rule uniform_limit_on_subset) auto
+ thus ?thesis
+ by (simp add: uniform_limit_image)
+qed
+
+
+subsection \Holomorphicity and continuity\
+
+lemma holomorphic_on_cot_pfd [holomorphic_intros]:
+ assumes "A \ -(\-{0})"
+ shows "cot_pfd holomorphic_on A"
+proof -
+ have *: "open (-(\-{0}) :: complex set)"
+ by (intro open_Compl closed_subset_Ints) auto
+ define f :: "nat \ complex \ complex"
+ where "f = (\N x. \n-{0})"
+ proof (rule holomorphic_uniform_sequence[OF *])
+ fix n :: nat
+ have **: "x\<^sup>2 - (of_nat (Suc n))\<^sup>2 \ 0" if "x \ -(\-{0})" for x :: complex and n :: nat
+ proof
+ assume "x\<^sup>2 - (of_nat (Suc n))\<^sup>2 = 0"
+ hence "(of_nat (Suc n))\<^sup>2 = x\<^sup>2"
+ by algebra
+ hence "x = of_nat (Suc n) \ x = -of_nat (Suc n)"
+ by (subst (asm) eq_commute, subst (asm) power2_eq_iff) auto
+ moreover have "(of_nat (Suc n) :: complex) \ \" "(-of_nat (Suc n) :: complex) \ \"
+ by (intro Ints_minus Ints_of_nat)+
+ ultimately show False using that
+ by (auto simp del: of_nat_Suc)
+ qed
+ show "f n holomorphic_on -(\ - {0})"
+ unfolding f_def by (intro holomorphic_intros **)
+ next
+ fix z :: complex assume z: "z \ -(\ - {0})"
+ from * z obtain r where r: "r > 0" "cball z r \ -(\-{0})"
+ using open_contains_cball by blast
+ have "uniform_limit (cball z r) f cot_pfd sequentially"
+ using uniform_limit_cot_pfd_complex[of "norm z + r"] unfolding f_def
+ proof (rule uniform_limit_on_subset)
+ show "cball z r \ cball 0 (norm z + r)"
+ unfolding cball_subset_cball_iff by (auto simp: dist_norm)
+ qed (use \r > 0\ in auto)
+ with r show "\d>0. cball z d \ - (\ - {0}) \ uniform_limit (cball z d) f cot_pfd sequentially"
+ by blast
+ qed
+ thus ?thesis
+ by (rule holomorphic_on_subset) fact
+qed
+
+lemma continuous_on_cot_pfd_complex [continuous_intros]:
+ assumes "A \ -(\-{0})"
+ shows "continuous_on A (cot_pfd :: complex \ complex)"
+ by (rule holomorphic_on_imp_continuous_on holomorphic_intros assms)+
+
+lemma continuous_on_cot_pfd_real [continuous_intros]:
+ assumes "A \ -(\-{0})"
+ shows "continuous_on A (cot_pfd :: real \ real)"
+proof -
+ have "continuous_on A (Re \ cot_pfd \ of_real)"
+ by (intro continuous_intros) (use assms in auto)
+ also have "Re \ cot_pfd \ of_real = cot_pfd"
+ by auto
+ finally show ?thesis .
+qed
+
+
+subsection \Functional equations\
+
+text \
+ In this section, we will show three few functional equations for the function \<^const>\cot_pfd\.
+ The first one is trivial; the other two are a bit tedious and not very insightful, so I
+ will not comment on them.
+\
+
+text \\<^const>\cot_pfd\ is an odd function:\
+lemma cot_pfd_complex_minus [simp]: "cot_pfd (-x :: complex) = -cot_pfd x"
+proof -
+ have "(\n. 2 * (-x) / ((-x) ^ 2 - of_nat (Suc n) ^ 2)) =
+ (\n. - (2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)))"
+ by simp
+ also have "\ sums -cot_pfd x"
+ by (intro sums_minus sums_cot_pfd_complex)
+ finally show ?thesis
+ using sums_cot_pfd_complex[of "-x"] sums_unique2 by blast
+qed
+
+lemma cot_pfd_real_minus [simp]: "cot_pfd (-x :: real) = -cot_pfd x"
+ using cot_pfd_complex_minus[of "of_real x"]
+ unfolding of_real_minus [symmetric] cot_pfd_complex_of_real of_real_eq_iff .
+
+text \\<^const>\cot_pfd\ is periodic with period 1:\
+lemma cot_pfd_plus_1_complex:
+ assumes "x \ \"
+ shows "cot_pfd (x + 1 :: complex) = cot_pfd x - 1 / (x + 1) + 1 / x"
+proof -
+ have *: "x ^ 2 \ of_nat n ^ 2" if "x \ \" for x :: complex and n
+ using that by (metis Ints_of_nat minus_in_Ints_iff power2_eq_iff)
+ have **: "x + of_nat n \ 0" if "x \ \" for x :: complex and n
+ using that by (metis Ints_0 Ints_add_iff2 Ints_of_nat)
+ have [simp]: "x \ 0"
+ using assms by auto
+ have [simp]: "x + 1 \ 0"
+ using assms by (metis "**" of_nat_1)
+ have [simp]: "x + 2 \ 0"
+ using **[of x 2] assms by simp
+
+ have lim: "(\n. 1 / (x + of_nat (Suc n))) \ 0"
+ by (intro tendsto_divide_0[OF tendsto_const] tendsto_add_filterlim_at_infinity[OF tendsto_const]
+ filterlim_compose[OF tendsto_of_nat] filterlim_Suc)
+ have sum1: "(\n. 1 / (x + of_nat (Suc n)) - 1 / (x + of_nat (Suc n + 2))) sums
+ (\n<2. 1 / (x + of_nat (Suc n)))"
+ using sums_long_telescope[OF lim, of 2] by (simp add: algebra_simps)
+
+ have "(\n. 2 * x / (x\<^sup>2 - (of_nat (Suc n))\<^sup>2) - 2 * (x + 1) / ((x + 1)^2 - (of_nat (Suc (Suc n)))\<^sup>2))
+ sums (cot_pfd x - (cot_pfd (x + 1) - 2 * (x + 1) / ((x + 1)^2 - (of_nat (Suc 0) ^ 2))))"
+ using sums_cot_pfd_complex[of "x + 1"]
+ by (intro sums_diff sums_cot_pfd_complex, subst sums_Suc_iff) auto
+ also have "2 * (x + 1) / ((x + 1)^2 - (of_nat (Suc 0) ^ 2)) = 2 * (x + 1) / (x * (x + 2))"
+ by (simp add: algebra_simps power2_eq_square)
+ also have "(\n. 2 * x / (x\<^sup>2 - (of_nat (Suc n))\<^sup>2) -
+ 2 * (x + 1) / ((x + 1)\<^sup>2 - (of_nat (Suc (Suc n)))\<^sup>2)) =
+ (\n. 1 / (x + of_nat (Suc n)) - 1 / (x + of_nat (Suc n + 2)))"
+ using *[of x] *[of "x + 1"] **[of x] **[of "x + 1"] assms
+ apply (intro ext)
+ apply (simp add: divide_simps del: of_nat_add of_nat_Suc)
+ apply (simp add: algebra_simps power2_eq_square)
+ done
+ finally have sum2: "(\n. 1 / (x + of_nat (Suc n)) - 1 / (x + of_nat (Suc n + 2))) sums
+ (cot_pfd x - cot_pfd (x + 1) + 2 * (x + 1) / (x * (x + 2)))"
+ by (simp add: algebra_simps)
+
+ have "cot_pfd x - cot_pfd (x + 1) + 2 * (x + 1) / (x * (x + 2)) =
+ (\n<2. 1 / (x + of_nat (Suc n)))"
+ using sum1 sum2 sums_unique2 by blast
+ hence "cot_pfd x - cot_pfd (x + 1) = -2 * (x + 1) / (x * (x + 2)) + 1 / (x + 1) + 1 / (x + 2)"
+ by (simp add: eval_nat_numeral divide_simps) algebra?
+ also have "\ = 1 / (x + 1) - 1 / x"
+ by (simp add: divide_simps) algebra?
+ finally show ?thesis
+ by algebra
+qed
+
+lemma cot_pfd_plus_1_real:
+ assumes "x \ \"
+ shows "cot_pfd (x + 1 :: real) = cot_pfd x - 1 / (x + 1) + 1 / x"
+proof -
+ have "cot_pfd (complex_of_real (x + 1)) = cot_pfd (of_real x) - 1 / (of_real x + 1) + 1 / of_real x"
+ using cot_pfd_plus_1_complex[of x] assms by simp
+ also have "\ = complex_of_real (cot_pfd x - 1 / (x + 1) + 1 / x)"
+ by simp
+ finally show ?thesis
+ unfolding cot_pfd_complex_of_real of_real_eq_iff .
+qed
+
+text \
+ \<^const>\cot_pfd\ satisfies the following functional equation:
+ \[2 f(x) = f\left(\frac{x}{2}\right) + f\left(\frac{x+1}{2}\right) + \frac{2}{x+1}\]
+\
+lemma cot_pfd_funeq_complex:
+ fixes x :: complex
+ assumes "x \ \"
+ shows "2 * cot_pfd x = cot_pfd (x / 2) + cot_pfd ((x + 1) / 2) + 2 / (x + 1)"
+proof -
+ define f :: "complex \ nat \ complex" where "f = (\x n. 1 / (x + of_nat (Suc n)))"
+ define g :: "complex \ nat \ complex" where "g = (\x n. 1 / (x - of_nat (Suc n)))"
+ define h :: "complex \ nat \ complex" where "h = (\x n. 2 * (f x (n + 1) + g x n))"
+
+ have sums: "(\n. f x n + g x n) sums cot_pfd x" if "x \ \" for x
+ unfolding f_def g_def by (intro sums_cot_pfd_complex' that)
+
+ have "x / 2 \ \"
+ proof
+ assume "x / 2 \ \"
+ hence "2 * (x / 2) \