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) \ \" + by (intro Ints_mult) auto + thus False using assms by simp + qed + moreover have "(x + 1) / 2 \ \" + proof + assume "(x + 1) / 2 \ \" + hence "2 * ((x + 1) / 2) - 1 \ \" + by (intro Ints_mult Ints_diff) auto + thus False using assms by (simp add: field_simps) + qed + ultimately have "(\n. (f (x / 2) n + g (x / 2) n) + (f ((x+1) / 2) n + g ((x+1) / 2) n)) sums + (cot_pfd (x / 2) + cot_pfd ((x + 1) / 2))" + by (intro sums_add sums) + + also have "(\n. (f (x / 2) n + g (x / 2) n) + (f ((x+1) / 2) n + g ((x+1) / 2) n)) = + (\n. h x (2 * n) + h x (2 * n + 1))" + proof + fix n :: nat + have "(f (x / 2) n + g (x / 2) n) + (f ((x+1) / 2) n + g ((x+1) / 2) n) = + (f (x / 2) n + f ((x+1) / 2) n) + (g (x / 2) n + g ((x+1) / 2) n)" + by algebra + also have "f (x / 2) n + f ((x+1) / 2) n = 2 * (f x (2 * n + 1) + f x (2 * n + 2))" + by (simp add: f_def field_simps) + also have "g (x / 2) n + g ((x+1) / 2) n = 2 * (g x (2 * n) + g x (2 * n + 1))" + by (simp add: g_def field_simps) + also have "2 * (f x (2 * n + 1) + f x (2 * n + 2)) + \ = + h x (2 * n) + h x (2 * n + 1)" + unfolding h_def by (simp add: algebra_simps) + finally show "(f (x / 2) n + g (x / 2) n) + (f ((x+1) / 2) n + g ((x+1) / 2) n) = + h x (2 * n) + h x (2 * n + 1)" . + qed + finally have sum1: + "(\n. h x (2 * n) + h x (2 * n + 1)) sums (cot_pfd (x / 2) + cot_pfd ((x + 1) / 2))" . + + have "f x \ 0" unfolding f_def + by (intro tendsto_divide_0[OF tendsto_const] + tendsto_add_filterlim_at_infinity[OF tendsto_const] + filterlim_compose[OF tendsto_of_nat] filterlim_Suc) + hence "(\n. 2 * (f x n + g x n) + 2 * (f x (Suc n) - f x n)) sums (2 * cot_pfd x + 2 * (0 - f x 0))" + by (intro sums_add sums sums_mult telescope_sums assms) + also have "(\n. 2 * (f x n + g x n) + 2 * (f x (Suc n) - f x n)) = h x" + by (simp add: h_def algebra_simps fun_eq_iff) + finally have *: "h x sums (2 * cot_pfd x - 2 * f x 0)" + by simp + + have "(\n. sum (h x) {n * 2..n. sum (h x) {n*2..n. h x (2 * n) + h x (2 * n + 1))" + by (simp add: mult_ac) + finally have sum2: "(\n. h x (2 * n) + h x (2 * n + 1)) sums (2 * cot_pfd x - 2 * f x 0)" . + + have "cot_pfd (x / 2) + cot_pfd ((x + 1) / 2) = 2 * cot_pfd x - 2 * f x 0" + using sum1 sum2 sums_unique2 by blast + also have "2 * f x 0 = 2 / (x + 1)" + by (simp add: f_def) + finally show ?thesis by algebra +qed + +lemma cot_pfd_funeq_real: + fixes x :: real + assumes "x \ \" + shows "2 * cot_pfd x = cot_pfd (x / 2) + cot_pfd ((x + 1) / 2) + 2 / (x + 1)" +proof - + have "complex_of_real (2 * cot_pfd x) = 2 * cot_pfd (complex_of_real x)" + by simp + also have "\ = complex_of_real (cot_pfd (x / 2) + cot_pfd ((x + 1) / 2) + 2 / (x + 1))" + using assms by (subst cot_pfd_funeq_complex) (auto simp flip: cot_pfd_complex_of_real) + finally show ?thesis + by (simp only: of_real_eq_iff) +qed + + +subsection \The limit at 0\ + +lemma cot_pfd_real_tendsto_0: "cot_pfd \0\ (0 :: real)" +proof - + have "filterlim cot_pfd (nhds 0) (at (0 :: real) within ball 0 1)" + proof (rule swap_uniform_limit) + show "uniform_limit (ball 0 1) + (\N x. \n2 - (real (Suc n))\<^sup>2)) cot_pfd sequentially" + using uniform_limit_cot_pfd_real[OF zero_le_one] by (rule uniform_limit_on_subset) auto + have "((\x. 2 * x / (x\<^sup>2 - (real (Suc n))\<^sup>2)) \ 0) (at 0 within ball 0 1)" for n + proof (rule filterlim_mono) + show "((\x. 2 * x / (x\<^sup>2 - (real (Suc n))\<^sup>2)) \ 0) (at 0)" + by real_asymp + qed (auto simp: at_within_le_at) + thus "\\<^sub>F N in sequentially. + ((\x. \n2 - (real (Suc n))\<^sup>2)) \ 0) (at 0 within ball 0 1)" + by (intro always_eventually allI tendsto_null_sum) + qed auto + thus ?thesis + by (simp add: at_within_open_NO_MATCH) +qed + + +subsection \Final result\ + +text \ + To show the final result, we first prove the real case using Herglotz's trick, following + the presentation in Proofs from {THE BOOK}'.~\cite[Chapter~23]{thebook}. +\ +lemma cot_pfd_formula_real: + assumes "x \ \" + shows "pi * cot (pi * x) = 1 / x + cot_pfd x" +proof - + have ev_not_int: "eventually (\x. r x \$$ (at x)" + if "filterlim r (at (r x)) (at x)" for r :: "real \ real" and x :: real + proof (rule eventually_compose_filterlim[OF _ that]) + show "eventually (\x. x \ \) (at (r x))" + using Ints_not_limpt[of "r x"] islimpt_iff_eventually by blast + qed + + text \ + We define the function $h(z)$ as the difference of the left-hand side and right-hand side. + The left-hand side and right-hand side have singularities at the integers, but we will + later see that these can be removed as \h\ tends to \0\ there. + \ + define f :: "real \ real" where "f = (\x. pi * cot (pi * x))" + define g :: "real \ real" where "g = (\x. 1 / x + cot_pfd x)" + define h where "h = (\x. if x \ \ then 0 else f x - g x)" + + have [simp]: "h x = 0" if "x \ \" for x + using that by (simp add: h_def) + + text \ + It is easy to see that the left-hand side and the right-hand side, and as a consequence + also our function \h\, are odd and periodic with period 1. + \ + have odd_h: "h (-x) = -h x" for x + by (simp add: h_def minus_in_Ints_iff f_def g_def) + have per_f: "f (x + 1) = f x" for x + by (simp add: f_def algebra_simps cot_def) + have per_g: "g (x + 1) = g x" if "x \ \" for x + using that by (simp add: g_def cot_pfd_plus_1_real) + interpret h: periodic_fun_simple' h + by standard (auto simp: h_def per_f per_g) + + text \ + \h\ tends to 0 at 0 (and thus at all the integers). + \ + have h_lim: "h \0\ 0" + proof (rule Lim_transform_eventually) + have "eventually (\x. x \ \) (at (0 :: real))" + by (rule ev_not_int) real_asymp + thus "eventually (\x::real. pi * cot (pi * x) - 1 / x - cot_pfd x = h x) (at 0)" + by eventually_elim (simp add: h_def f_def g_def) + next + have "(\x::real. pi * cot (pi * x) - 1 / x) \0\ 0" + unfolding cot_def by real_asymp + hence "(\x::real. pi * cot (pi * x) - 1 / x - cot_pfd x) \0\ 0 - 0" + by (intro tendsto_intros cot_pfd_real_tendsto_0) + thus "(\x. pi * cot (pi * x) - 1 / x - cot_pfd x) \0\ 0" + by simp + qed + + text \ + This means that our \h\ is in fact continuous everywhere: + \ + have cont_h: "continuous_on A h" for A + proof - + have "isCont h x" for x + proof (cases "x \ \") + case True + then obtain n where [simp]: "x = of_int n" + by (auto elim: Ints_cases) + show ?thesis unfolding isCont_def + by (subst at_to_0) (use h_lim in \simp add: filterlim_filtermap h.plus_of_int\) + next + case False + have "continuous_on (-\) (\x. f x - g x)" + by (auto simp: f_def g_def sin_times_pi_eq_0 mult.commute[of pi] intro!: continuous_intros) + hence "isCont (\x. f x - g x) x" + by (rule continuous_on_interior) + (use False in \auto simp: interior_open open_Compl[OF closed_Ints]\) + also have "eventually (\y. y \ -\) (nhds x)" + using False by (intro eventually_nhds_in_open) auto + hence "eventually (\x. f x - g x = h x) (nhds x)" + by eventually_elim (auto simp: h_def) + hence "isCont (\x. f x - g x) x \ isCont h x" + by (rule isCont_cong) + finally show ?thesis . + qed + thus ?thesis + by (simp add: continuous_at_imp_continuous_on) + qed + note [continuous_intros] = continuous_on_compose2[OF cont_h] + + text \ + Through the functional equations of the sine and cosine function, we can derive + the following functional equation for \f\ that holds for all non-integer reals: + \ + have eq_f: "f x = (f (x / 2) + f ((x + 1) / 2)) / 2" if "x \ \" for x + proof - + have "x / 2 \ \" + using that by (metis Ints_add field_sum_of_halves) + hence nz1: "sin (x/2 * pi) \ 0" + by (subst sin_times_pi_eq_0) auto + + have "(x + 1) / 2 \ \" + proof + assume "(x + 1) / 2 \ \" + hence "2 * ((x + 1) / 2) - 1 \ \" + by (intro Ints_mult Ints_diff) auto + thus False using that by (simp add: field_simps) + qed + hence nz2: "sin ((x+1)/2 * pi) \ 0" + by (subst sin_times_pi_eq_0) auto + + have nz3: "sin (x * pi) \ 0" + using that by (subst sin_times_pi_eq_0) auto + + have eq: "sin (pi * x) = 2 * sin (pi * x / 2) * cos (pi * x / 2)" + "cos (pi * x) = (cos (pi * x / 2))\<^sup>2 - (sin (pi * x / 2))\<^sup>2" + using sin_double[of "pi * x / 2"] cos_double[of "pi * x / 2"] by simp_all + show ?thesis using nz1 nz2 nz3 + apply (simp add: f_def cot_def field_simps ) + apply (simp add: add_divide_distrib sin_add cos_add power2_eq_square eq algebra_simps) + done + qed + + text \ + The corresponding functional equation for \<^const>\cot_pfd\ that we have already shown + leads to the same functional equation for \g\ as we just showed for \f\: + \ + have eq_g: "g x = (g (x / 2) + g ((x + 1) / 2)) / 2" if "x \ \" for x + using cot_pfd_funeq_real[OF that] by (simp add: g_def) + + text \ + This then leads to the same functional equation for \h\, and because \h\ is continuous + everywhere, we can extend the validity of the equation to the full domain. + \ + have eq_h: "h x = (h (x / 2) + h ((x + 1) / 2)) / 2" for x + proof - + have "eventually (\x. x \ \) (at x)" "eventually (\x. x / 2 \ \) (at x)" + "eventually (\x. (x + 1) / 2 \ \) (at x)" + by (rule ev_not_int; real_asymp)+ + hence "eventually (\x. h x - (h (x / 2) + h ((x + 1) / 2)) / 2 = 0) (at x)" + proof eventually_elim + case (elim x) + thus ?case using eq_f[of x] eq_g[of x] + by (simp add: h_def field_simps) + qed + hence "(\x. h x - (h (x / 2) + h ((x + 1) / 2)) / 2) \x\ 0" + by (simp add: tendsto_eventually) + moreover have "continuous_on UNIV (\x. h x - (h (x / 2) + h ((x + 1) / 2)) / 2)" + by (auto intro!: continuous_intros) + ultimately have "h x - (h (x / 2) + h ((x + 1) / 2)) / 2 = 0" + by (meson LIM_unique UNIV_I continuous_on_def) + thus ?thesis + by simp + qed + + text \ + Since \h\ is periodic with period 1 and continuous, it must attain a global maximum \h\ + somewhere in the interval $[0, 1]$. Let's call this maximum $m$ and let $x_0$ be some point + in the interval $[0, 1]$ such that $h(x_0) = m$. + \ + define m where "m = Sup (h  {0..1})" + have "m \ h  {0..1}" + unfolding m_def + proof (rule closed_contains_Sup) + have "compact (h  {0..1})" + by (intro compact_continuous_image cont_h) auto + thus "bdd_above (h  {0..1})" "closed (h  {0..1})" + by (auto intro: compact_imp_closed compact_imp_bounded bounded_imp_bdd_above) + qed auto + then obtain x0 where x0: "x0 \ {0..1}" "h x0 = m" + by blast + + have h_le_m: "h x \ m" for x + proof - + have "h x = h (frac x)" + unfolding frac_def by (rule h.minus_of_int [symmetric]) + also have "\ \ m" unfolding m_def + proof (rule cSup_upper) + have "frac x \ {0..1}" + using frac_lt_1[of x] by auto + thus "h (frac x) \ h  {0..1}" + by blast + next + have "compact (h  {0..1})" + by (intro compact_continuous_image cont_h) auto + thus "bdd_above (h  {0..1})" + by (auto intro: compact_imp_bounded bounded_imp_bdd_above) + qed + finally show ?thesis . + qed + + text \ + Through the functional equation for \h\, we can show that if \h\ attains its maximum at + some point \x\, it also attains it at $\frac{1}{2} x$. By iterating this, it attains the + maximum at all points of the form $2^{-n} x_0$. + \ + have h_eq_m_iter_aux: "h (x / 2) = m" if "h x = m" for x + using eq_h[of x] that h_le_m[of "x / 2"] h_le_m[of "(x + 1) / 2"] by simp + have h_eq_m_iter: "h (x0 / 2 ^ n) = m" for n + proof (induction n) + case (Suc n) + have "h (x0 / 2 ^ Suc n) = h (x0 / 2 ^ n / 2)" + by (simp add: field_simps) + also have "\ = m" + by (rule h_eq_m_iter_aux) (use Suc.IH in auto) + finally show ?case . + qed (use x0 in auto) + + text \ + Since the sequence $n \mapsto 2^{-n} x_0$ tends to 0 and \h\ is continuous, we derive \m = 0\. + \ + have "(\n. h (x0 / 2 ^ n)) \ h 0" + by (rule continuous_on_tendsto_compose[OF cont_h[of UNIV]]) (force | real_asymp)+ + moreover from h_eq_m_iter have "(\n. h (x0 / 2 ^ n)) \ m" + by simp + ultimately have "m = h 0" + using tendsto_unique by force + hence "m = 0" + by simp + + text \ + Since \h\ is odd, this means that \h\ is identically zero everywhere, and our result follows. + \ + have "h x = 0" + using h_le_m[of x] h_le_m[of "-x"] \m = 0\ odd_h[of x] by linarith + thus ?thesis + using assms by (simp add: h_def f_def g_def) +qed + + +text \ + We now lift the result from the domain \\\\\ to \\\\\. We do this by noting that \\\\\ is + connected and the point $\frac{1}{2}$ is both in \\\\\ and a limit point of \\\\\. +\ +lemma one_half_limit_point_Reals_minus_Ints: "(1 / 2 :: complex) islimpt \ - \" +proof (rule islimptI) + fix T :: "complex set" + assume "1 / 2 \ T" "open T" + then obtain r where r: "r > 0" "ball (1 / 2) r \ T" + using open_contains_ball by blast + define y where "y = 1 / 2 + min r (1 / 2) / 2" + have "y \ {0<..<1}" + using r by (auto simp: y_def) + hence "complex_of_real y \ \ - \" + by (auto elim!: Ints_cases) + moreover have "complex_of_real y \ 1 / 2" + proof + assume "complex_of_real y = 1 / 2" + also have "1 / 2 = complex_of_real (1 / 2)" + by simp + finally have "y = 1 / 2" + unfolding of_real_eq_iff . + with r show False + by (auto simp: y_def) + qed + moreover have "complex_of_real y \ ball (1 / 2) r" + using \r > 0\ by (auto simp: y_def dist_norm) + with r have "complex_of_real y \ T" + by blast + ultimately show "\y\\ - \. y \ T \ y \ 1 / 2" + by blast +qed + +theorem cot_pfd_formula_complex: + fixes z :: complex + assumes "z \ \" + shows "pi * cot (pi * z) = 1 / z + cot_pfd z" +proof - + let ?f = "\z::complex. pi * cot (pi * z) - 1 / z - cot_pfd z" + have "pi * cot (pi * z) - 1 / z - cot_pfd z = 0" + proof (rule analytic_continuation[where f = ?f]) + show "?f holomorphic_on -\" + unfolding cot_def by (intro holomorphic_intros) (auto simp: sin_eq_0) + next + show "open (-\ :: complex set)" "connected (-\ :: complex set)" + by (auto intro!: path_connected_imp_connected path_connected_complement_countable countable_int) + next + show "\ - \ \ (-\ :: complex set)" + by auto + next + show "(1 / 2 :: complex) islimpt \ - \" + by (rule one_half_limit_point_Reals_minus_Ints) + next + show "1 / (2 :: complex) \ -\" + using fraction_not_in_ints[of 2 1, where ?'a = complex] by auto + next + show "z \ -\" + using assms by simp + next + show "?f z = 0" if "z \ \ - \" for z + proof - + have "complex_of_real pi * cot (complex_of_real pi * z) - 1 / z - cot_pfd z = + complex_of_real (pi * cot (pi * Re z) - 1 / Re z - cot_pfd (Re z))" + using that by (auto elim!: Reals_cases simp: cot_of_real) + also have "\ = 0" + by (subst cot_pfd_formula_real) (use that in \auto elim!: Reals_cases\) + finally show ?thesis . + qed + qed + thus ?thesis + by algebra +qed + +end \ No newline at end of file diff --git a/thys/Cotangent_PFD_Formula/ROOT b/thys/Cotangent_PFD_Formula/ROOT new file mode 100644 --- /dev/null +++ b/thys/Cotangent_PFD_Formula/ROOT @@ -0,0 +1,12 @@ +chapter AFP + +session Cotangent_PFD_Formula (AFP) = "HOL-Complex_Analysis" + + options [timeout = 600] + sessions + "HOL-Real_Asymp" + theories + Cotangent_PFD_Formula + document_files + "root.tex" + "root.bib" + diff --git a/thys/Cotangent_PFD_Formula/document/root.bib b/thys/Cotangent_PFD_Formula/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Cotangent_PFD_Formula/document/root.bib @@ -0,0 +1,8 @@ +@book{thebook, +author = {Aigner, Martin and Ziegler, Günter M.}, +title = {Proofs from {THE BOOK}}, +year = {2009}, +isbn = {3642008550}, +publisher = {Springer}, +edition = {4th} +} diff --git a/thys/Cotangent_PFD_Formula/document/root.tex b/thys/Cotangent_PFD_Formula/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Cotangent_PFD_Formula/document/root.tex @@ -0,0 +1,41 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} +\usepackage{amsfonts,amsmath,amssymb} +\usepackage{pgfplots} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +\begin{document} + +\title{A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent} +\author{Manuel Eberl} +\maketitle + +\begin{abstract} +In this article, I formalise a proof from THE BOOK~\cite[Chapter~23]{thebook}; namely a formula that was called one of the most beautiful formulas involving elementary functions': +$\pi \cot(\pi z) = \frac{1}{z} + \sum_{n=1}^\infty\left(\frac{1}{z+n} + \frac{1}{z-n}\right)$ +The proof uses Herglotz's trick to show the real case and analytic continuation for the complex case. +\end{abstract} + +\tableofcontents +\newpage +\parindent 0pt\parskip 0.5ex + +\input{session} + +\nocite{corless96} +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,669 +1,670 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras +Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PAL PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quasi_Borel_Spaces Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL