つまりAtCoder社はこの記事とは異なる仮定をおいているはずであることの証明。

この記事はAtCoderのレート計算式の子記事であり、該当の記事を事前に読んでおかないと意味が分からないので注意。

以下の仮定をおく。

コンテストのRatedな参加人数は中心極限定理を適用できる程度に大きい。
コンテストのRatedな参加者はそれぞれ、神のみが知っているただ一つの実数である「実力」という値を持つ。
コンテストのRatedな参加者が持つ実力の分布はある連続確率分布に従う。
コンテストでは同着順位は発生しない。
実力差を$x$とするとき、実力が高い側が$\frac{1}{1 + 6^{-\frac{x}{400}}}$の確率で勝つ。（勝つとはコンテストで高い順位になること）
あるRatedな参加者に勝てる確率と、別のあるRatedな参加者に勝てる確率は独立である。
内部パフォーマンスとパフォーマンスを整数に丸めず実数のまま扱う。

このとき、以下の命題を証明する。

命題「どのような状況、どのようなユーザーであっても、99.9%以上の確率で、実力の値はレート（第三段階）の値以上である」は偽である。

証明の方針

コンテストのRatedな参加者が持つ実力の分布としてどのような確率分布を仮定したとしても、十分に実力の高いユーザーならば、AGCに一回だけ参加した直後において、レート（第三段階）の値として実力より高い値を出せる確率を50%より大きくできることを証明する。

証明の直感的な理解

あまりにも強いユーザーは実力よりも高いレートが出がちになる。（本当に？）

命題の定式化

命題「どのようなユーザーであっても、AGCに一回だけ参加した直後において、99.9%以上の確率で、実力の値はレート（第三段階）の値以上である」を論理式の形に直す。

確率変数$X$が連続確率分布に従うとき、$X$の確率密度関数を$f_X(x)$と書くことにする。
確率変数$X$が離散確率分布に従うとき、$X$の確率質量関数を$f_X(x)$と書くことにする。
確率変数$X$の累積分布関数を$F_X(x)$と書くことにする。
$\int_{-\infty}^x F_X(y) \mathrm{d}y$を$\mathbf{F}_X(x)$と書くことにする。
$\int_{-\infty}^x \mathbf{F}_X(y) \mathrm{d}y$を$\mathbb{F}_X(x)$と書くことにする。
確率変数$X$の期待値を$E(X)$と書くことにする。
確率変数$X$の分散を$V(X)$と書くことにする。
事象$E$の発生確率を$\mathrm{Pr}(E)$と書くことにする。

AtCoderに登録した直後の、実力が$\theta$のユーザー$\Theta$がAGCに一回だけ参加したとする。
このときのコンテストのRatedな参加人数を$n + 1$と書くことにする。
$\Theta$はコンテストの$n + 1$人目のRatedな参加者であるとする。
$i$人目のRatedな参加者が持つ実力を確率変数$A_i$と書くことにする。
$i$人目のRatedな参加者に$\Theta$が勝てる確率を確率変数${}_\theta W'_i$と書くことにする。
$i$人目のRatedな参加者に$\Theta$が勝てたなら1、勝てなかったなら0となる確率変数を${}_\theta W_i$と書くことにする。
$\Theta$の内部パフォーマンスを確率変数${}_\theta P'$と書くことにする。
$\Theta$の内部レートを確率変数${}_\theta R'$と書くことにする。
$\Theta$のパフォーマンスを確率変数${}_\theta P$と書くことにする。
$\Theta$のレート（第二段階）を確率変数${}_\theta R_2$と書くことにする。
$\Theta$のレート（第三段階）を確率変数${}_\theta R_3$と書くことにする。

連続一様分布$U(0, 1)$に従う、お互いどの確率変数とも独立な$n$個の確率変数列を$U_1, U_2, \ldots, U_n$と書くことにする。
${}_\eta W_i - {}_\tau W'_i$を${}^\eta_\tau D_i$と書くことにする。
$\sum_{i=1}^n {}^\eta_\tau D_i$を${}^\eta_\tau \hat{D}_n$と書くことにする。

偽であることを証明する命題は、

\forall \theta. \mathrm{Pr}\left(\theta \geq {}_\theta R_3\right) \geq 0.999

証明

第一部: ${}_\eta W'_i$と$F_{{}_\eta W'_i}(x)$と$f_{{}_\eta W'_i}(x)$と$\mathbf{F}_{{}_\eta W'_i}(x)$と$\mathbb{F}_{{}_\eta W'_i}(x)$の導出
第二部: $F_{{}_\eta W_i^{\prime 2}}(x)$と$f_{{}_\eta W_i^{\prime 2}}(x)$の導出
第三部: $E({}_\eta W'_i)$と$E({}_\eta W_i^{\prime 2})$の導出
第四部: ${}_\eta W_i$と$f_{{}_\eta W_i}(x)$の導出
第五部: $E({}_\eta W_i)$と$E({}_\eta W_i^2)$の導出
第六部: $E\left({}_\eta W_i \cdot {}_\tau W'_i\right)$の導出
第七部: $E\left({}^\eta_\tau D_i\right)$と$E\left({}^\eta_\tau D_i^2\right)$と$V\left({}^\eta_\tau D_i\right)$の導出
第八部: $F_{{}^\eta_\tau \hat{D}_n}(x)$の導出
第九部: $F_{{}_\theta P'}(x)$の導出
第十部: $\mathrm{Pr}\left(\theta \geq {}_\theta R_3\right)$の導出
第十一部: $\forall \theta. \mathrm{Pr}\left(\theta \geq {}_\theta R_3\right) \geq 0.999$の反証

第一部

${}_\eta W'_i$と$F_{{}_\eta W'_i}(x)$と$f_{{}_\eta W'_i}(x)$と$\mathbf{F}_{{}_\eta W'_i}(x)$と$\mathbb{F}_{{}_\eta W'_i}(x)$を導出する。

$1 \leq i \leq n$に対して、

\begin{align*}
{}_\eta W'_i =& \frac{1}{1 + 6^\frac{A_i - \eta}{400}}\\
\\
\\
F_{{}_\eta W'_i}(x) =& \mathrm{Pr}({}_\eta W'_i \leq x)\\
=& \mathrm{Pr}\left(\frac{1}{1 + 6^\frac{A_i - \eta}{400}} \leq x\right)\\
=& \left\{\begin{array}{ll}
0 & \text{if } x \leq 0\\
\mathrm{Pr}\left(A_i \geq 400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) & \text{if }0 < x < 1\\
1 & \text{if } 1 \leq x\\
\end{array}\right.\\
=& \left\{\begin{array}{ll}
0 & \text{if } x \leq 0\\
1 - \mathrm{Pr}\left(A_i \leq 400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) & \text{if }0 < x < 1\\
1 & \text{if } 1 \leq x\\
\end{array}\right.\\
=& \left\{\begin{array}{ll}
0 & \text{if } x \leq 0\\
1 - F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) & \text{if }0 < x < 1\\
1 & \text{if } 1 \leq x\\
\end{array}\right.\\
\\
\\
f_{{}_\eta W'_i}(x) =& \frac{d}{\mathrm{d}x} F_{{}_\eta W'_i}(x)\\
=& \left\{\begin{array}{ll}
\frac{d}{\mathrm{d}x} \left(1 - F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right)\right) & \text{if } 0 < x < 1\\
0 & \text{otherwise.}\\
\end{array}\right.\\
=& \left\{\begin{array}{ll}
\frac{400}{\log 6 \cdot x(1 - x)} f_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) & \text{if } 0 < x < 1\\
0 & \text{otherwise.}\\
\end{array}\right.\\
\\
\\
\mathbf{F}_{{}_\eta W'_i}(x) =& \int_{-\infty}^x F_{{}_\eta W'_i}(y) \mathrm{d}y\\
=& \left\{\begin{array}{ll}
0 & \text{if } x \leq 0\\
\int_0^x F_{{}_\eta W'_i}(y) \mathrm{d}y & \text{if }0 < x < 1\\
\int_0^1 F_{{}_\eta W'_i}(y) \mathrm{d}y + x - 1 & \text{if } 1 \leq x\\
\end{array}\right.\\
=& \left\{\begin{array}{ll}
0 & \text{if } x \leq 0\\
x - \int_0^x F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \eta\right) \mathrm{d}y & \text{if }0 < x < 1\\
x - \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \eta\right) \mathrm{d}y & \text{if } 1 \leq x\\
\end{array}\right.\\
\\
\\
\mathbb{F}_{{}_\eta W'_i}(x) =& \int_{-\infty}^x \mathbf{F}_{{}_\eta W'_i}(y) \mathrm{d}y\\
=& \left\{\begin{array}{ll}
0 & \text{if } x \leq 0\\
\int_0^x \mathbf{F}_{{}_\eta W'_i}(y) \mathrm{d}y & \text{if }0 < x < 1\\
\int_0^1 \mathbf{F}_{{}_\eta W'_i}(y) \mathrm{d}y + \int_1^x \mathbf{F}_{{}_\eta W'_i}(y) \mathrm{d}y & \text{if } 1 \leq x\\
\end{array}\right.\\
=& \left\{\begin{array}{ll}
0 & \text{if } x \leq 0\\
\frac{1}{2} x^2 - \int_0^x \int_0^y F_{A_i}\left(400 \log_6 \left(\frac{1}{z} - 1\right) + \eta\right) \mathrm{d}z \mathrm{d}y & \text{if }0 < x < 1\\
\frac{1}{2} x^2 - \int_0^1 \int_0^y F_{A_i}\left(400 \log_6 \left(\frac{1}{z} - 1\right) + \eta\right) \mathrm{d}z \mathrm{d}y - \left(x - 1\right) \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \eta\right) \mathrm{d}y & \text{if } 1 \leq x\\
\end{array}\right.\\
\end{align*}

第二部

$F_{{}_\eta W_i^{\prime 2}}(x)$と$f_{{}_\eta W_i^{\prime 2}}(x)$を導出する。

$1 \leq i \leq n$に対して、

\begin{align*}
F_{{}_\eta W_i^{\prime 2}}(x) =& \mathrm{Pr}({}_\eta W_i^{\prime 2} \leq x)\\
=& \left\{\begin{array}{ll}
0 & \text{if } x \leq 0\\
\mathrm{Pr}({}_\eta W'_i \leq \sqrt{x}) & \text{if } 0 < x < 1\\
1 & \text{if } 1 \leq x\\
\end{array}\right.\\
=& \left\{\begin{array}{ll}
0 & \text{if } x \leq 0\\
F_{{}_\eta W'_i}(\sqrt{x}) & \text{if } 0 < x < 1\\
1 & \text{if } 1 \leq x\\
\end{array}\right.\\
=& \left\{\begin{array}{ll}
0 & \text{if } x \leq 0\\
1 - F_{A_i}\left(400 \log_6 \left(\frac{1}{\sqrt{x}} - 1\right) + \eta\right) & \text{if } 0 < x < 1\\
1 & \text{if } 1 \leq x\\
\end{array}\right.\\
\\
\\
f_{{}_\eta W_i^{\prime 2}}(x) =& \left\{\begin{array}{ll}
\frac{f_{{}_\eta W'_i}(\sqrt{x})}{2\sqrt{x}} & \text{if } 0 < x < 1\\
0 & \text{otherwise.}\\
\end{array}\right.\\
=& \left\{\begin{array}{ll}
\frac{400 f_{A_i}\left(400 \log_6 \left(\frac{1}{\sqrt{x}} - 1\right) + \eta\right)}{2 \log 6 \cdot x\sqrt{x}(1 - x)} & \text{if } 0 < x < 1\\
0 & \text{otherwise.}\\
\end{array}\right.\\
\end{align*}

第三部

$E({}_\eta W'_i)$と$E({}_\eta W_i^{\prime 2})$を導出する。

$1 \leq i \leq n$に対して、

\begin{align*}
E\left({}_\eta W'_i\right) =& \int_{-\infty}^\infty x \cdot f_{{}_\eta W'_i}(x) \mathrm{d}x\\
=& \int_0^1 x \cdot f_{{}_\eta W'_i}(x) \mathrm{d}x\\
=& \left[x \cdot F_{{}_\eta W'_i}(x)\right]_{x=0}^{x=1} - \int_0^1 F_{{}_\eta W'_i}(x) \mathrm{d}x\\
=& 1 - \mathbf{F}_{{}_\eta W'_i}(1)\\
=& \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) \mathrm{d}x\\
\\
\\
E({}_\eta W_i^{\prime 2}) =& \int_{-\infty}^\infty x \cdot f_{{}_\eta W_i^{\prime 2}}(x) \mathrm{d}x\\
=& \int_0^1 x \cdot f_{{}_\eta W_i^{\prime 2}}(x) \mathrm{d}x\\
=& \left[x \cdot F_{{}_\eta W_i^{\prime 2}}(x)\right]_{x=0}^{x=1} - \int_0^1 F_{{}_\eta W_i^{\prime 2}}(x) \mathrm{d}x\\
=& \left[x \cdot F_{{}_\eta W'_i}(\sqrt{x})\right]_{x=0}^{x=1} - \int_0^1 F_{{}_\eta W'_i}(\sqrt{x}) \mathrm{d}x\\
=& 1 - \int_0^1 F_{{}_\eta W'_i}(\sqrt{x}) \mathrm{d}x\\
=& 1 - \int_0^1 F_{{}_\eta W'_i}(\sqrt{x}) \frac{\mathrm{d}x}{\mathrm{d}\sqrt{x}} \mathrm{d}\sqrt{x}\\
=& 1 - 2 \int_0^1 F_{{}_\eta W'_i}(\sqrt{x}) \sqrt{x} \mathrm{d}\sqrt{x}\\
=& 1 - 2 \int_0^1 F_{{}_\eta W'_i}(x) x \mathrm{d}x\\
=& 1 - 2 \left(\left[x \cdot \mathbf{F}_{{}_\eta W'_i}(x)\right]_{x=0}^{x=1} - \int_0^1 \mathbf{F}_{{}_\eta W'_i}(x) \mathrm{d}x\right)\\
=& 1 - 2 \left(\mathbf{F}_{{}_\eta W'_i}(1) - \mathbb{F}_{{}_\eta W'_i}(1)\right)\\
=& 1 - 2 \mathbf{F}_{{}_\eta W'_i}(1) + 2 \mathbb{F}_{{}_\eta W'_i}(1)\\
=& 2 \left(\int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) \mathrm{d}x - \int_0^1 \int_0^x F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \eta\right) \mathrm{d}y \mathrm{d}x\right)\\
\end{align*}

第四部

${}_\eta W_i$と$f_{{}_\eta W_i}(x)$を導出する。

$1 \leq i \leq n$に対して、

\begin{align*}
{}_\eta W_i =& \left\{\begin{array}{ll}
1 & \text{if } U_i \leq {}_\eta W'_i\\
0 & \text{otherwise.}
\end{array}\right.\\
\\
\\
\mathrm{Pr}\left({}_\eta W_i = 1\right) =& \mathrm{Pr}\left(U_i \leq {}_\eta W'_i\right)\\
=& \int_0^1 \mathrm{Pr}\left(x \leq {}_\eta W'_i\right) \mathrm{d}x\\
=& \int_0^1 \left(1 - \mathrm{Pr}\left({}_\eta W'_i \leq x\right)\right) \mathrm{d}x\\
=& 1 - \int_0^1 F_{{}_\eta W'_i}\left(x\right)\mathrm{d}x\\
=& 1 - \int_{-\infty}^1 F_{{}_\eta W'_i}\left(x\right)\mathrm{d}x\\
=& 1 - \mathbf{F}_{{}_\eta W'_i}(1)\\
=& \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) \mathrm{d}x\\
f_{{}_\eta W_i}(x) =& \left\{\begin{array}{ll}
1 - \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) \mathrm{d}x & \text{if } x = 0\\
\int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) \mathrm{d}x & \text{if } x = 1\\
0 & \text{otherwise.}\\
\end{array}\right.\\
\end{align*}

第五部

$E({}_\eta W_i)$と$E({}_\eta W_i^2)$を導出する。

$1 \leq i \leq n$に対して、

\begin{align*}
E\left({}_\eta W_i\right) =& 1 \cdot f_{{}_\eta W_i}(1) + 0 \cdot f_{{}_\eta W_i}(0)\\
=& \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) \mathrm{d}x\\
\\
\\
{}_\eta W_i^2 =& {}_\eta W_i \hspace{1em} \because {}_\eta W_i \in \{0, 1\}\\
E\left({}_\eta W_i^2\right) =& E\left({}_\eta W_i\right)\\
=& \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) \mathrm{d}x\\
\end{align*}

第六部

$E\left({}_\eta W_i \cdot {}_\tau W'_i\right)$を導出する。
途中でヘルパー関数$h_1(x)$を定義する。

$1 \leq i \leq n$に対して、

\begin{align*}
E\left({}_\eta W_i \cdot {}_\tau W'_i\right) =& \sum_{j=0}^1 \lim_{m \to \infty} \sum_{k=0}^{m-1} j \cdot \frac{k}{m} \cdot \mathrm{Pr}\left({}_\eta W_i = j \land \frac{k}{m} \leq {}_\tau W'_i \leq \frac{k}{m} + \frac{1}{m}\right)\\
=& \lim_{m \to \infty} \sum_{k=0}^{m-1} \frac{k}{m} \cdot \mathrm{Pr}\left({}_\eta W_i = 1 \land \frac{k}{m} \leq {}_\tau W'_i \leq \frac{k}{m} + \frac{1}{m}\right)\\
=& \lim_{m \to \infty} \sum_{k=0}^{m-1} \frac{k}{m} \cdot \mathrm{Pr}\left(U_i \leq {}_\eta W'_i \land \frac{k}{m} \leq {}_\tau W'_i \leq \frac{k}{m} + \frac{1}{m}\right)\\
=& \lim_{m \to \infty} \sum_{k=0}^{m-1} \frac{k}{m} \left(\mathrm{Pr}\left(U_i \leq {}_\eta W'_i \land {}_\tau W'_i \leq \frac{k}{m} + \frac{1}{m}\right) - \mathrm{Pr}\left(U_i \leq {}_\eta W'_i \land \lnot \left(\frac{k}{m} \leq {}_\tau W'_i\right)\right) + \mathrm{Pr}\left(U_i \leq {}_\eta W'_i \land \lnot \left(\frac{k}{m} \leq {}_\tau W'_i \lor {}_\tau W'_i \leq \frac{k}{m} + \frac{1}{m}\right)\right)\right)\\
=& \lim_{m \to \infty} \sum_{k=0}^{m-1} \frac{k}{m} \left(\mathrm{Pr}\left(U_i \leq {}_\eta W'_i \land {}_\tau W'_i \leq \frac{k}{m} + \frac{1}{m}\right) - \mathrm{Pr}\left(U_i \leq {}_\eta W'_i \land {}_\tau W'_i \leq \frac{k}{m}\right)\right)\\
=& \lim_{m \to \infty} \sum_{k=0}^{m-1} \frac{k}{m} \left(\int_0^1 \mathrm{Pr}\left(x \leq {}_\eta W'_i \land {}_\tau W'_i \leq \frac{k}{m} + \frac{1}{m}\right) \mathrm{d}x - \int_0^1 \mathrm{Pr}\left(x \leq {}_\eta W'_i \land {}_\tau W'_i \leq \frac{k}{m}\right) \mathrm{d}x\right)\\
h_1(x) =& \int_0^1 \mathrm{Pr}\left(y \leq {}_\eta W'_i \land {}_\tau W'_i \leq x\right) \mathrm{d}y\\
=& \int_0^1 \mathrm{Pr}\left(y \leq \frac{1}{1 + 6^\frac{A_i - \eta}{400}} \land \frac{1}{1 + 6^\frac{A_i - \tau}{400}} \leq x\right) \mathrm{d}y\\
=& \int_0^1 \mathrm{Pr}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \tau \leq A_i \leq 400 \log_6 \left(\frac{1}{y} - 1\right) + \eta\right) \mathrm{d}y\\
=& \int_0^1 \max\left(F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \eta\right) - F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \tau\right), 0\right) \mathrm{d}y\\
h'_1(x) =& \frac{\mathrm{d}}{\mathrm{d}x} h_1(x)\\
E\left({}_\eta W_i \cdot {}_\tau W'_i\right) =& \lim_{m \to \infty} \sum_{k=0}^{m-1} \frac{k}{m} \left(h_1\left(\frac{k}{m} + \frac{1}{m}\right) - h_1\left(\frac{k}{m}\right)\right)\\
=& \lim_{m \to \infty} \sum_{k=0}^{m-1} \frac{k}{m} \left(h_1\left(\frac{k}{m} + \frac{1}{m}\right) - h_1\left(\frac{k}{m}\right)\right) \frac{\frac{1}{m}}{\frac{1}{m}}\\
=& \lim_{m \to \infty} \sum_{k=0}^{m-1} \frac{k}{m} \frac{h_1\left(\frac{k}{m} + \frac{1}{m}\right) - h_1\left(\frac{k}{m}\right)}{\left(\frac{k}{m} + \frac{1}{m}\right) - \frac{k}{m}} \frac{1}{m}\\
=& \int_0^1 x h'_1(x) \mathrm{d}x\\
=& \left[x h_1(x)\right]_{x=0}^{x=1} - \int_0^1 h_1(x) \mathrm{d}x\\
=& h_1(1) - \int_0^1 h_1(x) \mathrm{d}x\\
=& \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \eta\right) \mathrm{d}y - \int_0^1 \int_0^1 \max\left(F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \eta\right) - F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \tau\right), 0\right) \mathrm{d}y \mathrm{d}x\\
\end{align*}

第七部

$E\left({}^\eta_\tau D_i\right)$と$E\left({}^\eta_\tau D_i^2\right)$と$V\left({}^\eta_\tau D_i\right)$を導出する。

$1 \leq i \leq n$に対して、

\begin{align*}
E\left({}^\eta_\tau D_i\right) =& E\left({}_\eta W_i - {}_\tau W'_i\right)\\
=& E\left({}_\eta W_i\right) - E\left({}_\tau W'_i\right)\\
=& \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) \mathrm{d}x - \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \tau\right) \mathrm{d}x\\
\\
\\
E\left({}^\eta_\tau D_i^2\right) =& E\left(\left({}_\eta W_i - {}_\tau W'_i\right)^2\right)\\
=& E\left({}_\eta W_i^2\right) + E\left({}_\tau W_i^{\prime 2}\right) - 2 E\left({}_\eta W_i \cdot {}_\tau W'_i\right)\\
=& \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) \mathrm{d}x + 2 \left(\int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \tau\right) \mathrm{d}x - \int_0^1 \int_0^x F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \tau\right) \mathrm{d}y \mathrm{d}x\right) - 2 \left(\int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \eta\right) \mathrm{d}y - \int_0^1 \int_0^1 \max\left(F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \eta\right) - F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \tau\right), 0\right) \mathrm{d}y \mathrm{d}x\right)\\
=& 2 \left(\int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \tau\right) \mathrm{d}x - \int_0^1 \int_0^x F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \tau\right) \mathrm{d}y \mathrm{d}x + \int_0^1 \int_0^1 \max\left(F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \eta\right) - F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \tau\right), 0\right) \mathrm{d}y \mathrm{d}x\right) - \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) \mathrm{d}x\\
\\
\\
V\left({}^\eta_\tau D_i\right) =& E\left({}^\eta_\tau D_i^2\right) - E\left({}^\eta_\tau D_i\right)^2\\
=& 2 \left(\int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \tau\right) \mathrm{d}x - \int_0^1 \int_0^x F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \tau\right) \mathrm{d}y \mathrm{d}x + \int_0^1 \int_0^1 \max\left(F_{A_i}\left(400 \log_6 \left(\frac{1}{y} - 1\right) + \eta\right) - F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \tau\right), 0\right) \mathrm{d}y \mathrm{d}x\right) - \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) \mathrm{d}x - \left(\int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \eta\right) \mathrm{d}x - \int_0^1 F_{A_i}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \tau\right) \mathrm{d}x\right)^2\\
\end{align*}

第八部

$F_{{}^\eta_\tau \hat{D}_n}(x)$を導出する。

中心極限定理より、${}^\eta_\tau \hat{D}_n \sim N\left(n E\left({}^\eta_\tau D_1\right), n V\left({}^\eta_\tau D_1\right)\right)$に近似できるので、

\begin{align*}
F_{{}^\eta_\tau \hat{D}_n}(x) \approx& \frac{1}{2} \left(1 + \mathrm{erf}\left(\frac{x - n E\left({}^\eta_\tau D_1\right)}{\sqrt{2n V\left({}^\eta_\tau D_1\right)}}\right)\right)\\
\end{align*}

第九部

$F_{{}_\theta P'}(x)$を導出する。
途中でヘルパー関数$h_2(x)$を定義する。

\begin{align*}
h_2(x) =& \sum_{i=1}^n {}_x W'_i + \frac{1}{1 + 6^\frac{\theta - x}{400}}\\
\sum_{i=1}^n {}_\theta W_i + 0.5 =& h_2\left({}_\theta P'\right)\\
{}_\theta P' =& h_2^{-1}\left(\sum_{i=1}^n {}_\theta W_i + 0.5\right)\\
F_{{}_\theta P'}(x) =& \mathrm{Pr}\left({}_\theta P' \leq x\right)\\
=& \mathrm{Pr}\left(h_2^{-1}\left(\sum_{i=1}^n {}_\theta W_i + 0.5\right) \leq x\right)\\
=& \mathrm{Pr}\left(\sum_{i=1}^n {}_\theta W_i + 0.5 \leq h_2(x)\right)\\
=& \mathrm{Pr}\left(\sum_{i=1}^n {}_\theta W_i + 0.5 \leq \sum_{i=1}^n {}_x W'_i + \frac{1}{1 + 6^\frac{\theta - x}{400}}\right)\\
=& \mathrm{Pr}\left(\sum_{i=1}^n {}^\theta_x D_i \leq \frac{1}{1 + 6^\frac{\theta - x}{400}} - 0.5\right)\\
=& \mathrm{Pr}\left({}^\theta_x \hat{D}_n \leq \frac{1}{1 + 6^\frac{\theta - x}{400}} - 0.5\right)\\
=& F_{{}^\theta_x \hat{D}_n}\left(\frac{1}{1 + 6^\frac{\theta - x}{400}} - 0.5\right)\\
\approx& \frac{1}{2} \left(1 + \mathrm{erf}\left(\frac{\frac{1}{1 + 6^\frac{\theta - x}{400}} - 0.5 - n E\left({}^\theta_x D_1\right)}{\sqrt{2n V\left({}^\theta_x D_1\right)}}\right)\right)
\end{align*}

第十部

$\mathrm{Pr}\left(\theta \geq {}_\theta R_3\right)$を導出する。

\begin{align*}
\mathrm{Pr}\left(\theta \geq {}_\theta R_3\right) =& \mathrm{Pr}\left(\theta \geq {}_\theta R_2 - 1200\right)\\
=& \mathrm{Pr}\left(\theta \geq {}_\theta P - 1200\right)\\
=& \mathrm{Pr}\left(\theta \geq {}_\theta P' - 1200\right)\\
=& \mathrm{Pr}\left({}_\theta P' \leq \theta + 1200\right)\\
=& F_{{}_\theta P'}\left(\theta + 1200\right)\\
\approx& \frac{1}{2} \left(1 + \mathrm{erf}\left(\frac{-\frac{215}{434} - n E\left({}^\theta_{\theta + 1200} D_1\right)}{\sqrt{2n V\left({}^\theta_{\theta + 1200} D_1\right)}}\right)\right)\\
\end{align*}

第十一部

$\forall \theta. \mathrm{Pr}\left(\theta \geq {}_\theta R_3\right) \geq 0.999$を反証する。

\begin{align*}
\mathrm{Pr}\left(\theta \geq {}_\theta R_3\right) \geq& 0.999\\
\frac{1}{2} \left(1 + \mathrm{erf}\left(\frac{-\frac{215}{434} - n E\left({}^\theta_{\theta + 1200} D_1\right)}{\sqrt{2n V\left({}^\theta_{\theta + 1200} D_1\right)}}\right)\right) \geq& 0.999\\
\frac{-\frac{215}{434} - n E\left({}^\theta_{\theta + 1200} D_1\right)}{\sqrt{2n V\left({}^\theta_{\theta + 1200} D_1\right)}} \geq& \mathrm{erf}^{-1}(0.998)\\
\frac{-\frac{215}{434} - n E\left({}^\theta_{\theta + 1200} D_1\right)}{\sqrt{2n V\left({}^\theta_{\theta + 1200} D_1\right)}} \geq& 2.1851242191330043 \ldots\\
\end{align*}

$\theta$が十分大きいとき、$E\left({}^\theta_{\theta + 1200} D_1\right)$は0にいくらでも近付けることができる。
なぜならば、

\begin{align*}
E\left({}^\theta_{\theta + 1200} D_1\right) =& \int_0^1 F_{A_1}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \theta\right) \mathrm{d}x - \int_0^1 F_{A_1}\left(400 \log_6 \left(\frac{1}{x} - 1\right) + \theta + 1200\right) \mathrm{d}x\\
=& E\left({}_\theta W'_1\right) - E\left({}_{\theta + 1200} W'_1\right)\\
\end{align*}

であるが、$\theta$が十分大きいとき、$E\left({}_\theta W'_1\right)$も$E\left({}_{\theta + 1200} W'_1\right)$もいくらでも1に近付けることができるからである。

$\sqrt{2n V\left({}^\theta_{\theta + 1200} D_1\right)}$は正の数なので、$\frac{-\frac{215}{434} - n E\left({}^\theta_{\theta + 1200} D_1\right)}{\sqrt{2n V\left({}^\theta_{\theta + 1200} D_1\right)}}$は、$\theta$が十分大きいとき負の数である。
これは$\frac{-\frac{215}{434} - n E\left({}^\theta_{\theta + 1200} D_1\right)}{\sqrt{2n V\left({}^\theta_{\theta + 1200} D_1\right)}} \geq 2.1851242191330043 \ldots$に矛盾する。

この証明は正しいのか？

中心極限定理による近似はこの文脈で妥当なのか検証が必要。
単純に証明が長すぎるのでどこかでミスをしている可能性は否めない。