{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "7f80d5e8-bab3-461d-840b-cf4ecc53a6fd",
   "metadata": {},
   "source": [
    "定理 $A_k=\\frac{\\left(\\frac12\\right)_k^3}{k!^3}$として\n",
    "$$\\frac{16}{\\pi}=\\sum_{k=0}^{\\infty }{\\frac{\\left(42\\,k+5\\right)\\,A_{k}}{2^{6\\,k}}}$$\n",
    "
\n",
    "\n",
    "証明の方針は以下の通りです。前回に得られた以下のアイゼンシュタイン級数の2つの式で$n=7$の場合を計算していきます。\n",
    "$$ \\tag{${A1}$}P\\left(e^ {- 2\\,\\pi\\,\\sqrt{n} }\\right)=\\left(1-2\\,x_{n}\\right)\\,\\sum_{k=0}^{\\infty }{\\left(3\\,k+1\\right)\\,A_{k}\\,X_{n}^{k}}$$\n",
    "$$ \\tag{${A2}$}\\frac{6\\,\\sqrt{n}}{\\pi}-P\\left(e^ {- \\frac{2\\,\\pi}{\\sqrt{n}} }\\right)=n\\,P\\left(e^ {- 2\\,\\pi\\,\\sqrt{n} }\\right) $$\n",
    "ただし以下の3つの事実を証明抜きで使うことにします。\n",
    "$$\\tag{${A3}$}7\\,P\\left(e^ {- 2\\,\\sqrt{7}\\,\\pi }\\right)-P\\left(e^ {- \\frac{2\\,\\pi}{\\sqrt{7}} }\\right)=\\frac{27\\,\\sqrt{7}\\,z_{7}^2}{8}$$\n",
    "$$1-2\\,x_{7}=\\frac{3\\,\\sqrt{7}}{8}$$\n",
    "$$X_7=\\frac{1}{2^6}$$\n",
    "ここで$z_7^2=\\sum_{k=0}^{\\infty}A_k\\,X_7^k$です。また$X_n=4\\,x_n\\,(1-x_n)$でした。上記の値でこれが成立していることは簡単に確認できるので、証明抜きで使うのは実際は2つの事実ということになります。
\n",
    "\n",
    "\n",
    "証明の流れは、まず$A2, A3$から$P\\left(e^ {- 2\\,\\pi\\,\\sqrt{n} }\\right)$を求めます。その結果と$X_7, x_7$を$A1$に代入して整理すると定理を証明することができます。\n",
    "\n",
    "\n",
    "まず前回証明した2つの式を$A1, A2$として再掲します。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "0b1a7e62-3d67-48c5-90eb-69a62afe7738",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{0}$}P\\left(e^ {- 2\\,\\pi\\,\\sqrt{n} }\\right)=\\left(1-2\\,x_{n}\\right)\\,\\sum_{k=0}^{\\infty }{\\left(3\\,k+1\\right)\\,A_{k}\\,X_{n}^{k}}\\]"
      ],
      "text/plain": [
       "                                              inf\n",
       "                                              ====\n",
       "                - 2 %pi sqrt(n)               \\                   k\n",
       "(%o0)       P(%e               ) = (1 - 2 x )  >    (3 k + 1) A  X\n",
       "                                           n  /                k  n\n",
       "                                              ====\n",
       "                                              k = 0"
      ],
      "text/x-maxima": [
       "P(%e^-(2*%pi*sqrt(n))) = (1-2*x[n])*'sum((3*k+1)*A[k]*X[n]^k,k,0,inf)"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{1}$}\\frac{6\\,\\sqrt{n}}{\\pi}-P\\left(e^ {- \\frac{2\\,\\pi}{\\sqrt{n}} }\\right)=n\\,P\\left(e^ {- 2\\,\\pi\\,\\sqrt{n} }\\right)\\]"
      ],
      "text/plain": [
       "                                 2 %pi\n",
       "                              - -------\n",
       "              6 sqrt(n)         sqrt(n)          - 2 %pi sqrt(n)\n",
       "(%o1)         --------- - P(%e         ) = n P(%e               )\n",
       "                 %pi"
      ],
      "text/x-maxima": [
       "(6*sqrt(n))/%pi-P(%e^-((2*%pi)/sqrt(n))) = n*P(%e^-(2*%pi*sqrt(n)))"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A1:P(exp(-2*%pi*sqrt(n)))=(1-2*x[n])*sum((3*k+1)*A[k]*X[n]^k,k,0,inf);\n",
    "A2:6*sqrt(n)/%pi-P(exp(-2*%pi/sqrt(n)))=n*P(exp(-2*%pi*sqrt(n)));"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "45450682-9ad2-4682-a821-f04d0bccfd5c",
   "metadata": {},
   "source": [
    "またラマヌジャンが導入した$f_n(q)$という関数を以下のように定義します。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "3a29bf0c-74a9-4815-a200-abb19473da06",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{2}$}f_{n}(q):=n\\,P\\left(q^{2\\,n}\\right)-P\\left(q^2\\right)\\]"
      ],
      "text/plain": [
       "                                        2 n       2\n",
       "(%o2)                     f (q) := n P(q   ) - P(q )\n",
       "                           n"
      ],
      "text/x-maxima": [
       "f[n](q):=n*P(q^(2*n))-P(q^2)"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "f[n](q):=n*P(q^(2*n))-P(q^2);"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "aeb24a0a-e879-4921-a492-9972e245ee6a",
   "metadata": {},
   "source": [
    "証明抜きで使う最初の事実は次のように表すことができます。この式を$A3$とします。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "9e7edc5c-3549-4599-a041-755f4b645392",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{3}$}7\\,P\\left(e^ {- 2\\,\\sqrt{7}\\,\\pi }\\right)-P\\left(e^ {- \\frac{2\\,\\pi}{\\sqrt{7}} }\\right)=\\frac{27\\,\\sqrt{7}\\,z_{7}^2}{8}\\]"
      ],
      "text/plain": [
       "                                            2 %pi                 2\n",
       "                                         - -------    27 sqrt(7) z\n",
       "                  - 2 sqrt(7) %pi          sqrt(7)                7\n",
       "(%o3)       7 P(%e               ) - P(%e         ) = -------------\n",
       "                                                            8"
      ],
      "text/x-maxima": [
       "7*P(%e^-(2*sqrt(7)*%pi))-P(%e^-((2*%pi)/sqrt(7))) = (27*sqrt(7)*z[7]^2)/8"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A3:f[7](exp(-%pi/sqrt(7)))=27*sqrt(7)/8*z[7]^2;"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "df937c9e-561c-4c4c-b30d-ef5852f0f618",
   "metadata": {},
   "source": [
    "$A2$で$n=7$の場合を計算して結果を$A4$とします。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "1153fffc-4475-4cfb-8f9f-ae86d9c1a68d",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{4}$}\\frac{6\\,\\sqrt{7}}{\\pi}-P\\left(e^ {- \\frac{2\\,\\pi}{\\sqrt{7}} }\\right)=7\\,P\\left(e^ {- 2\\,\\sqrt{7}\\,\\pi }\\right)\\]"
      ],
      "text/plain": [
       "                                 2 %pi\n",
       "                              - -------\n",
       "              6 sqrt(7)         sqrt(7)          - 2 sqrt(7) %pi\n",
       "(%o4)         --------- - P(%e         ) = 7 P(%e               )\n",
       "                 %pi"
      ],
      "text/x-maxima": [
       "(6*sqrt(7))/%pi-P(%e^-((2*%pi)/sqrt(7))) = 7*P(%e^-(2*sqrt(7)*%pi))"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A4:A2,n:7;"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b9e26580-990e-4e27-877c-2ab1f6bb62c1",
   "metadata": {},
   "source": [
    "$P\\left(e^ {- \\frac{2\\,\\pi}{\\sqrt{7}} }\\right), 7\\,P\\left(e^ {- 2\\,\\sqrt{7}\\,\\pi }\\right)$を変数と見立てて$A3, A4$を連立1次方程式として解きます。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "b4bccc9a-2594-4303-a280-1a92a5422725",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{5}$}\\left[ \\left[ P\\left(e^ {- 2\\,\\sqrt{7}\\,\\pi }\\right)=\\frac{27\\,\\sqrt{7}\\,\\pi\\,z_{7}^2+48\\,\\sqrt{7}}{112\\,\\pi} , P\\left(e^ {- \\frac{2\\,\\pi}{\\sqrt{7}} }\\right)=-\\frac{27\\,\\sqrt{7}\\,\\pi\\,z_{7}^2-48\\,\\sqrt{7}}{16\\,\\pi} \\right]  \\right] \\]"
      ],
      "text/plain": [
       "                                               2\n",
       "                               27 sqrt(7) %pi z  + 48 sqrt(7)\n",
       "            - 2 sqrt(7) %pi                    7\n",
       "(%o5) [[P(%e               ) = ------------------------------, \n",
       "                                          112 %pi\n",
       "                                   2 %pi                       2\n",
       "                                - -------      27 sqrt(7) %pi z  - 48 sqrt(7)\n",
       "                                  sqrt(7)                      7\n",
       "                            P(%e         ) = - ------------------------------]]\n",
       "                                                           16 %pi"
      ],
      "text/x-maxima": [
       "[[P(%e^-(2*sqrt(7)*%pi)) = (27*sqrt(7)*%pi*z[7]^2+48*sqrt(7))/(112*%pi),\n",
       "  P(%e^-((2*%pi)/sqrt(7))) = -(27*sqrt(7)*%pi*z[7]^2-48*sqrt(7))/(16*%pi)]]"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "SOL:solve([A3,A4],[P(exp(-2*sqrt(7)*%pi)), P(exp(-2/sqrt(7)*%pi))]);"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "4bdffc59-4fd9-4041-97f4-75e9e6445910",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{6}$}P\\left(e^ {- 2\\,\\sqrt{7}\\,\\pi }\\right)=\\frac{27\\,\\sqrt{7}\\,\\pi\\,z_{7}^2+48\\,\\sqrt{7}}{112\\,\\pi}\\]"
      ],
      "text/plain": [
       "                                                    2\n",
       "                                    27 sqrt(7) %pi z  + 48 sqrt(7)\n",
       "                 - 2 sqrt(7) %pi                    7\n",
       "(%o6)        P(%e               ) = ------------------------------\n",
       "                                               112 %pi"
      ],
      "text/x-maxima": [
       "P(%e^-(2*sqrt(7)*%pi)) = (27*sqrt(7)*%pi*z[7]^2+48*sqrt(7))/(112*%pi)"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A5:SOL[1][1];"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4b992916-6bb5-402f-b43c-323169154c78",
   "metadata": {},
   "source": [
    "$A1$で$n=7$とした式を計算し、上記の結果を代入します。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "11b0e65f-109a-4dc3-88b9-e689aec03746",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{7}$}P\\left(e^ {- 2\\,\\sqrt{7}\\,\\pi }\\right)=\\left(1-2\\,x_{7}\\right)\\,\\sum_{k=0}^{\\infty }{X_{7}^{k}\\,\\left(3\\,k+1\\right)\\,A_{k}}\\]"
      ],
      "text/plain": [
       "                                              inf\n",
       "                                              ====\n",
       "                - 2 sqrt(7) %pi               \\      k\n",
       "(%o7)       P(%e               ) = (1 - 2 x )  >    X  (3 k + 1) A\n",
       "                                           7  /      7            k\n",
       "                                              ====\n",
       "                                              k = 0"
      ],
      "text/x-maxima": [
       "P(%e^-(2*sqrt(7)*%pi)) = (1-2*x[7])*'sum(X[7]^k*(3*k+1)*A[k],k,0,inf)"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A6:A1,n:7;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "id": "333f1a33-8891-4d2c-a591-112b4cdebc6a",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{27}$}\\frac{27\\,\\sqrt{7}\\,\\pi\\,z_{7}^2+48\\,\\sqrt{7}}{112\\,\\pi}=\\left(1-2\\,x_{7}\\right)\\,\\sum_{k=0}^{\\infty }{X_{7}^{k}\\,\\left(3\\,k+1\\right)\\,A_{k}}\\]"
      ],
      "text/plain": [
       "                       2                           inf\n",
       "       27 sqrt(7) %pi z  + 48 sqrt(7)              ====\n",
       "                       7                           \\      k\n",
       "(%o27) ------------------------------ = (1 - 2 x )  >    X  (3 k + 1) A\n",
       "                  112 %pi                       7  /      7            k\n",
       "                                                   ====\n",
       "                                                   k = 0"
      ],
      "text/x-maxima": [
       "(27*sqrt(7)*%pi*z[7]^2+48*sqrt(7))/(112*%pi)\n",
       "  = (1-2*x[7])*'sum(X[7]^k*(3*k+1)*A[k],k,0,inf)"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A7:A6,A5;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "id": "9b31722a-c69b-4082-8cd2-977f9471e670",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{28}$}\\frac{27\\,z_{7}^2}{16\\,\\sqrt{7}}+\\frac{3}{\\sqrt{7}\\,\\pi}=\\sum_{k=0}^{\\infty }{\\left(3\\,X_{7}^{k}\\,k\\,A_{k}+X_{7}^{k}\\,A_{k}\\right)}-2\\,x_{7}\\,\\sum_{k=0}^{\\infty }{\\left(3\\,X_{7}^{k}\\,k\\,A_{k}+X_{7}^{k}\\,A_{k}\\right)}\\]"
      ],
      "text/plain": [
       "             2                    inf\n",
       "         27 z                     ====\n",
       "             7           3        \\         k         k\n",
       "(%o28) ---------- + ----------- =  >    (3 X  k A  + X  A )\n",
       "       16 sqrt(7)   sqrt(7) %pi   /         7    k    7  k\n",
       "                                  ====\n",
       "                                  k = 0\n",
       "                                                      inf\n",
       "                                                      ====\n",
       "                                                      \\         k         k\n",
       "                                               - 2 x   >    (3 X  k A  + X  A )\n",
       "                                                    7 /         7    k    7  k\n",
       "                                                      ====\n",
       "                                                      k = 0"
      ],
      "text/x-maxima": [
       "(27*z[7]^2)/(16*sqrt(7))+3/(sqrt(7)*%pi)\n",
       "  = 'sum(3*X[7]^k*k*A[k]+X[7]^k*A[k],k,0,inf)\n",
       "  -2*x[7]*'sum(3*X[7]^k*k*A[k]+X[7]^k*A[k],k,0,inf)"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "%,expand;"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "50b599b8-6185-44ca-8f5a-89909693cfbb",
   "metadata": {},
   "source": [
    "$z_7^2$にその級数展開を代入します。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "id": "85d8d509-614a-45d4-bd05-c13e6129459b",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{29}$}\\frac{27\\,\\sum_{k=0}^{\\infty }{X_{7}^{k}\\,A_{k}}}{16\\,\\sqrt{7}}+\\frac{3}{\\sqrt{7}\\,\\pi}=\\sum_{k=0}^{\\infty }{\\left(3\\,X_{7}^{k}\\,k\\,A_{k}+X_{7}^{k}\\,A_{k}\\right)}-2\\,x_{7}\\,\\sum_{k=0}^{\\infty }{\\left(3\\,X_{7}^{k}\\,k\\,A_{k}+X_{7}^{k}\\,A_{k}\\right)}\\]"
      ],
      "text/plain": [
       "          inf\n",
       "          ====\n",
       "          \\      k\n",
       "       27  >    X  A\n",
       "          /      7  k                 inf\n",
       "          ====                        ====\n",
       "          k = 0              3        \\         k         k\n",
       "(%o29) -------------- + ----------- =  >    (3 X  k A  + X  A )\n",
       "         16 sqrt(7)     sqrt(7) %pi   /         7    k    7  k\n",
       "                                      ====\n",
       "                                      k = 0\n",
       "                                                      inf\n",
       "                                                      ====\n",
       "                                                      \\         k         k\n",
       "                                               - 2 x   >    (3 X  k A  + X  A )\n",
       "                                                    7 /         7    k    7  k\n",
       "                                                      ====\n",
       "                                                      k = 0"
      ],
      "text/x-maxima": [
       "(27*'sum(X[7]^k*A[k],k,0,inf))/(16*sqrt(7))+3/(sqrt(7)*%pi)\n",
       "  = 'sum(3*X[7]^k*k*A[k]+X[7]^k*A[k],k,0,inf)\n",
       "  -2*x[7]*'sum(3*X[7]^k*k*A[k]+X[7]^k*A[k],k,0,inf)"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "%,z[7]^2=sum(A[k]*X[7]^k,k,0,inf);"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "id": "a0a921c4-5eac-4300-ac7b-a0568f406502",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{30}$}27\\,\\sum_{k=0}^{\\infty }{X_{7}^{k}\\,A_{k}}+\\frac{48}{\\pi}=16\\,\\sqrt{7}\\,\\sum_{k=0}^{\\infty }{\\left(3\\,X_{7}^{k}\\,k\\,A_{k}+X_{7}^{k}\\,A_{k}\\right)}-32\\,\\sqrt{7}\\,x_{7}\\,\\sum_{k=0}^{\\infty }{\\left(3\\,X_{7}^{k}\\,k\\,A_{k}+X_{7}^{k}\\,A_{k}\\right)}\\]"
      ],
      "text/plain": [
       "          inf                            inf\n",
       "          ====                           ====\n",
       "          \\      k      48               \\         k         k\n",
       "(%o30) 27  >    X  A  + --- = 16 sqrt(7)  >    (3 X  k A  + X  A )\n",
       "          /      7  k   %pi              /         7    k    7  k\n",
       "          ====                           ====\n",
       "          k = 0                          k = 0\n",
       "                                                      inf\n",
       "                                                      ====\n",
       "                                                      \\         k         k\n",
       "                                      - 32 sqrt(7) x   >    (3 X  k A  + X  A )\n",
       "                                                    7 /         7    k    7  k\n",
       "                                                      ====\n",
       "                                                      k = 0"
      ],
      "text/x-maxima": [
       "27*'sum(X[7]^k*A[k],k,0,inf)+48/%pi = 16*sqrt(7)\n",
       "                                        *'sum(3*X[7]^k*k*A[k]+X[7]^k*A[k],k,0,\n",
       "                                              inf)\n",
       "                                    -32*sqrt(7)*x[7]\n",
       "                                       *'sum(3*X[7]^k*k*A[k]+X[7]^k*A[k],k,0,\n",
       "                                             inf)"
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "%*16*sqrt(7),expand;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "id": "742e9365-6699-482c-8ef7-f22360c673d6",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{31}$}\\frac{48}{\\pi}=-32\\,\\sqrt{7}\\,x_{7}\\,\\sum_{k=0}^{\\infty }{\\left(3\\,X_{7}^{k}\\,k\\,A_{k}+X_{7}^{k}\\,A_{k}\\right)}+16\\,\\sqrt{7}\\,\\sum_{k=0}^{\\infty }{\\left(3\\,X_{7}^{k}\\,k\\,A_{k}+X_{7}^{k}\\,A_{k}\\right)}-27\\,\\sum_{k=0}^{\\infty }{X_{7}^{k}\\,A_{k}}\\]"
      ],
      "text/plain": [
       "                              inf\n",
       "                              ====\n",
       "       48                     \\         k         k\n",
       "(%o31) --- = (- 32 sqrt(7) x   >    (3 X  k A  + X  A ))\n",
       "       %pi                  7 /         7    k    7  k\n",
       "                              ====\n",
       "                              k = 0\n",
       "                                     inf                            inf\n",
       "                                     ====                           ====\n",
       "                                     \\         k         k          \\      k\n",
       "                        + 16 sqrt(7)  >    (3 X  k A  + X  A ) - 27  >    X  A\n",
       "                                     /         7    k    7  k       /      7  k\n",
       "                                     ====                           ====\n",
       "                                     k = 0                          k = 0"
      ],
      "text/x-maxima": [
       "48/%pi = (-32*sqrt(7)*x[7]*'sum(3*X[7]^k*k*A[k]+X[7]^k*A[k],k,0,inf))\n",
       "       +16*sqrt(7)*'sum(3*X[7]^k*k*A[k]+X[7]^k*A[k],k,0,inf)\n",
       "       -27*'sum(X[7]^k*A[k],k,0,inf)"
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A8:%-first(lhs(%));"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ef6b85ec-ee57-46ca-8d35-7c6ebfdea531",
   "metadata": {},
   "source": [
    "級数の項を全て右辺に集めて整理すると目的の式の片鱗が見えてきます。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "id": "e6628a1f-2792-4a95-9755-a2624c092fb3",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{32}$}\\frac{48}{\\pi}=-\\sum_{k=0}^{\\infty }{X_{7}^{k}\\,\\left(\\left(96\\,\\sqrt{7}\\,x_{7}-48\\,\\sqrt{7}\\right)\\,k+32\\,\\sqrt{7}\\,x_{7}-16\\,\\sqrt{7}+27\\right)\\,A_{k}}\\]"
      ],
      "text/plain": [
       "               inf\n",
       "               ====\n",
       "       48      \\      k\n",
       "(%o32) --- = -  >    X  ((96 sqrt(7) x  - 48 sqrt(7)) k + 32 sqrt(7) x\n",
       "       %pi     /      7               7                               7\n",
       "               ====\n",
       "               k = 0\n",
       "                                                         - 16 sqrt(7) + 27) A\n",
       "                                                                             k"
      ],
      "text/x-maxima": [
       "48/%pi = -'sum(X[7]^k*((96*sqrt(7)*x[7]-48*sqrt(7))*k\n",
       "                      +32*sqrt(7)*x[7]-16*sqrt(7)+27)*A[k],k,0,inf)"
      ]
     },
     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A9:factor(sumcontract(intosum(A8)));"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6327ade6-1787-4ec9-801d-e90ca2a89f53",
   "metadata": {},
   "source": [
    "$X_7=\\frac{1}{2^6}$を代入します。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "id": "aa302a9a-cc19-4222-8734-532c1ca7a2ee",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{34}$}\\frac{48}{\\pi}=-\\sum_{k=0}^{\\infty }{\\frac{\\left(\\left(96\\,\\sqrt{7}\\,x_{7}-48\\,\\sqrt{7}\\right)\\,k+32\\,\\sqrt{7}\\,x_{7}-16\\,\\sqrt{7}+27\\right)\\,A_{k}}{64^{k}}}\\]"
      ],
      "text/plain": [
       "       48\n",
       "(%o34) --- = \n",
       "       %pi\n",
       "    inf\n",
       "    ====  ((96 sqrt(7) x  - 48 sqrt(7)) k + 32 sqrt(7) x  - 16 sqrt(7) + 27) A\n",
       "    \\                   7                               7                     k\n",
       "  -  >    ---------------------------------------------------------------------\n",
       "    /                                        k\n",
       "    ====                                   64\n",
       "    k = 0"
      ],
      "text/x-maxima": [
       "48/%pi = -'sum((((96*sqrt(7)*x[7]-48*sqrt(7))*k+32*sqrt(7)*x[7]-16*sqrt(7)+27)\n",
       "                *A[k])\n",
       "                /64^k,k,0,inf)"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A10:A9, X[7]=1/2^6;"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e02cd64e-2971-4044-a0e2-c7873665849b",
   "metadata": {},
   "source": [
    "事実その2の式を$x_7$について解きます。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "fecdcb33-9da8-47bf-a7bc-647eace130df",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{16}$}1-2\\,x_{7}=\\frac{3\\,\\sqrt{7}}{8}\\]"
      ],
      "text/plain": [
       "                                        3 sqrt(7)\n",
       "(%o16)                       1 - 2 x  = ---------\n",
       "                                    7       8"
      ],
      "text/x-maxima": [
       "1-2*x[7] = (3*sqrt(7))/8"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "1-2*x[7]=3*sqrt(7)/8;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "c7107d3d-66ff-4a78-9857-46ed7569c20c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{17}$}\\left[ x_{7}=-\\frac{3\\,\\sqrt{7}-8}{16} \\right] \\]"
      ],
      "text/plain": [
       "                                    3 sqrt(7) - 8\n",
       "(%o17)                      [x  = - -------------]\n",
       "                              7          16"
      ],
      "text/x-maxima": [
       "[x[7] = -(3*sqrt(7)-8)/16]"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "SOL2:solve(%,x[7]);"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e050fcc2-d15a-43db-9d1a-55fe6fb1f110",
   "metadata": {},
   "source": [
    "結果を$A10$に代入します。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "f6b132c9-943f-4011-a954-2e73fc10d1e8",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{18}$}\\frac{48}{\\pi}=-\\sum_{k=0}^{\\infty }{\\frac{\\left(\\left(-6\\,\\sqrt{7}\\,\\left(3\\,\\sqrt{7}-8\\right)-48\\,\\sqrt{7}\\right)\\,k-2\\,\\sqrt{7}\\,\\left(3\\,\\sqrt{7}-8\\right)-16\\,\\sqrt{7}+27\\right)\\,A_{k}}{64^{k}}}\\]"
      ],
      "text/plain": [
       "               inf\n",
       "               ====\n",
       "       48      \\\n",
       "(%o18) --- = -  >    ((((- 6 sqrt(7) (3 sqrt(7) - 8)) - 48 sqrt(7)) k\n",
       "       %pi     /\n",
       "               ====\n",
       "               k = 0\n",
       "                                                                             k\n",
       "                        - 2 sqrt(7) (3 sqrt(7) - 8) - 16 sqrt(7) + 27) A )/64\n",
       "                                                                        k"
      ],
      "text/x-maxima": [
       "48/%pi = -'sum(((((-6*sqrt(7)*(3*sqrt(7)-8))-48*sqrt(7))*k\n",
       "                -2*sqrt(7)*(3*sqrt(7)-8)-16*sqrt(7)+27)\n",
       "                *A[k])\n",
       "                /64^k,k,0,inf)"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A11:A10,SOL2;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "141050d6-b3b6-4486-a845-147bbc2c46e1",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{19}$}\\frac{48}{\\pi}=\\sum_{k=0}^{\\infty }{\\frac{\\left(126\\,k+15\\right)\\,A_{k}}{2^{6\\,k}}}\\]"
      ],
      "text/plain": [
       "                                inf\n",
       "                                ====  (126 k + 15) A\n",
       "                          48    \\                   k\n",
       "(%o19)                    --- =  >    ---------------\n",
       "                          %pi   /           6 k\n",
       "                                ====       2\n",
       "                                k = 0"
      ],
      "text/x-maxima": [
       "48/%pi = 'sum(((126*k+15)*A[k])/2^(6*k),k,0,inf)"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A12:radcan(A11);"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "32526f18-c336-4703-95d7-1da53e1f8233",
   "metadata": {},
   "source": [
    "整理して両辺を$3$で割れば証明は終了します。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "8477f513-01af-4abf-8b5e-7be525fcdceb",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\[\\tag{${\\it \\%o}_{20}$}\\frac{16}{\\pi}=\\sum_{k=0}^{\\infty }{\\frac{\\left(42\\,k+5\\right)\\,A_{k}}{2^{6\\,k}}}\\]"
      ],
      "text/plain": [
       "                                 inf\n",
       "                                 ====  (42 k + 5) A\n",
       "                           16    \\                 k\n",
       "(%o20)                     --- =  >    -------------\n",
       "                           %pi   /          6 k\n",
       "                                 ====      2\n",
       "                                 k = 0"
      ],
      "text/x-maxima": [
       "16/%pi = 'sum(((42*k+5)*A[k])/2^(6*k),k,0,inf)"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A13:ratsimp(intosum(A12/3));"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Maxima",
   "language": "maxima",
   "name": "maxima"
  },
  "language_info": {
   "codemirror_mode": "maxima",
   "file_extension": ".mac",
   "mimetype": "text/x-maxima",
   "name": "maxima",
   "pygments_lexer": "maxima",
   "version": "5.44.0"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}