コラッツ予想がとけたらいいな

コラッツ予想がとけたらいいな at MATH

[前50を表示]
450:righ1113 ◆OPKWA8uhcY
16/06/14 09:36:32.33 GDyexPn/.net
Xsを12ステップで区切った時、8個以上1が入る事はありません。(※)
Coq版できました。
ただnub permutationsの部分がCoqでは12時間計算しても終わらなかったので、
そこだけHaskellで495行出力して（それでも1時間かかる）、permu.vに書いています。
permu.v
Require Import List.
Definition nub_permu: list (list nat) :=
((0::0::0::0::1::1::1::1::1::1::1::1::nil)::
(1::0::0::0::0::1::1::1::1::1::1::1::nil)::
---略---
(1::1::1::1::1::0::1::0::0::1::1::0::nil)::
(1::1::1::1::1::1::0::0::0::1::1::0::nil)::nil).

451:righ1113 ◆OPKWA8uhcY
16/06/14 09:41:24.87 GDyexPn/.net
collatz06.v
Require Import Omega.
Require Import List.
Require Import Coq.Program.Wf.
Require Import permu.
Fixpoint cycle{A} (n:nat) (la:list A) (lb:list A) :list A :=
match n with
| 0 => la
| S m => cycle m (app la lb) lb
end.
Fixpoint remove_0_0 (l:list nat): bool :=
match l with
| nil => true
| _::nil => true
| 0::0::_ => false
| l1::ls => remove_0_0 ls
end.
Fixpoint remove_1_1_1 (l:list nat): bool :=
match l with
| nil => true
| _::nil => true
| _::_::nil => true
| 1::1::1::_ => false
| l1::ls => remove_1_1_1 ls
end.
Fixpoint remove_1_1_0_1_1 (l:list nat): bool :=
match l with
| nil => true
| _::nil => true
| _::_::nil => true
| _::_::_::nil => true
| _::_::_::_::nil => true
| 1::1::0::1::1::_ => false
| l1::ls => remove_1_1_0_1_1 ls
end.

452:righ1113 ◆OPKWA8uhcY
16/06/14 09:46:24.20 GDyexPn/.net
Fixpoint beq_list (l:list nat) (m:list nat): bool :=
match l,m with
| nil, nil => true
| nil, _ => false
| _, nil => false
| l1::ls, m1::ms => if beq_nat l1 m1 then beq_list ls ms else false
end.
Fixpoint elem (x:list nat) (l:list (list nat)): bool :=
match l with
| nil => false
| l1::ls => if beq_list x l1 then true else elem x ls
end.
Fixpoint nub (l:list (list nat)): list (list nat) :=
match l with
| nil => nil
| l1::ls => (if elem l1 ls then nil else (l1::nil)) ++ (nub ls)
end.
Definition bnt_nat (x:nat) (y:nat): bool :=
if beq_nat x y then false else true.
Fixpoint concatMap (f:nat->list (list nat)) (l:list nat): list (list nat) :=
match l with
| nil => nil
| l1::ls => (f l1) ++ concatMap f ls
end.
Fixpoint replace (x y:nat) (l m:list nat): list nat :=
match m with
| nil => l
| m1::ms => if beq_nat x m1 then replace x y (y::l) ms else replace x y (m1::l) ms
end.
Program Fixpoint permutations (l:list nat) (cnt:nat) {measure cnt}: (list (list nat)) :=
match cnt with
| 0 => ((nil)::nil)
| _ =>
match l with
| nil => ((nil)::nil)
| ls => concatMap (fun x => (map (fun y => x::y) (permutations (filter (bnt_nat x) ls) (cnt-1)))) ls
end
end.
Next Obligation.
omega.
Qed.

453:righ1113 ◆OPKWA8uhcY
16/06/14 09:49:36.01 GDyexPn/.net
Definition multi1: list (list nat) :=
filter remove_1_1_1
(filter remove_0_0
(* (nub (map (replace 2 0 nil)
(map (replace 3 0 nil)
(map (replace 4 0 nil)
(map (replace 5 1 nil)
(map (replace 6 1 nil)
(map (replace 7 1 nil)
(map (replace 8 1 nil)
(map (replace 9 1 nil)
(map (replace 10 1 nil)
(map (replace 11 1 nil)
(permutations (0::1::2::3::4::5::6::7::8::9::10::11::nil) 12)))))))))))) *)
nub_permu).
Definition multi2: list (list nat) :=
filter remove_1_1_0_1_1 (filter remove_1_1_1 (map (cycle 2 (nil)) multi1)).
Theorem multi2_is_nil:
multi2 = nil.
Proof.
compute.
reflexivity.
Qed.
やっぱQed.が通ると気持ちが良いですね。

454:righ1113 ◆OPKWA8uhcY
16/06/14 17:28:23.76 GDyexPn/.net
pdf修正しました。
まだpre版で、日本語と英語が混ざってて気持ち悪いですが、
良かったら見てみてください。
URLﾘﾝｸ(drive.google.com)

455:１３２人目の素数さん
16/06/14 20:06:46.34 mUIjFDF1.net
俺じゃ理解できないけどどうやら進んでるようで、おめ

456:righ1113 ◆OPKWA8uhcY
16/06/15 22:55:25.35 s5Jlp8vN.net
ありがとうございます。

457:righ1113 ◆OPKWA8uhcY
16/06/19 03:31:16.15 HPZ4uwl5.net
ちょっとは読みやすくなったと思います。
URLﾘﾝｸ(drive.google.com)
-----
「ライトエッジパターン」というものを定義する。
これは、右端が繰り上がった時は1、そうでない時は0を置くものである。
x=319のライトエッジパターンは、[-,0,1,1,0,1,0,1,1,0,1,0,1,0,1,1,0,1,1]である。
-----

458:１３２人目の素数さん
16/06/19 05:13:52.50 R9PbWXF5.net
>>1
コラッツパターンとかライトエッジパターンとかよくわからん。
もし余力があればideoneにプログラム上げてくれんか？
好きな数を入力してそれに対してそのパターンを出力してほしい。
URLﾘﾝｸ(ideone.com)
haskellも選べるからたぶんもうすでに書いたものがあるだろ？

459:righ1113 ◆OPKWA8uhcY
16/06/19 06:49:14.93 HPZ4uwl5.net
Excelマクロでも良いですか？
URLﾘﾝｸ(drive.google.com)
A列に10進数で数を入れて、「計算」ボタンを押すと、
B列にライトエッジパターンが、
C列からにコラッツパターンが表示されます。
ideoneはよく分かりませんでした。 <

460:righ1113 ◆OPKWA8uhcY
16/06/19 06:55:07.24 HPZ4uwl5.net
あ、ダウンロードして使って下さいね。

461:１３２人目の素数さん
16/06/19 08:36:15.00 R9PbWXF5.net
エクセルマクロはうごきました。
サンクス。
左端がどう決まってるのかいまいち分かってないんだけど
２で割れた回数とかだよね？
>>439のは英語だったからいまいち自信がもてない。

462:righ1113 ◆OPKWA8uhcY
16/06/19 12:31:44.57 o4I0V/Mj.net
コラッツパターンの左側は、
コラッツ操作で＜2で割った回数-1＞を蓄積しているものです。
>>172にもあります。
（マクロやpdfでは0を書いてないけど）

463:１３２人目の素数さん
16/06/20 20:49:50.82 AO/P2Y9A.net
左端を伸ばすパターンの説明で
3. Becomes the next x from the left end of the 1 to 1 on the right.
てのがあるんだけど、どう訳せばいいのかよくわからんｗ
教えて～

464:righ1113 ◆OPKWA8uhcY
16/06/20 22:36:36.36 IBPpfU1W.net
「次のxとして、左端の1から右端の1までを取る」という意味です。
_111111001　=x0が
1011110111　=x1になった時、
x1は左端の1から右端の1までを取るね、という事です。
実は英語は苦手で、いつも赤点でしたwww

465:righ1113 ◆OPKWA8uhcY
16/06/21 06:10:35.56 pnfuA33J.net
>>439を更新しました。

466:righ1113 ◆OPKWA8uhcY
16/06/21 14:05:46.27 w+gnd+8K.net
今日扇風機を出しました。すずしいです。

467:１３２人目の素数さん
16/06/21 20:10:09.84 shTmSKB6.net
まだ理解できてないが左端を伸ばすパターンもエクセルマクロあるの？
あるならオクレ。

468:righ1113 ◆OPKWA8uhcY
16/06/21 20:18:58.92 w+gnd+8K.net
左端を伸ばすパターンは数が左に伸びるのと、
ステップが無限に続くので、作れてないです。すみません。

469:１３２人目の素数さん
16/06/21 20:27:44.17 shTmSKB6.net
ないのか、残念。
まあしょうがない。

470:１３２人目の素数さん
16/06/21 21:05:09.09 shTmSKB6.net
んー左に伸ばすパターンって出力のサイズを制限したらプログラム書ける？
制限しても難しい？

471:righ1113 ◆OPKWA8uhcY
16/06/21 21:34:19.98 w+gnd+8K.net
ちょっとやってみます。
気長にお待ちください。

472:１３２人目の素数さん
16/06/21 21:48:26.05 shTmSKB6.net
すまんね、クレクレ言って。

473:righ1113 ◆OPKWA8uhcY
16/06/22 06:06:53.11 kg3XYDgA.net
URLﾘﾝｸ(drive.google.com)
A列に10進数で数を入れて、「計算」ボタンを押すと、
B列にコラッツパターンのライトエッジパターンが、
C列に左端を伸ばすパターンのライトエッジパターンが、
D列からにコラッツパターンと左端を伸ばすパターンが表示されます。
B,C列で色が変わっている所は、コラッツパターンと左端を伸ばすパターンの右端がずれている所です。
大きい数を入れると「列が足りない」エラーが出るかもしれませんが、
Excel2007以降を使っているならば、Officeボタンから「変換」を選んで開きなおすと、
最大列が256列から16384列になります。

474:成清愼
16/06/22 18:39:08.04 dJB43qU2.net
以前より進化しました。
諸兄におかれましては何卒よろしくご査収の上ご批評賜りたくよろしくお願い申し上げます。
URLﾘﾝｸ(koubeichizoku.ix-web.tk)

475:１３２人目の素数さん
16/06/22 20:08:21.63 3ACjIS1K.net
>>455
おおう、乙カレ。やるね。
左端を伸ばすパターンの正体がいまいちわかってないんだけどどういう思想で出来たものなの？
説明できるなら説明クレクレ。

476:１３２人目の素数さん
16/06/22 20:25:08.09 3ACjIS1K.net
333入れたら結果が出てこなかったんだが？
なんか制限とかあるんだっけ？
よくわかってなくてスマン。

477:righ1113 ◆OPKWA8uhcY
16/06/22 20:27:44.55 SAQFF6Ga.net
コラッツ予想を2進数で考える、というのは前々からあって、
コラッツパターンを見出した時に、最後のルール
「最後に、左端に+1する」
を外したら面白いんじゃね、と思って左端を伸ばすパターンが出来ました。
まあ、偶然の産物ですね。

478:righ1113 ◆OPKWA8uhcY
16/06/22 20:32:36.93 SAQFF6Ga.net
>>458
自分の環境では出てきます。
・マクロを有効にする
・数字を入れた後一回Enterを押して、カーソルを合わせ直して実行する
あたりを試してみてください。

479:１３２人目の素数さん
16/06/22 20:39:44.54 3ACjIS1K.net
>>460
でました。
カーソル合わせてなかったのかな？多分。

480:１３２人目の素数さん
16/06/22 20:55:10.79 3ACjIS1K.net
あとは論文を読むだけか
読めるかな～

481:１３２人目の素数さん
16/06/22 21:22:24.14 3ACjIS1K.net
ライトエッジを１２個づつに区切ったとき８個以上１が入らないことが言えると
なぜコラッツ予想が証明されたことになるの？
今はそこで悩んでる。

482:１３２人目の素数さん
16/06/22 21:31:10.84 3ACjIS1K.net
左端パターンとコラッツパターンのずれが有限だとコラッツの予想が証明されたことになるの？
やっぱまだよくわからん。

483:righ1113 ◆OPKWA8uhcY
16/06/22 22:01:29.56 SAQFF6Ga.net
>>463
X0とy0B*2^(py0+1)は右端が1ずれた（y0Bが大きい）状態からスタートします。
y0Bの12区切りのライトエッジパターンは1が7個はいっていて、
もしX0の12区切りのライトエッジパターンに1が8個以上入らなければ、初期値の1ずれがずっと維持されるので、
X0 < y0B*2^(py0+1)が言えるわけです。
これ自体でコラッツ予想は証明されないです。

484:righ1113 ◆OPKWA8uhcY
16/06/22 22:05:31.40 SAQFF6Ga.net
>>464
＞左端パターンとコラッツパターンのずれが有限だとコラッツの予想が証明されたことになるの？
次のセクションで、ずれが有限であることを利用して、
「5 there is no loop other than 4-2-1 in Collatz conjecture」
「6 Collatz conjecture is not the number that diverges to infinity」
で、「コラッツ予想に4-2-1以外のLoopがない」「コラッツ予想で無限大に発散する数はない」
事を個別に証明しています。

485:righ1113 ◆OPKWA8uhcY
16/06/22 22:11:13.67 SAQFF6Ga.net
>>465
2個目のX0 < y0B*2^(py0+1)は間違いで
Xs < ysB*2^(pys+1)
です。

486:righ1113 ◆OPKWA8uhcY
16/06/23 05:02:38.13 ta0z2vBC.net
最新版のpdfをご覧ください。
URLﾘﾝｸ(drive.google.com)

487:１３２人目の素数さん
16/06/23 21:56:11.47 tqdQH9fb.net
>>1
頑張ってもらってるのにスマンが俺の頭じゃいまいち理解が追いつかない。
面白そうではあるんだけど。
まあ、ボチボチ読んでみます。

488:１３２人目の素数さん
16/06/23 22:55:11.53 tqdQH9fb.net
５章の（１４）（１５）の式なんだけど
By the product of the loop 1 cycle X
X x X x X ...
It will be but , X > 1 so, either
X x X x X x ... > 2 ^ 3
てのがよくわからないんだけど、つまりXって何なの？

489:righ1113 ◆OPKWA8uhcY
16/06/23 23:37:45.96 2td5n7de.net
スレでは>>92ですが、
実際は違いますが、9→7→11→17→9とループしたとすると、
X=(1+1/(3*9))*(1+1/(3*7))*(1+1/(3*11))*(1+1/(3*17))となります。
これは明らかに1より大きいので、
X*X*X*... > 2^3となって、
(1+1/(3*x0))...(1+1/(3*x_s-1)) < 2^3と矛盾します。

490:１３２人目の素数さん
16/06/24 00:02:13.23 iaaPmoqS.net
よくわからん。
1→1のループは
X=(1+1/(3*1))=4/3>1
となって
X * X * X * >2^3となって
(1+1/(3*x0))...(1+1/(3*x_s-1)) < 2^3と矛盾しないの？

491:righ1113 ◆OPKWA8uhcY
16/06/24 00:31:18.91 4KA2vNvp.net
1→1のループは除外します。
全体的にこの論文は、コラッツ操作で1にたどり着く直前までを考えます。
1になった後のコラッツパターンを考えると、左端を伸ばすパターンとのずれは際限なく大きくなりますから。
URLﾘﾝｸ(cdn-ak.f.st-hatena.com)

492:righ1113 ◆OPKWA8uhcY
16/06/24 00:37:22.10 4KA2vNvp.net
つまり、コラッツ操作で1にたどり着いた後は、
(1+1/(3*x0))...(1+1/(3*x_s-1)) < 2^3
が成り立たなくなります。

493:１３２人目の素数さん
16/06/26 02:47:49.92 vn9j7NkJ.net
とりあえず、色々コンピュータで検証してます。
4.1 Xsを12ステップで区切ったときライトエッジパターンに８個以上１が入ることはない、についてだけど
2連続の0はない
3連続の1はない
11011のパターンはない
で計算したところ以下のパターンが出てきたんだが。
110101101011
これは問題になる？

494:righ1113 ◆OPKWA8uhcY
16/06/26 12:47:06.84 ONsv4xjJ.net
110101101011は、二回繰り返すと
110101101011110101101011となって、
3連続の1が出てくるので、除外されます。
Coqでは、>>468のpdfで、25ページ

495:の下の方の (filter remove_1_1_1 (map (cycle 2 nil) remove_8_12’)で、 cycle 2でパターンを二回繰り返して、filter remove_1_1_1で3連続の1を除外しています。

496:１３２人目の素数さん
16/06/26 13:09:08.17 vn9j7NkJ.net
どゆこと？
ライトエッジパターンは必ず周期１２のループになるの？

497:righ1113 ◆OPKWA8uhcY
16/06/26 14:12:10.81 ONsv4xjJ.net
そっかー、ならないですね。
二周期目を調べる時は、
12ステップで除外しきれなかったパターンの直積を取って、filterをかけないとダメですね。
……と思ったら「12ステップで除外しきれなかったパターン」って上の110101101011しかないんですね。
だったらcycle 2も直積も同じことで、110101101011110101101011となって、やはり除外されます。
これでどうでしょうか？

498:righ1113 ◆OPKWA8uhcY
16/06/26 14:41:21.46 ONsv4xjJ.net
いや、なんか怪しいです。
もうちょっと考え直してみます。

499:成清愼
16/06/26 18:26:22.61 0JPNDOFj.net
他スレのご指摘により数式だけでなく日本語の説明を加えました。
諸兄におかれましては何卒よろしくご査収の上ご批評賜りたくよろしくお願い申し上げます。
URLﾘﾝｸ(koubeichizoku.ix-web.tk)

500:成清愼
16/06/26 18:55:58.84 0JPNDOFj.net
ここで論じられているビットパターンは拙論では
2^p×3^m×ｇ±1　（ｇは 6a±1) として捉えており、これらは素因数分解の一意性
からユニークな数であることに着目しています。
コラッツ予想の題意に従った奇数から奇数への変化のうち奇数間で増大するものを
≫+で表せば　2・2＾p・ｇ－1　≫+　2・2＾（p-1）・3＾1・ｇ－1≫+　2・2＾（p-2）・3＾2・ｇ－1　...
≫+　2・2＾1・3＾（p-1）・ｇ－1　≫+　2・3＾p・ｇ－1　となって
L(p，g)：＝｛2・2＾p・ｇ－1，2・2＾（p-1）・3＾1・ｇ－1，　2・2＾（p-2）・3＾2・ｇ－1　...
，+　2・2＾1・3＾（p-1）・ｇ－1　，2・3＾p・ｇ－1｝　となって　相異なる（p，g）のL集合同士は互いに素
また同じく相異なるLの和集合同士も互いに素となります。（L（p,g）∪ L(p',g')=φ）（p≠p’）∨（g≠g’）

501:成清愼
16/06/26 18:57:28.09 0JPNDOFj.net
ここで論じられているビットパターンは拙論では
2^p×3^m×ｇ±1　（ｇは 6a±1) として捉えており、これらは素因数分解の一意性
からユニークな数であることに着目しています。
コラッツ予想の題意に従った奇数から奇数への変化のうち奇数間で増大するものを
≫+で表せば　2・2＾p・ｇ－1　≫+　2・2＾（p-1）・3＾1・ｇ－1≫+　2・2＾（p-2）・3＾2・ｇ－1　...
≫+　2・2＾1・3＾（p-1）・ｇ－1　≫+　2・3＾p・ｇ－1　となって
L(p，g)：＝｛2・2＾p・ｇ－1，2・2＾（p-1）・3＾1・ｇ－1，　2・2＾（p-2）・3＾2・ｇ－1　...
，+　2・2＾1・3＾（p-1）・ｇ－1　，2・3＾p・ｇ－1｝　とすれば、　相異なる（p，g）のL集合同士は互いに素
また同じく相異なるLの和集合同士も互いに素となります。（L（p,g）∪ L(p',g')=φ）（p≠p’）∨（g≠g’）

502:１３２人目の素数さん
16/06/26 20:18:08.07 EbU1sa9O.net
>>479
coqが通ったのに何が怪しいの？
なんのためのcoqなの？
coqは通ったけど、通った命題そのものがトンチンカンな主張だったってこと？

503:righ1113 ◆OPKWA8uhcY
16/06/26 20:34:28.45 ONsv4xjJ.net
＞coqは通ったけど、通った命題そのものがトンチンカンな主張だったってこと？
まあ、そういう事です。
Coqに通すまでの論証に穴があったという事です。

504:１３２人目の素数さん
16/06/26 21:05:16.83 vn9j7NkJ.net
そうならないように始めの命題からCoqで一気通貫で証明を通すことが望ましいね。
実際には難しいだろうけど。

505:righ1113 ◆OPKWA8uhcY
16/06/26 23:31:32.04 ONsv4xjJ.net
110101101011は除外出来ない事が分かりました。
そこで証明を次のように修正します。
12区切りのライトエッジパターンに110101101011が現れたとする。
末尾は1なので、次の12区切りは先頭が0である。
「先頭が1」「2連続の0」「3連続の1」「1,1,0,1,1」を除外した、12区切りで1が7個入るパターンは、
次の6つしかない。（Haskellで確認済み）
[0,1,0,1,0,1,1,0,1,0,1,1]
[0,1,0,1,1,0,1,0,1,0,1,1]
[0,1,1,0,1,0,1,0,1,0,1,1]
[0,1,1,0,1,0,1,1,0,1,0,1]
[0,1,1,0,1,0,1,0,1,1,0,1]
[0,1,0,1,1,0,1,0,1,1,0,1]
1~3個目は11で終わっているため、次の12区切りも0始まりとなってループする。
再び110101101011が来る余地は無い。
4~6個目は、次の12区切りで1始まりが可能なので、さらに調べる。

506:righ1113 ◆OPKWA8uhcY
16/06/26 23:35:20.57 ONsv4xjJ.net
「先頭が10」で、「2連続の0」「3連続の1」「1,1,0,1,1」を除外した、12区切りで1が7個入るパターンは、
次の8つしかない。（Haskellで確認済み）
[1,0,1,0,1,0,1,0,1,0,1,1]
[1,0,1,0,1,0,1,1,0,1,0,1]
[1,0,1,0,1,1,0,1,0,1,0,1]
[1,0,1,1,0,1,0,1,0,1,0,1]
[1,0,1,0,1,0,1,0,1,1,0,1]
[1,0,1,1,0,1,0,1,1,0,1,0]
[1,0,1,1,0,1,0,1,0,1,1,0]
[1,0,1,0,1,1,0,1,0,1,1,0]
1個目は11で終わっているため、次の12区切りも0始まりとなってループする。
2~5個目は1で終わっているため、次の12区切りも1or0始まりとなってループする。
6,7個目は、連続して並べると、
110101101011 [0,1,*,*,*,*,*,*,*,1,0,1] [1,0,1,1,0,1,0,1,1,0,1,0]
110101101011 [0,1,*,*,*,*,*,*,*,1,0,1] [1,0,1,1,0,1,0,1,0,1,1,0]
となって「1,1,0,1,1」が現れるので除外される。
8個目は、連続して並べると、
110101101011 [0,1,*,*,*,*,*,*,*,1,0,1] [1,0,1,0,1,1,0,1,0,1,1,0] 110101101011
となって「1,1,0,1,1」が現れるので110101101011にはならない。
よって、二回以上110101101011が現れることはない。
初期値をX0 とy0B * 2^(py0+2)（1ずらし→2ずらし）から始めれば、
Xs はysB * 2^(pys+2) を超えないので、Xs < ysB * 2^(pys+2) である。
さて、これをCoqでどうやってやろう……

507:１３２人目の素数さん
16/06/27 01:06:26.26 aRJFqPL1.net
どうせその論証にも穴がある。
都合の悪い並びはいつまで経ってもなくならない。
穴を埋めようとすると
＞「先頭が10」で、「2連続の0」「3連続の1」「1,1,0,1,1」を除外した
こんな感じの細かい条件がさらに追加される。
それでもなお、都合の悪い並びはなくならない。
キリがないどころか、そもそもこのやり方では本質的に不可能。
0と1の並び方の規則を探求すること自体が全くの無駄。
こいつらは基本的にランダム列に近づきたがっている。
途中で不完全燃焼を起こしてループに陥るだけで、
それまでの間はランダム列に近づきたがっている。
そうやって規則がない方向に行こうとしている対象について
規則を探求しても、うまく行くわけないだろ。
それよりも、「ランダム列に近づきたがってる」ことを
実際に証明した方が早い(もちろん現状では未解決)。

508:righ1113 ◆OPKWA8uhcY
16/06/27 06:17:35.12 QoZs645r.net
>>486-487の状態遷移図を作ってみました。
URLﾘﾝｸ(cdn-ak.f.st-hatena.com)
これを見ると穴は無いと思うんんですけどねー

509:１３２人目の素数さん
16/06/27 20:20:15.84 q11mMK/q.net
>>489
これ検証すんの結構つらいわｗ
Coqでなんとかならんか？
１が７個のパターンだけ考えてるみたいだけど
１が６個以下のパターンを除外していい理由がよくわからん。

510:righ1113 ◆OPKWA8uhcY
16/06/27 20:37:30.69 QoZs645r.net
Coqは考え中です。
（ちゃんとやってないですけど）
1が6個のパターンは、0,0が除外されるので
[0,1,0,1,0,1,0,1,0,1,0,1]
[1,0,1,0,1,0,1,0,1,0,1,0]
しかないんんですけど、こんなパターンは無いかなあと。
（どこかで1,1,が現れるはず）
1が5個以下のパターンは、必ず0,0が含まれるので、
全て除外されます。

511:１３２人目の素数さん
16/06/27 21:31:29.20 q11mMK/q.net
>>こんなパターンは無いかなあと。
数学の証明しようってのにずいぶんずぼらだなｗ
まあ気持ちはわかるが。

512:righ1113 ◆OPKWA8uhcY
16/06/27 21:44:48.79 QoZs645r.net
後でちゃんと証明しますねw

513:１３２人目の素数さん
16/06/27 22:43:04.85 j3iC4IAi.net
ポエムのうちは読む気はないけど証明されたら眺めてみようかくらいに思ってる人はそれなりにいると思うからがんばってね。

514:righ1113 ◆OPKWA8uhcY
16/06/28 02:37:55.06 yHVq8lhZ.net
12区切りで1が6個入るパターンは除外される証明ができました。
>>468の7ページを見ながらご覧下さい。
URLﾘﾝｸ(cdn-ak.f.st-hatena.com)
ライトエッジパターンでは「2連続の0」「3連続の1」「1,1,0,1,1」に加えて「0,1,0,1,0,1,0」
も除外されるという事です。

515:righ1113 ◆OPKWA8uhcY
16/06/28 14:15:43.06 QhVmHp3u.net
次の補題も証明します。
11010 11010 11010 11010 11ライトエッジパターンは無い。
URLﾘﾝｸ(cdn-ak.f.st-hatena.com)

516:１３２人目の素数さん
16/06/28 15:36:10.76 7Qb0mD6N.net
>>468
発散する初期値がないことの証明も間違ってるように見える。
実際に (log_2 x_s)/s の挙動を計算してみると、
発散する初期値があろうがなかろうが、無条件で有界であることが分かる。
まず、9ページ目の(3)式はコラッツの軌道のsステップ目を表現しただけだから、
何の条件もなしに成り立っている。以下、(3)式から出発して
x_s ＝ x_0(3^s/2^t)(1＋1/(3x_0))・・・(1＋1/(3x_{s－1}))
≦ x_0(3^s/2^t)(1＋1/3)・・・(1＋1/3)
＝ x_0(3^s/2^t)(1＋1/3)^s
＝ x_0(3^s/2^t)(4/3)^s
≦ x_0(3^s)(4/3)^s
＝ x_0 4^s
となるので、log_2 x_s ≦ log_2 x_0＋slog_2 4 となって、
(log_2 x_s)/s ≦(log_2 x0)/s ＋ 2 となる。よって、
発散する初期値があろうがなかろうが、無条件で有界になっている。
このことから、pdfの10ページ目にある
「 Here, from Fig.3 (傾きが垂直に近づくので) 」
のところは自動的に間違いとなる。

517:righ1113 ◆OPKWA8uhcY
16/06/28 15:53:05.99 QhVmHp3u.net
あちゃー
確かにその通りですね。

518:righ1113 ◆OPKWA8uhcY
16/06/28 18:10:44.75 QhVmHp3u.net
こういうのはどうでしょうか。
xは発散するとする。
(1+1/3x_0)…(1+1/3x_{s-1}) < 2^4 だから (1+1/3x_1)…(1+1/3x_s) < 2^4 も成り立つ。
t=saと置き、(1+3/t)^t < (1+1/3x_1)…(1+1/3x_s)が成り立つようにaを定める。
s→∞でt→∞だから、
lim[t→∞](1+3/t)^t = e^3 ≒ 20 > 16 だから、
無限大に辿り着く前に16を超える。越えた所をs'と置くと、
(1+1/3x_1)…(1+1/3x_s') > 16 となって、(1+1/3x_1)…(1+1/3x_s') < 2^4 と矛盾する。

519:１３２人目の素数さん
16/06/28 19:21:07.89 7Qb0mD6N.net
>>499
＞t=saと置き、(1+3/t)^t < (1+1/3x_1)…(1+1/3x_s)が成り立つようにaを定める。
問題外。x_sの発散スピードが大きいとき、そのようなaは取れない。
コラッツの問題を舐めるな。

520:righ1113 ◆OPKWA8uhcY
16/06/28 20:08:23.00 QhVmHp3u.net
t=e^sとか、t=s!とかにしてもダメなんでしょうか？

521:１３２人目の素数さん
16/06/28 20:15:33.20 7Qb0mD6N.net
>>501
どうも君は不等式に対する感覚がイカれてるね。
パッと見てすぐに分かる間違いに全く気づいてない。
tが大きければ大きいほど、(1＋3/t)^t は e^3 に近づくのだから、余計に
(1+3/t)^t < (1+1/3x_1)…(1+1/3x_s)
が成り立ちにくくなるだけだろ。
ていうか、x_1からx_sまでが物凄い勢いで大きければ、
(1+1/3x_1)…(1+1/3x_s) はほとんど 1 に等しいのだから、もはや
(1+3/t)^t < (1+1/3x_1)…(1+1/3x_s)
なんて成り立たないでしょ。

522:righ1113 ◆OPKWA8uhcY
16/06/28 20:29:39.54 QhVmHp3u.net
そうですか……
ありがとうございます……

523:１３２人目の素数さん
16/06/28 20:42:18.49 7Qb0mD6N.net
>>503
より詳しく説明しよう。
もし発散する初期値が存在するならば、次が成り立つことが証明できる。
∀ε＞0, ∃x_0 s.t.
x_0は発散する初期値であり、かつ (1+1/3x_1)…(1+1/3x_s) ＜ 1＋ε (s∈N).
このことから、(1+1/3x_1)…(1+1/3x_s) を統一的に下から押さえることができる定数は
「 1 」しかないことが分かる。つまり、x_0が発散する初期値ならば、
1 ＜ (1+1/3x_1)…(1+1/3x_s) (s∈N)
が成り立つということ。しかし、この不等式は自明なので、何の役にも立たない。
結局、この方針では原理的に不可能。

524:１３２人目の素数さん
16/06/28 21:02:38.37 pww1LGSL.net
ん～識者乱入か？
俺じゃよくわからんし勘違いを防ぐためにも
なるべくCoqで証明を通してほしいよね。

525:righ1113 ◆OPKWA8uhcY
16/06/28 21:52:49.95 QhVmHp3u.net
もしちゃんとZs < Ys <= Xs < ysB * 2^(pys+2) < 8Zs
が言えたら、
　　　Zsと8Zsのずれは3で、これがずっと変わらない
って無限大までいっても変わらないって事だから
xsが発散してもずれは3以下なんだと、今気づかせてもらった。
という訳で、無限大に発散する方はあきらめます。
4-2-1以外のLoopがない方に注力します。

526:１３２人目の素数さん
16/07/08 20:24:43.51 yhL7LYLZ.net
>>1はいまどうしてるの？
まだ頑張ってんの？
それとも休憩中？

527:righ1113 ◆OPKWA8uhcY
16/07/09 09:54:12.67 3emnwfEb.net
>>489の状態遷移図の穴が埋められないんです。
ちょっと休憩中です。

528:tai
16/07/09 14:00:47.29 vr192zDG.net
８っつぐらい問題解いた
URLﾘﾝｸ(taibuturi.fuma-kotaro.com)

529:１３２人目の素数さん
16/07/09 19:28:48.04 xlO52T1E.net
＞>>489の状態遷移図の穴が埋められないんです。
穴は埋まらないよ。この方針じゃ原理的に不可能。
なんで分からないのかなあ。>>506のときみたいに
「これじゃ本質的にダメなんだ」って心の底から悟れよ。
ダメなんだよこれじゃ。ダメなの。このやり方じゃ解けないの。

530:１３２人目の素数さん
16/07/09 19:38:05.16 9+qw8rwI.net
本質的に解けないことちゃんと数学的に証明をしてあげないと。
頭ごなしに否定するだけじゃ納得するはずないでしょ。

531:１３２人目の素数さん
16/07/09 20:14:55.98 xlO52T1E.net
>>511
数学的に証明するのはムリ。
しかし、ほぼ確実な状況証拠はある。
3n＋1版ではなく、an＋1版のコラッツ予想を考える(ただしaは7以上の奇数)。
この場合、ほとんどの初期値でコラッツの軌道が発散することが予想されている。
軌道上に出現する各々の値の偶奇を0,1で横一列に並べると、
どうもその列は、ほとんどの初期値で2進正規になっているように見える。
もし2進正規になってることが証明できたならば、コラッツ予想でおなじみの
「軌道上では偶数と奇数が1/2ずつの確率で出現しそう」というヒューリティクスが
実際に正しいことが分かり、「ほとんどの初期値で発散する」という予想も正しいことが確定する。
おそらく、コラッツの軌道は本質的にランダムになりたがってる。
もともとの3n＋1版でも同じことで、やはりランダムになりたがってる。
しかし、こちらの場合は掛ける数が「3」であるがゆえに、十分大きな数になれず、
それゆえに自由度が低下し、途中で不完全燃焼を起こしてループに陥る。
が、それまでの間はランダム列に近づきたがっている。初期値を大きく取れば取るほど、
ランダム列に近づきたがる期間も長くなるので、その間で幾らでも抜け穴となるパターンが生じうる。
だから本質的にムリなのだ。(続く)

532:１３２人目の素数さん
16/07/09 20:20:54.10 xlO52T1E.net
(続き)
ライトエッジの「抜け穴」と似たような現象は、以下の箇所にも見られる。
英語版のコラッツ予想の記事を見ると、
＞In particular, Krasikov and Lagarias showed that the number of integers in the interval [1,x]
＞that eventually reach one is at least proportional to x^0.84.[19]
という記述がある。区間[1,x]に属する自然数のうち、コラッツの変換によって1になる数の比率は、
少なくとも x^{0.84} はある、という驚くべき文章である。
文献[19]をかいつまんで説明すると、「コラッツの変換によって1になる自然数の集合」を、
ある種のパラメータで分割して、いくつかの集合に分けるところから始まる。
それらの集合の間に定まる漸化式を使って、x^{0.84}という評価を得ている。
この漸化式が完全に制御できれば、もっといい結果が出るわけだが、
漸化式がイジワルな形をしており、漸化式を展開するたびにランダム性が増してしまって制御できなくなる。
そこで、途中で評価を落として不等式の形にすることで、不等式の左辺と右辺に何とかパターン性を
出現させ、それによって問題を対処する。その結果、x^{0.84} という中途半端な数字になってしまう。
ライトエッジの抜け穴は、この「評価を落としてパターン性を出現させる」ところに
どことなく対応しているように見える。ライトエッジを完全に解析すると、まず間違いなく、
そのパターンは有限通りには収まらず、複雑な形の漸化式で記述されることになる。
その漸化式を展開するたびにランダム性が増してしまい、結局は制御できなくなる。
逆に、もしライトエッジが有限通りに収まったら、文献[19]の漸化式も実際には
上手くパターンに落とし込めることになると予想される。が、今のところそういう話は見てないし、
[19]を読んで漸化式を触ってみても、もう本能的に「こりゃムリだわ」っていう感想しか出てこない。
そんなわけで、ライトエッジの方針もムリに決まってるのだ。

533:１３２人目の素数さん
16/07/09 20:34:04.39 xlO52T1E.net
(補足)
結局、>>512の話でも、>>513の話でも、
コラッツの変換を深く深く弄れば弄るほど、
ランダム性が増していく感触が確かな手ごたえとして観測される。
どこまでいっても、パターンに収まってくれる気配が全く出てこない。
「本質的にランダムになりたがっている」としか思えないのだ。
また、コラッツ予想の難しさはまさにこの部分にあるはずだ。
>>488にも書いたが、コラッツ予想に取り組むなら、
「ランダムになりたがってる」という感触を
どうやって解析したらいいかを真正面から考えるしかないだろう。
そして、そのこと自体が既に難しく、だからこその未解決問題なのだろう。

534:１３２人目の素数さん
16/07/09 20:42:03.84 9+qw8rwI.net
ほほう。
あんたプロなの？

535:１３２人目の素数さん
16/07/10 01:04:15.98 p/ut3oXY.net
コラッツ予想で毎回思うんだけど
プログラムでいうif文を扱える数学って存在すんのかなあ

536:vote!
16/07/10 15:45:06.70 JC40fYH1.net
ifを扱える数学というか、プログラムの停止問題は解けないでそ。

537:１３２人目の素数さん
16/07/11 21:08:26.81 DZ0KCN8E.net
Coqでコラッツの予想を厳密に定義するとどんな感じになるの？

538:１３２人目の素数さん
16/07/11 22:30:49.04 DZ0KCN8E.net
有限回繰り返したときってCoqでどうやって表現すりゃいいんだ？

539:righ1113 ◆OPKWA8uhcY
16/07/12 22:09:14.33 5e2oe2Qm.net
>>518-519
Coqでは止まらない再帰関数は書けないので、
>>373では、再帰を有限回で0終了させる引数yを入れてあります。
で、どんなxに対してもlast collatz03が0にならないyが存在する、という事で、
Require Import List.して
Theorem collatz_is_true:
forall (x:nat), x<>0 -> (exists y:nat, 1=(last (collatz03 x y) 0)).
ってとこじゃないでしょうか。

540:１３２人目の素数さん
16/07/12 22:37:31.84 q0MU/n7u.net
うーんyで適用回数制限してんの？
止まらない再帰かけないってのも不便だな。
本質的には問題に成らんのかな

541:righ1113 ◆OPKWA8uhcY
16/07/12 22:53:05.49 5e2oe2Qm.net
Coqの仕様なんでなんとも……
>>520でコラッツの定義としては問題ないと思います。

542:１３２人目の素数さん
16/07/12 23:04:16.21 q0MU/n7u.net
>>522了解です。
ありがとう。

543:成清愼
16/07/16 07:54:51.11 bMeRtupm.net
URLﾘﾝｸ(koubeichizoku.ix-web.tk)
修正いたしました。当板の諸兄におかれましては何卒よろしくご査収の上
ご批評賜りたく、よろしくお願い申し上げます。

544:righ1113 ◆OPKWA8uhcY
16/07/18 02:49:08.81 9Ln5vaRN.net
まず、x0の範囲を8bit以上から15bit以上に変更します。
これで、Xsが1ステップ進むごとに約0.585プラスされます。
禁止パターンは以下です。
・00
・111
・11011
・0101010
・11 01011 01011 01011

545:righ1113 ◆OPKWA8uhcY
16/07/18 02:53:42.18 9Ln5vaRN.net
以下のシミュレーションをおこないます。
【シミュレーションA】
1.7ビットの初期値x0A=1111111を用意する。
2.x0Aを下位へ1ビットシフトして（末尾は捨てる）、x0Aに加える。
3.最下位ビットに1加える。（下位からの繰り上がりが常に有る事を想定）
4.n+1ビットになっていたら、最下位ビットを捨ててnビットにする。
5.2~4を繰り返す。
得られる値をxsAとする。
xsAのライトエッジパターンは17区切りで以下になりますが、
[0,#1,1,0,1,0,1,1,0,1,0,1,1,0,1,0,1,0]
1個左にずらして01101011010110101の繰り返しとします。
それに合わせて、X0のライトエッジパターンも0と定義して、0ステップ目から17区切りにします。
（もしX1が0なら従来通り1ステップ目から始めます。）

546:righ1113 ◆OPKWA8uhcY
16/07/18 02:57:33.00 9Ln5vaRN.net
URLﾘﾝｸ(drive.google.com)
xsAは17区切りで1が10個入ります。
17区切りで1が11個入るパターンは禁止パターンなので除外します。
17区切りで1が10個入るパターンは、全部で21個あるのですが、先のライトエッジパターンの操作により、
0始まりのもの8個だけを考えれば良いです。
A1からA8の状態遷移を考えます。どれも0につながるので、この8個で閉じています。
薄い灰色は禁止パターンになるので、遷移できない箇所です。
濃い灰色はXsに0.585を足していって脱落した所です。
これを元に樹形図を描くと、最長が
A4-A2-A2-A3-A3-A1-A8-A8-A7-A7-A6-脱落　の17*12ステップですが、
A2-A2-A3-A3　と　A8-A8-A7-A7は脱落するので、
A4-A2-A2-A3-A1-A8-A8-A7-A6-脱落　の17*10ステップが最長となります。
これは、170ステップ以内で、17区切りで1が9個入るパターンが現れる事を意味しています。

547:righ1113 ◆OPKWA8uhcY
16/07/18 03:02:47.11 9Ln5vaRN.net
xsAのライトエッジパターンに手を加えます。
170ステップごとに0を挿入します。
これをおこなっても先の議論より、
Xs < xsA*2^pxs　（2^pxsはXsより十分右へ離す定数）が言えます。
170ステップごとに0を挿入した事により、xsAの傾きが変わります。
挿入する前は10/17=0.58823… > log(3/2)ですが、
挿入後は100/171=0.58

548:479… < log(3/2)です。グラフでは、「左端を伸ばすパターン」<「コラッツパターン」<「xsA」と並んでいますが、 xsAの傾きがlog(3/2)より小さい為、順序が逆転し、矛盾します。この矛盾を回避するには、順序が逆転する前に、コラッツ値が1になるしかありません。

549:righ1113 ◆OPKWA8uhcY
16/07/18 03:50:24.14 9Ln5vaRN.net
書いてみて分かったんですが
ちょっとダメみたいです。お騒がせしました。

550:righ1113 ◆OPKWA8uhcY
16/07/18 11:28:23.95 9Ln5vaRN.net
状態遷移図を修正しました。
before:A1＼after:A1で結果がA8になっているのは、
A1からA1に遷移させるつもりだったけど、実際に計算してみるとA8に遷移してた、ということです。
あと、A4-A2-A2の遷移はA4-A2-A3になってしまうので、
A4-A2-A3-A1-A8-A8-A7-A6-D1　の17*9ステップが最長となります。
実はもう一つ問題があるのですが、それは後で書きます。

551:righ1113 ◆OPKWA8uhcY
16/07/18 13:43:41.26 9Ln5vaRN.net
A6-D1-A1-A8と遷移したとします。
D1の末尾は0なので、A1～A8に繋げる事ができません。
そこで11を挿入します。（1じゃないのは0101010回避のため）
次にA1を普通にやって、A8の先頭で、コラッツパターンの右端を2つ左にずらします。
これで11と相殺されます。
このときのA8のライトエッジパターンは[-2,1,0,1,1,0,1,0,1,1,0,1,0,1,0,1,1]
と書いても良いかもしれません。
これで「左端を伸ばすパターン」<「コラッツパターン」<「xsA」の関係も維持されます。

552:tai
16/07/18 15:08:39.36 10r4gZiw.net
2bitで計算して
coqで確認
というのは
どちらかというと
ありそうな証明です
頑張ってください

553:righ1113 ◆OPKWA8uhcY
16/07/18 15:18:39.40 9Ln5vaRN.net
ありがとうございます。励みになります。

554:１３２人目の素数さん
16/07/18 21:31:58.47 XgyK6DxB.net
全てのnに対して2^n-1がコラッツの予想成り立つことは示せないかな。

555:１３２人目の素数さん
16/07/18 21:42:48.17 ltHytvK0.net
数学的帰納法でいけるんじゃね
適当だけど

556:１３２人目の素数さん
16/07/18 21:53:16.94 XgyK6DxB.net
>>535
まじで。
>>1の言うようにビットパターンをセルオートマトンとみなすと
無限大に発散する数というのは自己複製型みたいになるのかな？

557:１３２人目の素数さん
16/07/18 21:54:40.85 ltHytvK0.net
いけんかったわ
すまんまん

558:righ1113 ◆OPKWA8uhcY
16/07/19 05:22:17.53 /x3cNL5P.net
>>531
ちょっと変えます。
A6-D1-A1と遷移したとします。
D1の末尾は0なので、A1～A8に繋げる事ができません。
そこで、適当な後方から11を借りてきます（1じゃないのは0101010回避のため）。
貸した部分まで来たら、また後方から11を借ります。
D1が現れるごとに借りる個数は増えていきますが、コラッツパターンは無限に続くという仮定の元でおこなっているので、問題ないです。
また、11を前方へ移動させているだけなので、ライトエッジパターンの総量はかわらず、
「左端を伸ばすパターン」<「コラッツパターン」<「xsA」の関係も維持されます。

559:１３２人目の素数さん
16/07/19 10:40:37.10 hOf9e9qx.net
まだナントカパターンでやってるのか。頭の悪い奴だな。
左端を延ばすパターンでも、ライトエッジパターンでも、
2進法で表された何らかの数の、左端と右端の数桁だか数十桁だかの
固定された桁数しか見ていない。そのような固定された桁数では、
絶対にパターンに嵌まらないイレギュラーなパターンが出てくる。
それらのパターンまで取り込むと、既存の桁数では足りず、
確認すべき桁数を拡張しなければならない。
＞そこで、適当な後方から11を借りてきます（1じゃないのは0101010回避のため）。
この部分は、まさに桁数を拡張していることに対応する。
そして、この作業は終わらない。すなわち、有限個のパターンでは収まらない。
一般的に記述すると、漸化式の形で延々と続くような記述になってしまう。
その漸化式は、次の項に進むごとに、2進法で表された数の中心に向かって、
左端と右端からどんどんと桁数が侵食されていくような形式になるはず。
＞D1が現れるごとに借りる個数は増えていきますが、コラッツパターンは無限に続くという仮定の元でおこなっているので、問題ないです。
この部分は、まさにこのことを示唆している。
そして、一般的に記述した漸化式を解析することは、もともとのコラッツの問題と
同程度もしくはそれ以上に難しい。よって、この方法では無理。
righ1113 ◆OPKWA8uhcY は、桁の計算をいつもいつも概算で済ませて「問題ないはず」と発言し、
そのたびに、後になって修正するのを繰り返しているが、要するに、
桁の計算は概算で済ませてはいけないのである。いい加減にコイツは気づくべきである。
概算で済ませず、厳密に計算してみろ。
有限個のパターンでは収まらず、漸化式の形で延々と続くような記述にしかならないはずだ。
そして、その漸化式は複雑すぎて手に負えず、この方針では解けないのだ。

560:１３２人目の素数さん
16/07/19 17:16:33.31 HatOoCps.net
仮に全ての奇数で成立することが証明できれば全ての整数で成り立ちますか？

561:534
16/07/19 20:46:50.47 epF0+HEh.net
>>1さんよ
とりあえず目標を>>534まで落としてみないか？
これでも十分難しいぞ？
Coqスレの147あんたじゃろ？
あの時は目標を落としたことで前に進んだじゃろ？
ちなみにCoqスレの148は俺じゃから。
まあ考えてみてくれ。

562:righ1113 ◆OPKWA8uhcY
16/07/20 02:31:18.77 BzZgXVUi.net
ありがとうございます。考えてみます。

563:righ1113 ◆OPKWA8uhcY
16/07/20 14:58:08.77 33UAumcc.net
調べた所、1000000009151が241ステップと長めだったので、計算してみました。
URLﾘﾝｸ(drive.google.com)
状態遷移は上手くいっているみたいです。
11の貸し借りも出来ているんですけど、、貸す所と借りる所がかぶらなかったので、あまり参考になりませんでした……

564:righ1113 ◆OPKWA8uhcY
16/07/20 15:04:00.42 33UAumcc.net
11の貸し借りでかぶるとどうなるかを見るために、
100ステップずつ11を借りる例を考えてみます。
借りる先は2乗ステップ目です。
・100ステップ目で10000ステップ目から11を借りる
・200ステップ目で40000ステップ目から11を借りる
……
・10000ステップ目で貸した11の穴埋めと、新たな11を10^8ステップ目から借りる
・40000ステップ目で貸した11の穴埋めと、新たな11を16*10^8ステップ目から借りる
……
・10^8ステップ目で計111111を、10^16ステップ目から借りる
・16*10^8ステップ目で計111111を、16^2*10^16ステップ目から借りる
……
貸す所が010101…になっている場合もあるので、実際は倍の長さが必要ですが、
それでも、「借りる11…が次のゾーンにひっかかる」というような事は起きません。
この作業に終わりはないのですが、この作業の途中で、
傾きの影響で、左端を伸ばすパターンとxsAの順序が逆転して矛盾します。

565:righ1113 ◆OPKWA8uhcY
16/07/20 16:53:11.61 33UAumcc.net
式で書くと、
100^(2^n-1)ステップで"11"*n*2を100^(2^n)ステップから借りる時、
次のゾーンまでは少なくとも200*100^(2^n-1)空いているから、
2*n*2 < 200*100^(2^n-1)が言えて、次のゾーンにはかからない。です。

566:righ1113 ◆OPKWA8uhcY
16/07/20 17:38:16.68 33UAumcc.net
修正します。
式で書くと、
100nステップで"11"*(log(4√n)+1)*2を(100n)^2ステップから借りる時、
次のゾーンまでは少なくとも200*100(n-1)空いているから、
2*(log(4√n)+1)*2 < 200*100(n-1)が言えて、次のゾーンにはかからない。です。

567:righ1113 ◆OPKWA8uhcY
16/07/20 18:24:37.15 33UAumcc.net
再修正します。
式で書くと、
100nステップで"11"*[(log(4√n)+1)]*2を(100n)^2ステップから借りる時、
(100(n+1))^2 -(100n)^2
=(10000(n+1)^2) -10000n^2
=10000n^2 +20000n +10000 -10000n^2
次のゾーンまでは少なくとも20000n空いているから、
2*[(log(4√n)+1)]*2 < 20000nが言えて、次のゾーンにはかからない。です。

568:righ1113 ◆OPKWA8uhcY
16/07/21 04:10:50.80 gnqJHnrj.net
>>540
全ての偶数は、2で割る事を繰り返せば奇数にたどり着くから、
全ての奇数で成立することが証明できれば、全ての自然数で成り立ちます。
全ての整数で成り立つかどうかは分からない。

569:righ1113 ◆OPKWA8uhcY
16/07/21 05:34:29.16 gnqJHnrj.net
>>541
2^n-1は、2進数で表すと1111…ですね。
試しに3(11)でおこなうと、次ステップは5(101)になります。
7(111)でおこなうと、次ステップは11(1101)になります。
5と11の関係は、101を右シフトして+1しているので、5*2+1=11です。

そこで、次の命題1を考えます。
・x以下で1にたどり着けば、2x+1以下も1にたどり着く

570:righ1113 ◆OPKWA8uhcY
16/07/21 05:36:06.86 gnqJHnrj.net
次に、次の命題2を考えます。
・x以下で1にたどり着けば、4x+2以下も1にたどり着く

まず、これをすべての偶数で証明します。
・2以下の偶数で1にたどり着けば、4*2+2=10以下の偶数も1にたどり着く　は真です。
・x以下の偶数で1にたどり着けば、4*x+2以下の偶数も1にたどり着く　を真としたとき、
x+2は2で割れるので、(x+2)/2 < x、
4*(x+2)+2も2で割れるので、2*(x+2)+1 < 4*x+2、よって
・x+2以下の偶数で1にたどり着けば、4*(x+2)+2以下の偶数も1にたどり着く　も真で、数学的帰納法で証明されました。

571:righ1113 ◆OPKWA8uhcY
16/07/21 05:38:32.36 gnqJHnrj.net
次に、命題2を奇数で証明したいので、2倍した偶数を考えます。
xを例にとると、xを2倍して、
・2x以下の偶数で1にたどり着けば、4*2x+2以下の偶数も1にたどり着く
2で割って
・x以下の数で1にたどり着けば、4*x+1以下の数も1にたどり着く

4*x+1 > 2*x+1なので、命題1
・x以下で1にたどり着けば、2x+1以下も1にたどり着く
も証明されました。
これで、5(101)->11(1101)->23(11101)->……が1にたどり着くことが証明できたので、
2^n-1も1にたどり着くことが証明できました。
>>534さん、これどうですかね。

572:righ1113 ◆OPKWA8uhcY
16/07/21 06:26:46.30 gnqJHnrj.net
ダメっぽい…・・・

573:righ1113 ◆OPKWA8uhcY
16/07/21 20:18:12.98 BLLqljYR.net
しばらくお休みします。

574:１３２人目の素数さん
16/07/21 20:33:10.01 t1QOdamn.net
乙カレ～

575:righ1113 ◆OPKWA8uhcY
16/08/31 04:00:14.65 CWBtxhlC.net
いまひとつ再開する気が起きません。
すみません。

576:１３２人目の素数さん
16/09/04 22:26:50.46 tnjLMu2d.net
　　　　　　　　　　　　、､､ , , _
　　　 ,. -┬i＾i､._　　　ｨ`,､,､,､,､,.、'、
.　　 /　　 | | .|=ゞ=､　__ｌ/＼　v~／!|
　　 l.　　　ｌｌ l　＼＼{f∥ミゞ, ,ｨ≪:lf＾i　　　　　　もういい…！
　／ヽ.　　ﾉ｢,ﾄ､｢.lﾍ‐iヾ|rｰ~r〉〉，こlﾚ'
/　　｀ヽ//| ﾄ､ヽｌｲ| |/|{王王王王}ﾄ､
|　　　　ﾚﾆ| lﾆゝ冫! l!L_, , ,ｰ, , , ,_｣ｼ’、　　　　もう…
ヽ　　　 __|ーL|┴＾ｰヽ＞'＾ヾ二三シ´＼＼
　,ゝ,／　 .}二二二二二二二二二ｌヽ.　ヽ＼　　　休めっ…！
l/　|ﾄ､.／´＼　　　　　　　　　　 ||.　レ'´￣｀ヽ
　　||　!　　､＼　　　　　　　　 ||. /　　　　 :|
　　||　|.l lﾞ!.|ｉ |ヽ)　　　　　　　　　 |l/　　　　 /　　休めっ…！
　　||　`ﾍ)U'J　　　　　　　　　　　/-─　　　,ｲ.|
　　||　　　＿　　　　　　　　　 /-─　　　/ ヽ|　　　太郎っ…！
　　||　 r‐-ﾞ=っ｀ヽ,.--r-─ ''"´￣｀ヽ　　 /　　 }
　　||.　{三二　　 |　│　　　　　　　　　 /　　 /
　　||.　ヾ＝--一'`ーゝ　　　　　　 _,. く　ノ|

577:righ1113 ◆OPKWA8uhcY
16/09/14 15:41:14.53 YiRX+BJ9.net
再開ではないですが、気になっている事があります。
x0から始まるコラッツ列が無限大に発散するとき、以下の式は成り立つのでしょうか。
lim[s->∞](1+1/3x_1)…(1+1/3x_s) > lim[y->∞](1+1/y)^y ≒ 2.718
自分としては、各x_sが定数な分だけ、左辺が大きいと思うのですが……

成り立つとすると、>>504と矛盾するのではないかという気がします。
（ε=0.1とおいて、有限積では1.1を越えないのに、無限積にすると2.718を超える）

自信がないので、ご意見お待ちしています。

578:１３２人目の素数さん
16/09/14 21:38:55.68 42EFYQdO.net
各x_sが定数ってどういうこと？
x_sはsが増えるにしたがって大きくなるじゃねーの？

579:righ1113 ◆OPKWA8uhcY
16/09/14 22:20:57.91 KaaHqR5J.net
左辺はsが増えても、それ以前の項のx_sは変わらないという意味で定数と書きました。
一方右辺はyが増えると、初項から全てのyが増加します。

580:１３２人目の素数さん
16/09/14 23:06:47.15 42EFYQdO.net
よくわからんが無限和が有限になることもあるように無限積も有限になる可能性がある？

581:righ1113 ◆OPKWA8uhcY
16/09/15 01:32:11.84 4GoSOaRl.net
無限積も有限になる可能性があるというのは、
lim[y->∞](1+1/y)^y ≒ 2.718
からも明らかです。
問題はこれより左辺
lim[s->∞](1+1/3x_1)…(1+1/3x_s)
が大きいと思われる事です。

582:１３２人目の素数さん
16/09/15 20:20:12.11 1hPVzgzD.net
定数だからって理由だけでは大小は決められないでしょ。
積の形だから惑わされるんじゃない？

おれもあんまり自信ないが
両辺logとって和の形にすればx_sになんらかの制限がなければ
大小は論じられないという結論になりそうな気がする。

583:righ1113 ◆OPKWA8uhcY
16/09/15 22:49:08.11 rOYm3tIQ.net
ダメって事でしょうか？
う～ん……

次ページ