Ln=Ll+1に式を代入して、
[log(x) +s*log(3/2) +log(1+1/3x)…(1+1/3x_s-1)] = [log(x) +s*log(3/2)] +1
切り上げを外して
log(1+1/3x)…(1+1/3x_s-1) < 2
logを外して
(1+1/3x)…(1+1/3x_s-1) < 4
となります。
もしコラッツ予想で4-2-1以外のループがあったら
(1+1/3x)…(1+1/3x_s-1)
の中のループ1周期の積をXとおいて
X*X*X*…
となりますが、X>1なので、いずれ
X*X*X*… > 4
となって
(1+1/3x)…(1+1/3x_s-1) < 4
と矛盾します。
よって
コラッツ予想で4-2-1以外のループは存在しない
ことが証明できました。
