# Theory Sophomores_Dream

(*
File:    Sophomores_Dream.thy
Author:  Manuel Eberl, University of Innsbruck
*)
section ‹The Sophomore's Dream›
theory Sophomores_Dream
imports "HOL-Analysis.Analysis" "HOL-Real_Asymp.Real_Asymp"
begin

text ‹
This formalisation mostly follows the very clear proof sketch from Wikipedia~\<^cite>‹"wikipedia"›.
That article also provides an interesting historical perspective. A more detailed
exploration of Bernoulli's historical proof can be found in the book by Dunham~\<^cite>‹"dunham"›.

The name Sophomore's Dream' apparently comes from a book by Borwein et al., in analogy to
the Freshman's Dream' equation $(x+y)^n = x^n + y^n$ (which is generally ∗‹not› true except
in rings of characteristic $n$).
›

subsection ‹Continuity and bounds for $x \log x$›

lemma x_log_x_continuous: "continuous_on {0..1} (λx::real. x * ln x)"
proof -
have "continuous (at x within {0..1}) (λx::real. x * ln x)" if "x ∈ {0..1}" for x
proof (cases "x = 0")
case True
have "((λx::real. x * ln x) ⤏ 0) (at_right 0)"
by real_asymp
thus ?thesis using True
by (simp add: continuous_def Lim_ident_at at_within_Icc_at_right)
qed (auto intro!: continuous_intros)
thus ?thesis
using continuous_on_eq_continuous_within by blast
qed

lemma x_log_x_within_01_le:
assumes "x ∈ {0..(1::real)}"
shows   "x * ln x ∈ {-exp (-1)..0}"
proof -
have "x * ln x ≤ 0"
using assms by (cases "x = 0") (auto simp: mult_nonneg_nonpos)
let ?f = "λx::real. x * ln x"
have diff: "(?f has_field_derivative (ln x + 1)) (at x)" if "x > 0" for x
using that by (auto intro!: derivative_eq_intros)
have diff': "?f differentiable at x" if "x > 0" for x
using diff[OF that] real_differentiable_def by blast

consider "x = 0" | "x = 1" | "x = exp (-1)" | "0 < x" "x < exp (-1)" | "exp (-1) < x" "x < 1"
using assms unfolding atLeastAtMost_iff by linarith
hence "x * ln x ≥ -exp (-1)"
proof cases
assume x: "0 < x" "x < exp (-1)"
have "∃l z. x < z ∧ z < exp (-1) ∧ (?f has_real_derivative l) (at z) ∧
?f (exp (-1)) - ?f x = (exp (-1) - x) * l"
using x by (intro MVT continuous_on_subset [OF x_log_x_continuous] diff') auto
then obtain l z where lz:
"x < z" "z < exp (-1)" "(?f has_real_derivative l) (at z)"
"?f x = -exp (-1) - (exp (-1) - x) * l"
by (auto simp: algebra_simps)
have [simp]: "l = ln z + 1"
using DERIV_unique[OF diff[of z] lz(3)] lz(1) x by auto
have "ln z ≤ ln (exp (-1))"
using lz x by (subst ln_le_cancel_iff) auto
hence "(exp (- 1) - x) * l ≤ 0"
using x lz by (intro mult_nonneg_nonpos) auto
with lz show ?thesis
by linarith
next
assume x: "exp (-1) < x" "x < 1"
have "∃l z. exp (-1) < z ∧ z < x ∧ (?f has_real_derivative l) (at z) ∧
?f x - ?f (exp (-1)) = (x - exp (-1)) * l"
proof (intro MVT continuous_on_subset [OF x_log_x_continuous] diff')
fix t :: real assume t: "exp (-1) < t"
show "t > 0"
by (rule less_trans [OF _ t]) auto
qed (use x in auto)
then obtain l z where lz:
"exp (-1) < z" "z < x" "(?f has_real_derivative l) (at z)"
"?f x = -exp (-1) - (exp (-1) - x) * l"
by (auto simp: algebra_simps)
have "z > 0"
by (rule less_trans [OF _ lz(1)]) auto
have [simp]: "l = ln z + 1"
using DERIV_unique[OF diff[of z] lz(3)] ‹z > 0› by auto
have "ln z ≥ ln (exp (-1))"
using lz ‹z > 0› by (subst ln_le_cancel_iff) auto
hence "(exp (- 1) - x) * l ≤ 0"
using x lz by (intro mult_nonpos_nonneg) auto
with lz show ?thesis
by linarith
qed auto

with ‹x * ln x ≤ 0› show ?thesis
by auto
qed

subsection ‹Convergence, Summability, Integrability›

text ‹
As a first result we can show that the two sums that occur in the two different versions
of the Sophomore's Dream are absolutely summable. This is achieved by a simple comparison
test with the series $\sum_{k=1}^\infty k^{-2}$, as $k^{-k} \in O(k^{-2})$.
›
theorem abs_summable_sophomores_dream: "summable (λk. 1 / real (k ^ k))"
proof (rule summable_comparison_test_bigo)
show "(λk. 1 / real (k ^ k)) ∈ O(λk. 1 / real k ^ 2)"
by real_asymp
show "summable (λn. norm (1 / real n ^ 2))"
using inverse_power_summable[of 2, where ?'a = real] by (simp add: field_simps)
qed

text ‹
The existence of the integral is also fairly easy to show since the integrand is continuous
and the integration domain is compact. There is, however, one hiccup: The integrand is not
actually continuous.

We have $\lim_{x\to 0} x^x = 1$, but in Isabelle $0^0$ is defined as ‹0› (for real numbers).
Thus, there is a discontinuity at ‹x = 0›

However, this is a removable discontinuity since for any $x>0$ we have $x^x = e^{x\log x}$, and
as we have just shown, $e^{x \log x}$ ∗‹is› continuous on $[0, 1]$. Since the two integrands
differ only for ‹x = 0› (which is negligible), the integral still exists.
›
theorem integrable_sophomores_dream: "(λx::real. x powr x) integrable_on {0..1}"
proof -
have "(λx::real. exp (x * ln x)) integrable_on {0..1}"
by (intro integrable_continuous_real continuous_on_exp x_log_x_continuous)
also have "?this ⟷ (λx::real. exp (x * ln x)) integrable_on {0<..<1}"
also have "… ⟷ (λx::real. x powr x) integrable_on {0<..<1}"
by (intro integrable_cong) (auto simp: powr_def)
also have "… ⟷ ?thesis"
finally show ?thesis .
qed

text ‹
Next, we have to show the absolute convergence of the two auxiliary sums that will occur in
our proofs so that we can exchange the order of integration and summation. This is done
with a straightforward application of the Weierstra\ss\ ‹M› test.
›
lemma uniform_limit_sophomores_dream1:
"uniform_limit {0..(1::real)}
(λn x. ∑k<n. (x * ln x) ^ k / fact k)
(λx. ∑k. (x * ln x) ^ k / fact k)
sequentially"
proof (rule Weierstrass_m_test)
show "summable (λk. exp (-1) ^ k / fact k :: real)"
using summable_exp[of "exp (-1)"] by (simp add: field_simps)
next
fix k :: nat and x :: real
assume x: "x ∈ {0..1}"
have "norm ((x * ln x) ^ k / fact k) = norm (x * ln x) ^ k / fact k"
also have "… ≤ exp (-1) ^ k / fact k"
by (intro divide_right_mono power_mono) (use x_log_x_within_01_le [of x] x in auto)
finally show "norm ((x * ln x) ^ k / fact k) ≤ exp (- 1) ^ k / fact k" .
qed

lemma uniform_limit_sophomores_dream2:
"uniform_limit {0..(1::real)}
(λn x. ∑k<n. (-(x * ln x)) ^ k / fact k)
(λx. ∑k. (-(x * ln x)) ^ k / fact k)
sequentially"
proof (rule Weierstrass_m_test)
show "summable (λk. exp (-1) ^ k / fact k :: real)"
using summable_exp[of "exp (-1)"] by (simp add: field_simps)
next
fix k :: nat and x :: real
assume x: "x ∈ {0..1}"
have "norm ((-x * ln x) ^ k / fact k) = norm (x * ln x) ^ k / fact k"
also have "… ≤ exp (-1) ^ k / fact k"
by (intro divide_right_mono power_mono) (use x_log_x_within_01_le [of x] x in auto)
finally show "norm ((-(x * ln x)) ^ k / fact k) ≤ exp (- 1) ^ k / fact k" by simp
qed

subsection ‹An auxiliary integral›

text ‹
Next we compute the integral
$\int_0^1 (x\log x)^n\,\text{d}x = \frac{(-1)^n\, n!}{(n+1)^{n+1}}\ ,$
which is a key ingredient in our proof.
›
lemma sophomores_dream_aux_integral:
"((λx. (x * ln x) ^ n) has_integral (- 1) ^ n * fact n / real ((n + 1) ^ (n + 1))) {0<..<1}"
proof -
have "((λt. t powr real n / exp t) has_integral fact n) {0..}"
using Gamma_integral_real[of "n + 1"] by (auto simp: Gamma_fact powr_realpow)
also have "?this ⟷ ((λt. t powr real n / exp t) has_integral fact n) {0<..}"
proof (rule has_integral_spike_set_eq)
have eq: "{x ∈ {0<..} - {0..}. x powr real n / exp x ≠ 0} = {}"
by auto
thus "negligible {x ∈ {0<..} - {0..}. x powr real n / exp x ≠ 0}"
by (subst eq) auto
have "{x ∈ {0..} - {0<..}. x powr real n / exp x ≠ 0} ⊆ {0}"
by auto
moreover have "negligible {0::real}"
by simp
ultimately show "negligible {x ∈ {0..} - {0<..}. x powr real n / exp x ≠ 0}"
by (meson negligible_subset)
qed
also have "… ⟷ ((λt::real. t ^ n / exp t) has_integral fact n) {0<..}"
by (intro has_integral_spike_eq) (auto simp: powr_realpow)
finally have 1: "((λt::real. t ^ n / exp t) has_integral fact n) {0<..}" .

have "(λx::real. ¦x¦ ^ n / exp x) integrable_on {0<..} ⟷
(λx::real. x ^ n / exp x) integrable_on {0<..}"
by (intro integrable_cong) auto
hence 2: "(λt::real. t ^ n / exp t) absolutely_integrable_on {0<..}"
using 1 by (simp add: absolutely_integrable_on_def power_abs has_integral_iff)

define g :: "real ⇒ real" where "g = (λx. -ln x * (n + 1))"
define g' :: "real ⇒ real" where "g' = (λx. -(n + 1) / x)"
define h :: "real ⇒ real" where "h = (λu. exp (-u / (n + 1)))"
have bij: "bij_betw g {0<..<1} {0<..}"
by (rule bij_betwI[of _ _ _ h]) (auto simp: g_def h_def mult_neg_pos)
have deriv: "(g has_real_derivative g' x) (at x within {0<..<1})"
if "x ∈ {0<..<1}" for x
unfolding g_def g'_def using that by (auto intro!: derivative_eq_intros simp: field_simps)

have "(λt::real. t ^ n / exp t) absolutely_integrable_on g  {0<..<1} ∧
integral (g  {0<..<1}) (λt::real. t ^ n / exp t) = fact n"
using 1 2 bij by (simp add: bij_betw_def has_integral_iff)
also have "?this ⟷ ((λx. ¦g' x¦ *⇩R (g x ^ n / exp (g x))) absolutely_integrable_on {0<..<1} ∧
integral {0<..<1} (λx. ¦g' x¦ *⇩R (g x ^ n / exp (g x))) = fact n)"
by (intro has_absolute_integral_change_of_variables_1' [symmetric] deriv)
(auto simp: inj_on_def g_def)
finally have "((λx. ¦g' x¦ *⇩R (g x ^ n / exp (g x))) has_integral fact n) {0<..<1}"
using eq_integralD set_lebesgue_integral_eq_integral(1) by blast
also have "?this ⟷
((λx::real. ((-1)^n*(n+1)^(n+1)) *⇩R (ln x ^ n * x ^ n)) has_integral fact n) {0<..<1}"
proof (rule has_integral_cong)
fix x :: real assume x: "x ∈ {0<..<1}"
have "¦g' x¦ *⇩R (g x ^ n / exp (g x)) =
(-1) ^ n * (real n + 1) ^ (n + 1) * ln x ^ n * (exp (ln x * (n + 1)) / x)"
also have "exp (ln x * (n + 1)) = x powr real (n + 1)"
using x by (simp add: powr_def)
also have "… / x = x ^ n"
using x by (subst powr_realpow) auto
finally show "¦g' x¦ *⇩R (g x ^ n / exp (g x)) =
((-1)^n*(n+1)^(n+1)) *⇩R (ln x ^ n * x ^ n)"
qed
also have "… ⟷ ((λx::real. ln x ^ n * x ^ n) has_integral
fact n /⇩R real_of_int ((- 1) ^ n * int ((n + 1) ^ (n + 1)))) {0<..<1}"
by (intro has_integral_cmul_iff') (auto simp del: power_Suc)
also have "fact n /⇩R real_of_int ((- 1) ^ n * int ((n + 1) ^ (n + 1))) =
(-1) ^ n * fact n / (n+1) ^ (n+1)"
by (auto simp: divide_simps)
finally show ?thesis
qed

subsection ‹Main proofs›

text ‹
We can now show the first formula: $\int_0^1 x^{-x}\,\text{d}x = \sum_{n=1}^\infty n^{-n}$
›
lemma sophomores_dream_aux1:
"summable (λk. 1 / real ((k+1)^(k+1)))"
"integral {0..1} (λx. x powr (-x)) = (∑n. 1 / (n+1)^(n+1))"
proof -
define S where "S = (λx::real. ∑k. (-(x * ln x)) ^ k / fact k)"
have S_eq: "S x = x powr (-x)" if "x > 0" for x
proof -
have "S x = exp (-x * ln x)"
by (simp add: S_def exp_def field_simps)
also have "… = x powr (-x)"
using ‹x > 0› by (simp add: powr_def)
finally show ?thesis .
qed

have cont: "continuous_on {0..1} (λx::real. ∑k<n. (-(x * ln x)) ^ k / fact k)" for n
by (intro continuous_on_sum continuous_on_divide x_log_x_continuous continuous_on_power
continuous_on_const continuous_on_minus) auto

obtain I J where IJ: "⋀n. ((λx. ∑k<n. (-(x * ln x)) ^ k / fact k) has_integral I n) {0..1}"
"(S has_integral J) {0..1}" "I ⇢ J"
using uniform_limit_integral [OF uniform_limit_sophomores_dream2 cont] by (auto simp: S_def)

note ‹(S has_integral J) {0..1}›
also have "(S has_integral J) {0..1} ⟷ (S has_integral J) {0<..<1}"
also have "… ⟷ ((λx. x powr (-x)) has_integral J) {0<..<1}"
by (intro has_integral_cong) (use S_eq in auto)
also have "… ⟷ ((λx. x powr (-x)) has_integral J) {0..1}"
finally have integral: "((λx. x powr (-x)) has_integral J) {0..1}" .

have I_eq: "I = (λn. ∑k<n. 1 / real ((k+1)^(k+1)))"
proof
fix n :: nat
have "((λx::real. ∑k<n. (-1)^k * ((x * ln x) ^ k / fact k)) has_integral
(∑k<n. (-1)^k * ((-1)^k * fact k / real ((k + 1) ^ (k + 1)) / fact k))) {0<..<1}"
by (intro has_integral_sum[OF _ has_integral_mult_right] has_integral_divide
sophomores_dream_aux_integral) auto
also have "(λx::real. ∑k<n. (-1)^k * ((x * ln x) ^ k / fact k)) =
(λx::real. ∑k<n. (-(x * ln x)) ^ k / fact k)"
also have "(∑k<n. (-1)^k * ((-1) ^ k * fact k / real ((k + 1) ^ (k + 1)) / fact k)) =
(∑k<n. 1 / real ((k + 1) ^ (k + 1)))"
by simp
also note has_integral_Icc_iff_Ioo [symmetric]
finally show "I n = (∑k<n. 1 / real ((k+1)^(k+1)))"
by (rule has_integral_unique [OF IJ(1)[of n]])
qed
hence sums: "(λk. 1 / real ((k + 1) ^ (k + 1))) sums J"
using IJ(3) I_eq by (simp add: sums_def)

from sums show "summable (λk. 1 / real ((k+1)^(k+1)))"
from integral sums show "integral {0..1} (λx. x powr (-x)) = (∑n. 1 / (n+1)^(n+1))"
qed

theorem sophomores_dream1:
"(λk::nat. norm (k powi (-k))) summable_on {1..}"
"integral {0..1} (λx. x powr (-x)) = (∑⇩∞ k∈{(1::nat)..}. k powi (-k))"
proof -
let ?I = "integral {0..1} (λx. x powr (-x))"
have "(λk::nat. norm (k powi (-k))) summable_on UNIV"
using abs_summable_sophomores_dream
by (intro norm_summable_imp_summable_on) (auto simp: power_int_minus field_simps)
thus "(λk::nat. norm (k powi (-k))) summable_on {1..}"
by (rule summable_on_subset_banach) auto

have "(λn. 1 / (n+1)^(n+1)) sums ?I"
using sophomores_dream_aux1 by (simp add: sums_iff)
moreover have "summable (λn. norm (1 / real (Suc n ^ Suc n)))"
by (subst summable_Suc_iff) (use abs_summable_sophomores_dream in ‹auto simp: field_simps›)
ultimately have "((λn::nat. 1 / (n+1)^(n+1)) has_sum ?I) UNIV"
by (intro norm_summable_imp_has_sum) auto
also have "?this ⟷ (((λn::nat. 1 / n^n) ∘ Suc) has_sum ?I) UNIV"
also have "… ⟷ ((λn::nat. 1 / n^n) has_sum ?I) (Suc  UNIV)"
by (intro has_sum_reindex [symmetric]) auto
also have "Suc  UNIV = {1..}"
using greaterThan_0 by auto
also have "((λn::nat. (1 / real (n ^ n))) has_sum ?I) {1..} ⟷
((λn::nat. n powi (-n)) has_sum ?I) {1..}"
by (intro has_sum_cong) (auto simp: power_int_minus field_simps power_minus')
finally show "integral {0..1} (λx. x powr (-x)) = (∑⇩∞k∈{(1::nat)..}. k powi (-k))"
by (auto dest!: infsumI simp: algebra_simps)
qed

text ‹
Next, we show the second formula: $\int_0^1 x^x\,\text{d}x = -\sum_{n=1}^\infty (-n)^{-n}$
›
lemma sophomores_dream_aux2:
"summable (λk. (-1) ^ k / real ((k+1)^(k+1)))"
"integral {0..1} (λx. x powr x) = (∑n. (-1)^n / (n+1)^(n+1))"
proof -
define S where "S = (λx::real. ∑k. (x * ln x) ^ k / fact k)"
have S_eq: "S x = x powr x" if "x > 0" for x
proof -
have "S x = exp (x * ln x)"
by (simp add: S_def exp_def field_simps)
also have "… = x powr x"
using ‹x > 0› by (simp add: powr_def)
finally show ?thesis .
qed

have cont: "continuous_on {0..1} (λx::real. ∑k<n. (x * ln x) ^ k / fact k)" for n
by (intro continuous_on_sum continuous_on_divide x_log_x_continuous continuous_on_power
continuous_on_const) auto

obtain I J where IJ: "⋀n. ((λx. ∑k<n. (x * ln x) ^ k / fact k) has_integral I n) {0..1}"
"(S has_integral J) {0..1}" "I ⇢ J"
using uniform_limit_integral [OF uniform_limit_sophomores_dream1 cont] by (auto simp: S_def)

note ‹(S has_integral J) {0..1}›
also have "(S has_integral J) {0..1} ⟷ (S has_integral J) {0<..<1}"
also have "… ⟷ ((λx. x powr x) has_integral J) {0<..<1}"
by (intro has_integral_cong) (use S_eq in auto)
also have "… ⟷ ((λx. x powr x) has_integral J) {0..1}"
finally have integral: "((λx. x powr x) has_integral J) {0..1}" .

have I_eq: "I = (λn. ∑k<n. (-1) ^ k / real ((k+1)^(k+1)))"
proof
fix n :: nat
have "((λx::real. ∑k<n. (x * ln x) ^ k / fact k) has_integral
(∑k<n. (-1) ^ k * fact k / real ((k + 1) ^ (k + 1)) / fact k)) {0<..<1}"
by (intro has_integral_sum has_integral_divide sophomores_dream_aux_integral) auto
also have "(∑k<n. (- 1) ^ k * fact k / real ((k + 1) ^ (k + 1)) / fact k) =
(∑k<n. (- 1) ^ k / real ((k + 1) ^ (k + 1)))"
by simp
also note has_integral_Icc_iff_Ioo [symmetric]
finally show "I n = (∑k<n. (-1) ^ k / real ((k+1)^(k+1)))"
by (rule has_integral_unique [OF IJ(1)[of n]])
qed
hence sums: "(λk. (-1) ^ k / real ((k + 1) ^ (k + 1))) sums J"
using IJ(3) I_eq by (simp add: sums_def)

from sums show "summable (λk. (-1) ^ k / real ((k+1)^(k+1)))"
from integral sums show "integral {0..1} (λx. x powr x) = (∑n. (-1)^n / (n+1)^(n+1))"
qed

theorem sophomores_dream2:
"(λk::nat. norm ((-k) powi (-k))) summable_on {1..}"
"integral {0..1} (λx. x powr x) = -(∑⇩∞ k∈{(1::nat)..}. (-k) powi (-k))"
proof -
let ?I = "integral {0..1} (λx. x powr x)"
have "(λk::nat. norm ((-k) powi (-k))) summable_on UNIV"
using abs_summable_sophomores_dream
by (intro norm_summable_imp_summable_on) (auto simp: power_int_minus field_simps)
thus "(λk::nat. norm ((-k) powi (-k))) summable_on {1..}"
by (rule summable_on_subset_banach) auto

have "(λn. (-1)^n / (n+1)^(n+1)) sums ?I"
using sophomores_dream_aux2 by (simp add: sums_iff)
moreover have "summable (λn. 1 / real (Suc n ^ Suc n))"
by (subst summable_Suc_iff) (use abs_summable_sophomores_dream in ‹auto simp: field_simps›)
hence "summable (λn. norm ((- 1) ^ n / real (Suc n ^ Suc n)))"
by simp
ultimately have "((λn::nat. (-1)^n / (n+1)^(n+1)) has_sum ?I) UNIV"
by (intro norm_summable_imp_has_sum) auto
also have "?this ⟷ (((λn::nat. -((-1)^n / n^n)) ∘ Suc) has_sum ?I) UNIV"
also have "… ⟷ ((λn::nat. -((-1)^n / n ^ n)) has_sum ?I) (Suc  UNIV)"
by (intro has_sum_reindex [symmetric]) auto
also have "Suc  UNIV = {1..}"
using greaterThan_0 by auto
also have "((λn::nat. -((- 1) ^ n / real (n ^ n))) has_sum ?I) {1..} ⟷
((λn::nat. -((-n) powi (-n))) has_sum ?I) {1..}"
by (intro has_sum_cong) (auto simp: power_int_minus field_simps power_minus')
also have "… ⟷ ((λn::nat. (-n) powi (-n)) has_sum (-?I)) {1..}"
end