12.5 Lempel–Ziv 符号

ここまでの符号は，どれも定義 12.1.1 の枠組みの中にあった．分布の族が与えられていて，そのどれが真かだけが分からない，という設定である．冗長度もミニマックス冗長度も，その族に対して定めた量だった．本節はその枠組みを離れる．前節の終わりに立てた問い，すなわち記憶のある情報源に対して，族を用意せずに $1$ 文字あたりの符号長をエントロピーレート（定義 3.2.1）まで下げる符号があるか，に答えるためである．定義 12.1.1 の族の分布はどれも $1$ 文字ずつの積なので，記憶のある情報源は，族をどう取り替えてもそこには入らない．そこで情報源の分布を持ち出さず，手元にある一本の系列だけを見て符号を作る．手がかりにするのは，系列の中で同じ並びが繰り返し現れることである．同じ並びが何度も出てくるなら，二度目からはその並びを指し示すだけで済む．どこがどう繰り返しているかは，分布を知らなくても系列そのものから読み取れる．

作り方はこうである．系列を先頭から読み，これまでに切り出した断片のどれとも違う並びが現れたところで区切り，その断片を辞書に加える．次からは辞書にある断片を足がかりにできるので，同じ並びが何度も出てくる系列では，断片がだんだん長くなり，本数が減っていく．断片の本数が減れば，それを書き並べるビット数も減る．これが 1978 年に提案された方式（LZ78 と呼ばれる）で，本書では Lempel–Ziv 符号 と呼ぶ．本節は分解の性質を三つ（フレーズが相異なること，長さの総和，本数の範囲）押さえ，そこから符号長を定めて評価する．

先に断りを一つ置く．本節が「符号長」と呼ぶのは，分解から決まるビット数のことである．12.2 節で述べた本章の方針では，長さの組が Kraft の不等式（定義 4.2.4）を満たすことを確かめたうえで，その長さをもつ符号の存在を定理 4.2.2 に任せてきた．本節が定めるビット数については，その不等式を本書では確かめない．以下の評価はそのビット数についてのものであって，それを符号語長とする符号が読む側で復号できることまでは述べていない．

道具を一つ借りる．実数 $𝑡$ に対し， $𝑡$ 以下の最大の整数を $⌊ 𝑡 ⌋$ と書き，床関数と呼ぶ．床関数について $⌊ 𝑡 ⌋ \leq 𝑡 < ⌊ 𝑡 ⌋ + 1$ が成り立つこと，および $𝑠 \leq 𝑡$ ならば $⌊ 𝑠 ⌋ \leq ⌊ 𝑡 ⌋$ であることを既知とする．当てる相手は，補題 12.5.6 の証明で対数の値を整数に切り下げるところ，定義 12.5.9 の符号長，定理 12.5.10 の証明で二つの床関数の値を比べるところ，そして系 12.5.12 の証明で $⌊ 𝑡 ⌋ \leq 𝑡$ を使うところである．第14章 14.2 節命題 14.2.3 の証明も，時分割の切れ目 $⌊ 𝜆 𝑛 ⌋$ を評価するのにこの宣言を引く．ただしあちらが引くのは挟み撃ちの不等式のほうだけで，単調性は使わない．

系列を分解する

定義 12.5.1（最長一致の貪欲な分解）. $X$ を空でない有限アルファベット， $𝑥$ を $X$ の文字を並べた有限列とする．辞書を空の並び，区切り候補 を空列として始め， $𝑥$ の文字を先頭から $1$ つずつ読む．読んだ文字を区切り候補の末尾に足した列を $𝑤$ とし， $𝑤$ が辞書にあれば区切り候補を $𝑤$ に置き換え， $𝑤$ が辞書になければ $𝑤$ を フレーズ として出力したうえで辞書の末尾に加え，区切り候補を空列に戻す． $𝑥$ を読み終えた時点で区切り候補に残っているものは出力しない．出力されたフレーズを出力順に並べた列を $S (𝑥) = (𝑠 1, \dots, 𝑠 𝑘)$ と書き，その項数 $𝑘$ を $| S (𝑥) |$ と書く． $S (𝑥)$ を $𝑥$ の 最長一致の貪欲な分解 と呼ぶ．

形式化: lz78PhraseStrings (ソース)

定義 12.5.1 の分岐をそのまま読むと，区切り候補は辞書にある列である限り伸び続け，辞書から外れた瞬間に区切られる．すなわち区切り候補は，つねに空列であるか辞書にある列であるかのどちらかで，出力されるフレーズは「辞書にある列（または空列）に $1$ 文字足したもの」である．最長一致という名前は，区切る前に候補をできるところまで伸ばす，というこの動きから来ている．読み終えたところで候補に残った切れ端を出力しないので，フレーズを全部つないでも $𝑥$ に届かないことがある．そのぶんが命題 12.5.4 の「以下」である．ただし，この切れ端も空列であるか辞書にある列であるかのどちらかだから，フレーズの並びに加えて，切れ端が辞書の何番目かを最後にもう一つ書き添えれば， $𝑥$ 全体が読み取れる．書き添えないと $𝑥$ は決まらない．たとえば $𝑥 = 10$ と $𝑥 = 101$ は，どちらも分解が $(1, 0)$ で，違いは切れ端が空列か $1$ かというところにしかないからである．

例 12.5.2（ $13$ 文字の二値系列）. $X = {0, 1}$ ， $𝑥 = 1011010100010$ （長さ $13$ ）とすると

S (𝑥) = (1, 0, 11, 01, 010, 00, 10)

であり， $| S (𝑥) | = 7$ ，フレーズの長さの総和は $13$ である．

証明. 定義 12.5.1 の手続きを追う．辞書は空，候補は空列から始まる．第 $1$ の文字 $1$ で $𝑤 = 1$ となり，辞書は空だから $1$ を出力して辞書に加える．第 $2$ の文字 $0$ で $𝑤 = 0$ となり，辞書には $1$ しかないから $0$ を出力して加える．第 $3$ の文字 $1$ で $𝑤 = 1$ となり，これは辞書にあるから候補が $1$ になる．第 $4$ の文字 $1$ で $𝑤 = 11$ となり，辞書に無いから $11$ を出力して加え，候補を空に戻す．以下同様に，第 $5$ ・第 $6$ の文字 $0, 1$ で $01$ を，第 $7$ から第 $9$ の文字 $0, 1, 0$ で $010$ を（ $0$ も $01$ も辞書にあるので候補が二度伸びる），第 $10$ ・第 $11$ の文字 $0, 0$ で $00$ を，第 $12$ ・第 $13$ の文字 $1, 0$ で $10$ を出力する．出力は $7$ 本で，読み終えた時点の候補は空列だから，長さの総和は $𝑥$ の長さ $13$ に等しい． $◼$

形式化上の注記. 具体的な系列を入れて分解を計算した宣言は無い．定義 12.5.1 の形式化 lz78PhraseStrings (InformationTheory/Shannon/LZ78/GreedyLongestPrefix.lean) は，辞書と候補を引数にとる補助関数の再帰としてそのまま計算できる形で書かれている．

例 12.5.2 では， $7$ 本のフレーズのうち $5$ 本が $2$ 文字以上である．辞書が育つほど候補が長く伸びられるようになる，というのが定義 12.5.1 の仕掛けである．逆に，どのフレーズも短いままなら，長さの総和が同じでも本数が増える．本数と長さのこのやりとりが，次の三つの主張で押さえる分解の性質であり，符号長の評価をそのまま決める．

分解の性質

命題 12.5.3. $X$ を空でない有限アルファベット， $𝑥$ を $X$ の文字を並べた有限列とすると， $S (𝑥)$ （定義 12.5.1）のフレーズはどの二つも相異なる．

証明（読んだ文字数についての数学的帰納法）. 「辞書は，そこまでに出力したフレーズを出力順に並べたものに一致する」という不変量を示す． $0$ 文字読んだ時点では辞書も出力も空であり，定義 12.5.1 の二つの分岐のどちらでも保たれる（第 $1$ の分岐は辞書も出力も変えず，第 $2$ の分岐は同じ列 $𝑤$ を両方の末尾に同時に加える）．

フレーズが出力されるのは $𝑤$ が辞書に無いときだけで，そのとき辞書はそれまでに出力したフレーズの全体だから，出力されるフレーズはそれ以前のどのフレーズとも異なる．出力の順に見れば，どの二つのフレーズも相異なる． $◼$

形式化: lz78PhraseStrings_nodup (ソース)

命題 12.5.4. $X$ を空でない有限アルファベット， $𝑥$ を $X$ の文字を並べた有限列とする． $S (𝑥)$ （定義 12.5.1）のフレーズはどれも空列でなく，それらを出力順に連結した列は $𝑥$ の語頭（定義 4.1.2）であり，フレーズの長さの総和は $𝑥$ の長さ以下である．

証明（読んだ文字数についての数学的帰納法）. フレーズが空列でないことは，出力されるのが区切り候補に読んだ文字を $1$ つ足した列だからである．

残りの二つには，「そこまでに出力したフレーズを出力順に連結した列に，その時点の区切り候補をつないだものは，そこまでに読んだ文字を順に並べた列に等しい」という不変量を立てる． $0$ 文字読んだ時点では三つとも空列であり，読んだ文字を $𝑎$ とすると，定義 12.5.1 の二つの分岐のどちらでも保たれる（第 $1$ の分岐は候補の末尾に $𝑎$ を足し，第 $2$ の分岐は候補に $𝑎$ を足した列を出力へ移して候補を空列に戻すので，どちらもつないだ列の末尾に $𝑎$ を足す）．

$𝑥$ を読み終えた時点で不変量を読むと，フレーズを連結した列に最後の区切り候補をつないだものが $𝑥$ に等しい．よって連結した列は $𝑥$ の語頭であり，その長さ，すなわちフレーズの長さの総和は $𝑥$ の長さ以下である． $◼$

形式化: lz78PhraseStrings_forall_ne_nil，lz78PhraseStrings_flatten_prefix，lz78PhraseStrings_total_length_le (ソース)

系 12.5.5. $X$ を空でない有限アルファベット， $𝑥$ を $X$ の文字を並べた長さ $𝑛$ の有限列とすると $| S (𝑥) | \leq 𝑛$ であり，さらに $𝑛 \geq 1$ ならば $| S (𝑥) | \geq 1$ である（ $S (𝑥)$ は定義 12.5.1 の貪欲な分解）．

証明. 上界から見る．命題 12.5.4 よりフレーズはどれも空列でないから，長さはどれも $1$ 以上であり，本数は長さの総和以下である．同じ命題より長さの総和は $𝑛$ 以下だから，本数も $𝑛$ 以下である．

下界に移る． $𝑛 \geq 1$ だから，定義 12.5.1 で最初の文字を読んだ時点で $𝑤$ は $1$ 文字の列になり，そのときの辞書は空だから $𝑤$ は出力される．よってフレーズは少なくとも $1$ 本ある． $◼$

形式化上の注記. 系 12.5.5 の上界に対応する宣言は lz78PhraseStrings_count_le (InformationTheory/Shannon/LZ78/GreedyLongestPrefix.lean) である．下界に対応する宣言は無く，系 12.5.5 に付した証明がその保証のすべてである．二つを一つにまとめた宣言も無いので，形式化ポインタは付けない．

系 12.5.5 の上界は，どのフレーズも $1$ 文字のままだった場合，つまり分解が何も学ばなかった場合の勘定である（実際には命題 12.5.3 よりフレーズは相異なるので， $1$ 文字のフレーズは高々 $| X |$ 本しかなく， $𝑛$ が $| X |$ を超えるとこの上界は達成されない．二値なら $𝑛 \geq 3$ で達成されない）．命題 12.5.4 より長さの総和は $𝑛$ を超えないから，フレーズが長くなればそのぶん本数は減る．次はその減り方を，系列の中身によらない形で押さえる．効くのは命題 12.5.3 の「相異なる」と，命題 12.5.4 の「空列でない」「長さの総和が $𝑛$ 以下」の三つだけで，どんな並びであろうと，相異なる列を何本もそろえるには文字数が要る，という一点に帰する．

フレーズは何本まで作れるか

補題 12.5.6（相異なる列の詰め込み）. $X$ を空でない有限アルファベット， $𝑘 \geq 1$ とし， $𝑠 1, \dots, 𝑠 𝑘$ を $X$ の文字を並べた空でない有限列で，どの二つも相異なるものとすると

𝑘 l o g 2 𝑘 \leq 3 l o g 2 (| X | + 1) 𝑘 \sum 𝑗 = 1 | 𝑠 𝑗 |

である．

証明. $𝑇 : = \sum 𝑘 𝑗 = 1 | 𝑠 𝑗 |$ と置く． $X$ は空でないから $| X | + 1 \geq 2$ であり， $l o g 2 (| X | + 1) \geq 1$ である．また各 $| 𝑠 𝑗 |$ は $1$ 以上だから $𝑘 \leq 𝑇$ である． $𝑘 = 1$ のときは左辺が $0$ で右辺は $0$ 以上だから，以下 $𝑘 \geq 2$ とする．

まず詰め込みを数える． $𝑚$ を $0$ 以上の整数とすると， $X$ の文字を並べた長さ $𝑚$ 以下の列は高々 $(| X | + 1) 𝑚$ 本しかない．実際， $X$ に属さない記号 $*$ を一つ用意し，長さ $𝑚$ 以下の列に，末尾に $*$ を足して長さちょうど $𝑚$ にそろえた組を対応させる．もとの列に $*$ は現れないから，組の最初の $*$ の手前までを読めばもとの列が復元でき，この対応は単射である．行き先は $X$ に $*$ を足した $| X | + 1$ 個の記号を $𝑚$ 個並べた組の全体で，その個数は $(| X | + 1) 𝑚$ である．

次に長さで分ける．

𝑚 0 : = ⌊ l o g 2 (𝑘 / 2) l o g 2 (| X | + 1) ⌋

と置く． $𝑘 \geq 2$ より $l o g 2 (𝑘 / 2) \geq 0$ だから $𝑚 0$ は $0$ 以上の整数であり，床関数の性質と $l o g 2 (| X | + 1) > 0$ から $𝑚 0 l o g 2 (| X | + 1) \leq l o g 2 (𝑘 / 2)$ ，すなわち $(| X | + 1) 𝑚 0 \leq 𝑘 / 2$ である．前段より長さ $𝑚 0$ 以下の $𝑠 𝑗$ は高々 $(| X | + 1) 𝑚 0$ 本，すなわち $𝑘 / 2$ 本以下だから，長さ $𝑚 0 + 1$ 以上の $𝑠 𝑗$ が $𝑘 / 2$ 本以上ある．長さは非負だから

𝑇 \geq (𝑚 0 + 1) \cdot 𝑘 2

である．床関数の性質 $l o g 2 (𝑘 / 2) < (𝑚 0 + 1) l o g 2 (| X | + 1)$ を入れ， $2 l o g 2 (| X | + 1) > 0$ を掛けると

2 𝑇 l o g 2 (| X | + 1) > 𝑘 (l o g 2 𝑘 - 1)

となる．

最後にまとめる． $l o g 2 (| X | + 1) \geq 1$ と $𝑘 \leq 𝑇$ から $𝑘 \leq 𝑇 l o g 2 (| X | + 1)$ である．前段の不等式に足して $𝑘 l o g 2 𝑘 < 3 𝑇 l o g 2 (| X | + 1)$ を得る． $◻$

形式化上の注記. 補題 12.5.6 に対応する宣言として total_length_ge_count_mul_log (InformationTheory/Shannon/LZ78/PhraseCounting.lean) がある．仮定は本文より弱く，本数が $1$ 以上であることを要さない（列が相異なることと空でないことだけを課す）．

形式化上の注記（本節と次節の詰め込みの不等式に共通）. この形の不等式に対応する宣言は， $l o g$ を自然対数にとる．どの不等式も両辺が $l o g$ の $1$ 次なので，底を変えると両辺が同じ倍率で変わり，自然対数で書いた宣言と底 $2$ で書いた本文の主張は同じことを述べている．そのうえで本節の三つ，すなわち補題 12.5.6・定理 12.5.7・系 12.5.12 に対応する宣言は，詰め込みの数え上げの定数を $8 l o g 2 (| X | + 1)$ でとる．本文はこれを $3 l o g 2 (| X | + 1)$ でとるので，宣言はいずれも本文より弱い不等式を述べていることになり，三つとも形式化ポインタは付けない．機械検証が及んでいるのは，定数を $8$ にした形までである．

補題 12.5.6 の読み方は素直である．長さをある値以下に抑えた列は，その値で決まる本数しかないので，相異なる列を多く用意するほど，そのうち長いものの割合が増え，文字数の合計が膨らむ．裏返せば，文字数の合計が $𝑛$ しかないところに詰め込める相異なる列の本数には限りがある．次の定理はこれを分解に当てる．

定理 12.5.7（貪欲な分解のフレーズ数）. $X$ を空でない有限アルファベット， $𝑛 \geq 1$ ， $𝑥 \in X 𝑛$ とすると

| S (𝑥) | l o g 2 | S (𝑥) | \leq 3 l o g 2 (| X | + 1) 𝑛

である（ $S (𝑥)$ は定義 12.5.1 の貪欲な分解）．

証明. $𝑘 : = | S (𝑥) |$ と置くと， $𝑛 \geq 1$ だから系 12.5.5 より $𝑘 \geq 1$ である．命題 12.5.3 よりフレーズはどの二つも相異なり，命題 12.5.4 よりどれも空列でないから，補題 12.5.6 を $𝑠 1, \dots, 𝑠 𝑘$ に当てて

𝑘 l o g 2 𝑘 \leq 3 l o g 2 (| X | + 1) 𝑘 \sum 𝑗 = 1 | 𝑠 𝑗 |

を得る．命題 12.5.4 より右辺の和は $𝑛$ 以下で， $3 l o g 2 (| X | + 1)$ は正だから，主張が従う． $◼$

形式化上の注記. 定理 12.5.7 に対応する宣言として lz78PhraseStrings_mul_log_le (InformationTheory/Shannon/LZ78/PhraseCounting.lean) がある．仮定は本文より弱く，長さが $1$ 以上であること（すなわち $𝑛 \geq 1$ ）を要さない．

系 12.5.8. $X$ を空でない有限アルファベット， $𝑛 \geq 2$ ， $𝑥 \in X 𝑛$ とすると

| S (𝑥) | \leq 6 l o g 2 (| X | + 1) 𝑛 l o g 2 𝑛

である（ $S (𝑥)$ は定義 12.5.1 の貪欲な分解）．右辺の係数は $X$ だけで決まり， $𝑛$ にも $𝑥$ にも依らない．

証明. $𝑘 : = | S (𝑥) |$ と置く． $𝑛 \geq 2$ より $l o g 2 𝑛 \geq 1 > 0$ であり， $| X | \geq 1$ より $3 l o g 2 (| X | + 1) \geq 3$ である．定理 12.5.7 より $𝑘 l o g 2 𝑘 \leq 3 l o g 2 (| X | + 1) 𝑛$ である． $𝑘$ と $\sqrt 𝑛$ の大小で二つに分ける．

$𝑘 \geq \sqrt 𝑛$ の場合を見る． $𝑘$ は整数で $\sqrt 𝑛 > 1$ だから $𝑘 \geq 2$ であり， $l o g 2 𝑘 \geq 12 l o g 2 𝑛 > 0$ である． $𝑘 l o g 2 𝑘 \leq 3 l o g 2 (| X | + 1) 𝑛$ の両辺を $l o g 2 𝑘$ で割ると

𝑘 \leq 3 l o g 2 (| X | + 1) 𝑛 l o g 2 𝑘 \leq 6 l o g 2 (| X | + 1) 𝑛 l o g 2 𝑛

である．

$𝑘 < \sqrt 𝑛$ の場合に移る．補題 1.1.7 の対数不等式 $l o g 𝑡 \leq (𝑡 - 1) l o g 𝑒$ を底 $2$ のもとで $𝑡 : = \sqrt 𝑛$ に当てると $12 l o g 2 𝑛 \leq (\sqrt 𝑛 - 1) l o g 2 𝑒 \leq \sqrt 𝑛 l o g 2 𝑒$ である．ここで $2 l o g 2 𝑒 = 2.885 \dots$ であり， $| X | \geq 1$ より $6 l o g 2 (| X | + 1) \geq 6$ だから， $l o g 2 𝑛 \leq 2 l o g 2 𝑒 \sqrt 𝑛 \leq 6 l o g 2 (| X | + 1) \sqrt 𝑛$ である．両辺に $\sqrt 𝑛 > 0$ を掛けて $l o g 2 𝑛 > 0$ で割ると $\sqrt 𝑛 \leq 6 l o g 2 (| X | + 1) 𝑛 / l o g 2 𝑛$ を得る． $𝑘 < \sqrt 𝑛$ と合わせて主張が従う． $◼$

形式化上の注記. 系 12.5.8 に対応する宣言として lz78PhraseStrings_count_isBigO (InformationTheory/Shannon/LZ78/PhraseCounting.lean) がある．ただしこれは，各 $𝑛$ に長さ $𝑛$ の系列を一つずつ与えた列に対し，フレーズ数が $𝑛 / l o g 𝑛$ の定数倍で抑えられることを述べたもので，本文より狭いところが二つある．一つは係数で，本文は $6 l o g 2 (| X | + 1)$ と具体的に書き，系列の取り方によらないと述べている．もう一つは範囲で，宣言は十分大きい $𝑛$ についての評価であり，本文が $𝑛 \geq 2$ のすべてで述べていることは覆っていない．そのため形式化ポインタは付けない．宣言が使う定理 12.5.7 の形（lz78PhraseStrings_mul_log_le）のほうは系列ごとに成り立つ．機械検証が及んでいないのは，そこから系列に依らない係数を取り出すところと， $𝑛 \geq 2$ のすべてに広げるところである．

系 12.5.8 が言っているのは，分解のフレーズ数が長さに比べて小さい，ということである．系 12.5.5 の $𝑛$ 本という上界に対し， $𝑛$ が大きいところでは $l o g 2 𝑛$ 分の $1$ の水準までしか作れない（短い系列では系 12.5.5 のほうが小さい． $| X | = 2$ なら系 12.5.8 の右辺が $𝑛$ を下回るのは $𝑛 \geq 730$ からで，例 12.5.2 の $𝑛 = 13$ では $33.4 \dots$ 対 $13$ である）．しかもこれは系列の中身によらず，どんな並びに対しても成り立つ．この差がそのまま符号長に効く．フレーズ $1$ 本を書くのに要するビット数は，次の定義で見るとおり $l o g 2 𝑛$ の水準だからである．次はその勘定を最後まで書き下す．

符号長

定義 12.5.9（Lempel–Ziv 符号長）. $X$ を空でない有限アルファベット， $𝑛 \geq 0$ ， $𝑥 \in X 𝑛$ とし， $𝑘 : = | S (𝑥) |$ （定義 12.5.1）と置く． $𝑥$ の Lempel–Ziv 符号長 を

ℓ L Z 𝑛 (𝑥) : = 𝑘 (⌊ l o g 2 (𝑘 + 1) ⌋ + ⌊ l o g 2 | X | ⌋ + 2)

で定める．

形式化: $1$ フレーズあたりのビット数 LZ78Phrase.bitLength (ソース)，符号長 lz78GreedyEncodingLength (ソース)

括弧の中は，フレーズ $1$ 本を書くのに割り当てるビット数である．内訳はこうである．定義 12.5.1 の分岐から読んだとおり，各フレーズは辞書にある列（または空列）に $1$ 文字足したものだった．そこで各フレーズを，足す前の列が辞書の何番目かという番号と，足した $1$ 文字との対で書く．番号のほうは，空列の場合を合わせて $𝑘 + 1$ 通りを区別すればよいので $⌊ l o g 2 (𝑘 + 1) ⌋ + 1$ ビット，文字のほうは $| X |$ 通りだから $⌊ l o g 2 | X | ⌋ + 1$ ビットである．二つを足したものが括弧の中で，どのフレーズにも同じだけ割り当てる（辞書が小さいうちは番号がもっと短く書けるが，本数を掛けたときの見積もりを簡単にするため，最後の大きさにそろえておく）．対の並びを先頭から読めば，番号の指す列に文字を足してフレーズが一本ずつ決まり，辞書もそのつど組み直せるから，フレーズの列はここから復元できる．定義 12.5.1 の直後に見たとおり， $𝑥$ に戻るにはさらに，読み残した切れ端が辞書の何番目かを書き足す必要がある．そのぶんは番号だけで足りるので，フレーズ $1$ 本に割り当てるビット数より少ないが，定義 12.5.9 はこの $1$ 本を数えていない．本節のはじめに断ったとおり，本書はこれらを主張として述べず，証明もしない．以下の評価は，定義 12.5.9 の右辺について述べたものである．

形式化上の注記. 対を固定長のビット列に書く割り当てが一意復号可能であること，すなわちビット列の並びから対の並びが復元できることは，ビット列の並びから符号語の並びが復元できることを述べた uniquelyDecodable_lz78TokenCode と，符号語から対に戻せることを述べた injective_lz78TokenCode (InformationTheory/Shannon/LZ78/ConverseUDObject.lean) の二つを合わせたものである．対の並びから系列そのものが決まる側には単独の宣言が無く，三つの合成で得られる．親の番号と足した $1$ 文字がすべてのフレーズで一致すればフレーズの並びが一致することを述べた lz78PhraseStrings_getElem_eq_of_parentData_eq と，切れ端の番号が一致すれば切れ端が一致することを述べた lz78PhraseStrings_tail_eq_of_tailIdx_eq (InformationTheory/Shannon/LZ78/AsymptoticOptimality/ParentBridgeConverse.lean)，そして命題 12.5.4 に紐付けた lz78PhraseStrings_flatten_prefix (InformationTheory/Shannon/LZ78/GreedyLongestPrefix.lean) の三つである．

定理 12.5.10. $X$ を空でない有限アルファベット， $𝑛 \geq 0$ ， $𝑥 \in X 𝑛$ とすると

ℓ L Z 𝑛 (𝑥) \leq 𝑛 (⌊ l o g 2 (𝑛 + 1) ⌋ + ⌊ l o g 2 | X | ⌋ + 2)

である（ $ℓ L Z 𝑛$ は定義 12.5.9 の符号長）．

証明. $𝑘 : = | S (𝑥) |$ と置くと系 12.5.5 より $𝑘 \leq 𝑛$ である． $l o g 2$ は狭義単調増加で，床関数は $𝑠 \leq 𝑡$ ならば $⌊ 𝑠 ⌋ \leq ⌊ 𝑡 ⌋$ を満たすから $⌊ l o g 2 (𝑘 + 1) ⌋ \leq ⌊ l o g 2 (𝑛 + 1) ⌋$ であり，括弧の中は $𝑘$ を $𝑛$ に取り替えても減らない．括弧の中は正だから， $𝑘 \leq 𝑛$ と合わせて，二つの因子をそれぞれ大きくして主張を得る． $◼$

形式化: lz78_encoding_length_le_n_log_n_plus_const (ソース)

系 12.5.11. $X$ を空でない有限アルファベット， $𝑛 \geq 1$ ， $𝑥 \in X 𝑛$ とすると

ℓ L Z 𝑛 (𝑥) 𝑛 \leq ⌊ l o g 2 (𝑛 + 1) ⌋ + ⌊ l o g 2 | X | ⌋ + 2

である（ $ℓ L Z 𝑛$ は定義 12.5.9 の符号長）．

証明. 定理 12.5.10 の両辺を $𝑛 > 0$ で割ればよい． $◼$

形式化: lz78_encoding_length_per_symbol_le (ソース)

系 12.5.11 の右辺は $𝑛$ とともに増えるので，これだけでは $1$ 文字あたりの符号長が定数で抑えられたことにならない． $𝑘 \leq 𝑛$ で済ませたのが，定数で抑えるという目的には粗すぎたのである（もっとも，短い系列では系 12.5.11 の右辺のほうが小さい． $| X | = 2$ なら，次の系 12.5.12 の右辺を下回るのは $𝑛 \leq 62$ の範囲で，例 12.5.13 の $𝑛 = 13$ では $6$ 対 $8.754 \dots$ である）．定理 12.5.10 と系 12.5.11 をここに置いたのは，フレーズ数の抑えを使わずに系 12.5.5 だけでどこまで言えるかを先に出しておくためで，次はその一段だけを取り替える．定理 12.5.7 のフレーズ数の抑えを定義 12.5.9 に入れ直せば，増える項が消える．

系 12.5.12. $X$ を空でない有限アルファベット， $𝑛 \geq 1$ ， $𝑥 \in X 𝑛$ とすると

ℓ L Z 𝑛 (𝑥) 𝑛 \leq 3 l o g 2 (| X | + 1) + ⌊ l o g 2 | X | ⌋ + 3

である（ $ℓ L Z 𝑛$ は定義 12.5.9 の符号長）．右辺は $X$ だけで決まり， $𝑛$ にも $𝑥$ にも依らない．

証明. $𝑘 : = | S (𝑥) |$ と置くと， $𝑛 \geq 1$ だから系 12.5.5 より $𝑘 \geq 1$ であり， $𝑘 + 1 \leq 2 𝑘$ から $l o g 2 (𝑘 + 1) \leq l o g 2 𝑘 + 1$ である．床関数の性質 $⌊ 𝑡 ⌋ \leq 𝑡$ と合わせると

ℓ L Z 𝑛 (𝑥) \leq 𝑘 l o g 2 𝑘 + 𝑘 (⌊ l o g 2 | X | ⌋ + 3)

である．定理 12.5.7 より第 $1$ 項は $3 l o g 2 (| X | + 1) 𝑛$ 以下，系 12.5.5 より第 $2$ 項の $𝑘$ は $𝑛$ 以下だから，両辺を $𝑛 > 0$ で割れば主張を得る． $◼$

形式化上の注記. 系 12.5.12 に対応する宣言として lz78_rate_le_const (InformationTheory/Shannon/LZ78/AsymptoticOptimality/EncodingLength.lean) がある．仮定は本文より弱く， $𝑛 = 0$ の場合も含めて述べている．

例 12.5.13（ $13$ 文字の二値系列の符号長）. 例 12.5.2 の $𝑥 = 1011010100010$ （ $X = {0, 1}$ ， $𝑛 = 13$ ）に対し $ℓ L Z 13 (𝑥) = 42$ ビットである（ $ℓ L Z 𝑛$ は定義 12.5.9 の符号長）．

証明. 例 12.5.2 より $𝑘 = | S (𝑥) | = 7$ である． $⌊ l o g 2 8 ⌋ = 3$ であり， $| X | = 2$ だから $⌊ l o g 2 2 ⌋ = 1$ である．よってフレーズ $1$ 本あたりのビット数は $3 + 1 + 2 = 6$ で， $ℓ L Z 13 (𝑥) = 7 \times 6 = 42$ である． $◼$

形式化上の注記. 例 12.5.13 は形式化されていない．例 12.5.13 に付した計算が，この主張の保証のすべてである．

$13$ 文字を $1$ 文字 $1$ ビットで書き写せば $13$ ビットで済むから，この系列では Lempel–Ziv 符号のほうが $3$ 倍以上長い．フレーズ $1$ 本に $6$ ビットを払って，覆えているのは平均 $13 / 7$ 文字だからである．短い系列で膨らむのはこのためで，縮むとすれば，辞書が育ってフレーズ $1$ 本の覆う文字数が増えてからである．その育ち方を，同じ文字が続くだけの系列で見ておく．

例 12.5.14（ $0$ だけを並べた二値系列）. $X = {0, 1}$ ， $𝑛 \geq 1$ とし， $𝑥$ を $0$ を $𝑛$ 個並べた列とする． $𝑘 (𝑘 + 1) / 2 \leq 𝑛$ を満たす最大の整数を $𝑘$ とすると， $S (𝑥)$ （定義 12.5.1）は $0$ を $1$ 個， $2$ 個， $\dots$ ， $𝑘$ 個並べた列をこの順に並べたもので， $| S (𝑥) | = 𝑘$ であり

ℓ L Z 𝑛 (𝑥) = 𝑘 (⌊ l o g 2 (𝑘 + 1) ⌋ + 3)

である（ $ℓ L Z 𝑛$ は定義 12.5.9 の符号長）．とくに $𝑛 = 21$ では $𝑘 = 6$ で $30$ ビット， $𝑛 = 54$ では $𝑘 = 9$ で $54$ ビット， $𝑛 = 61$ では $𝑘 = 10$ で $60$ ビットである．

証明. 分解から見る．定義 12.5.1 の手続きを追うと，辞書が $0$ を $1$ 個から $𝑗$ 個まで並べた列からなる状態では，区切り候補は $0$ を $𝑗$ 個読むまで伸び， $𝑗 + 1$ 個目の $0$ で辞書から外れて出力される．よって出力は $0$ を $1$ 個， $2$ 個， $\dots$ と並べた列がこの順に現れ， $𝑗$ 個の列まで出し終えた時点で読んだ文字数は $1 + 2 + \dots + 𝑗 = 𝑗 (𝑗 + 1) / 2$ である． $𝑘$ のとり方より $𝑘 (𝑘 + 1) / 2 \leq 𝑛$ だから $0$ を $𝑘$ 個並べた列までは出力される．残る $𝑛 - 𝑘 (𝑘 + 1) / 2$ 文字が $𝑘 + 1$ 個以上あれば $(𝑘 + 1) (𝑘 + 2) / 2 \leq 𝑛$ となって $𝑘$ の最大性に反するから，残りは $𝑘$ 個以下で，候補に残って出力されない．よってフレーズは $𝑘$ 本である．

ビット数を勘定する． $| X | = 2$ だから $⌊ l o g 2 | X | ⌋ = 1$ であり，定義 12.5.9 の括弧の中は $⌊ l o g 2 (𝑘 + 1) ⌋ + 3$ である． $𝑛 = 21$ では $6 \times 7 / 2 = 21 \leq 21$ かつ $7 \times 8 / 2 = 28 > 21$ だから $𝑘 = 6$ で， $⌊ l o g 2 7 ⌋ = 2$ よりフレーズ $1$ 本あたり $5$ ビット，合わせて $30$ ビットである． $𝑛 = 54$ では $9 \times 10 / 2 = 45 \leq 54$ かつ $10 \times 11 / 2 = 55 > 54$ だから $𝑘 = 9$ で， $⌊ l o g 2 10 ⌋ = 3$ よりフレーズ $1$ 本あたり $6$ ビット，合わせて $54$ ビットである． $𝑛 = 61$ では $55 \leq 61$ かつ $11 \times 12 / 2 = 66 > 61$ だから $𝑘 = 10$ で，同じく $⌊ l o g 2 11 ⌋ = 3$ よりフレーズ $1$ 本あたり $6$ ビット，合わせて $60$ ビットである． $◼$

形式化上の注記. 例 12.5.14 は形式化されていない．例 12.5.14 に付した計算が，この主張の保証のすべてである．

辞書が育つ様子がそのまま数に出ている． $𝑛 = 21$ では $6$ 本のフレーズが $21$ 文字を覆い， $1$ 本あたり平均 $3.5$ 文字で，例 12.5.13 の $13 / 7$ 文字より長い．それでも $30$ ビットかかって，書き写す $21$ ビットには負けている． $𝑛 = 54$ でようやく書き写すのと並び， $𝑛 = 61$ では $60$ ビットで書き写すより短くなる．これだけかかるのは，フレーズ $1$ 本あたりのビット数が本数の対数で増えるいっぽう，この系列で $𝑘$ 本のフレーズが覆える文字数は $𝑘 (𝑘 + 1) / 2$ と，本数の $2$ 乗の水準でしか伸びないからである．縮むところまで持っていくには，同じ文字が続くだけの系列でもこれだけの長さが要る．

系 12.5.12 が抑えたのはそこまでである． $1$ 文字あたりの符号長が定数を超えないことは分かったが，行き着く値が情報源のエントロピーレートかどうかは，ここまでの数え上げでは決まらない．数え上げが見ているのはフレーズが相異なることだけで，どのフレーズがどれだけ起こりやすいかを見ていないからである．次節は，そこに情報源の確率を入れる．

InformationTheory — 形式化検証つき情報理論教科書（レビュー版）．数式は MathJax + AMS Euler で事前レンダリング．