2021-06-02

雑記

キャラクターの原作とは無関係です。お気付きの点がありましたらご指摘いただけますと幸いです。

f:id:cookie-box:20180305232608p:plain:w60

例えば僕たちのカードの中で「焼き芋」に関連するカードを探したいとします。

f:id:cookie-box:20180305231302p:plain:w60

普通にカードっていうな！メタ世界に触れるのやめて！あと焼き芋に関連するカードなんてあるの！？

アイドルマスターsideM Wiki* で確認できるカード 2229 枚（2021-06-02 現在）のうち、アルバムでの台詞（チェンジ前後含む）に「焼き芋」を含むカードは以下の4枚がありました。

【緋色のﾊﾟﾝｸﾛｯｸ】秋山 隼人  
【白狐演舞祭】若里 春名  
【ﾊﾟﾝｷｯｼｭﾗｲﾌﾞ】若里 春名  
【秋の妖魔】水嶋 咲

俺だった！！

さらにハヤトのカードの台詞を調べると以下の44単語から構成されていました（助詞や記号をフィルタリングし、各単語は基本形にしています）。うち「焼き芋」の出現回数は1回でした。

'たち': 3, 'うまい': 2, 'やる': 2, 'たい': 2, 'いただき': 1, 'ま': 1, 'ー': 1, 'す': 1,
'アチチ': 1, '熱い': 1, '焼き芋': 1, 'サイコー': 1, （後略）

焼き芋大絶賛だったな俺！？単語を並べただけで何言ってるかだいたいわかるんだけど…。

なのでこの場合「焼き芋」に対するハヤトのカードの関連度は以下のようになると考えられます。用語は Lucene のドキュメントにしたがいます。

${\rm tf}(t=$ 焼き芋 ${\rm in} \; \, d) = {\rm frequency}^{1/2} = 1$
${\rm idf}(t=$ 焼き芋 $\displaystyle ) = 1 + \log \left( \frac{\rm docCount + 1}{\rm docFreq + 1} \right) = 1 + \log \left( \frac{2229 + 1}{4 + 1} \right) \fallingdotseq 7.100319$
${\rm norm}(t=$ 焼き芋 $\displaystyle , \, d) = \frac{1}{\sqrt{\rm length}} = \frac{1}{\sqrt{44}} \fallingdotseq 0.150756$

つづいたらつづく

2021-06-01

雑記

お気付きの点がありましたらご指摘いただけますと幸いです。

Mehryar Mohri -- Foundations of Machine Learning - Book

f:id:cookie-box:20210304153450p:plain:w60

参考文献1. は序文を読むと、機械学習のトピックを理論的基盤から紹介する本なのですね。但しグラフィカルモデルやニューラルネットについては現状で理論が強固でないので扱わないということですが。本の構成としては最初の3、4章は理論の準備で、その後の各章は一部を除き自己完結していると。以下のような感じですね。

1. イントロダクション／ 2. PAC学習／ 3. VC次元／ 4. モデル選択
5. サポートベクターマシン
6. カーネル法
7. ブースティング
8. オンライン学習
9. 多クラス分類
10. ランキング
11. 回帰
12. 最大エントロピーモデル／ 13. 条件付き最大エントロピーモデル
14. アルゴリズムの安定性
15. 次元削減
16. 学習オートマトンと言語
17. 強化学習

それで各章の章末には演習問題があり、全ての問題に解答を付け…解答！？た、確かに、別冊になっていますが MIT Press というリンク先の Reader Resources から解答をダウンロードできますね！！なんとやさしい世界なのでしょう…私は既にこの本に感動しました…。

f:id:cookie-box:20210304153503p:plain:w60

序文だけで！？

まあそれで、この本は機械学習の色々なトピックや領域に統一的な表現を与えることを目指していて、よくある個別の見方に特化している本とは一線を画しているとありますね。

1章のイントロダクションをみると…この章は本当に導入ですね。あまり初めて聞くようなことはないですが、1.4節の hypothesis set とは候補として考えている関数族、という意味でしょうか。各 hypothesis は関数ですよね。データを示す example とこの hypothesis は例や仮説と和訳すると日常的な意味の例や仮説に聞こえてしまうので英語のままつかいましょうか。そうすると 1.4 節のスパムメール分類の例での学習のステージとは以下の流れですね。

ラベル付きの examples を訓練データ、評価データ、テストデータに分ける。
examples に使用する特徴を関連付ける（学習に有用な特徴を選ぶ必要がある）。
関連付けた特徴でアルゴリズム $\mathcal{A}$ を実行しハイパーパラメータ $\Theta$ をチューニングする。選択された hypothesis が評価データで最もよいパフォーマンスとなった $\Theta_0$ を採用する。
その hypothesis を用いてテストデータのラベルを予測し、アルゴリズム $\mathcal{A}$ の性能を評価する。

1.5 節は学習のシナリオにはどんなものがあるかという話ですね。以下の箇条書きの主語は learner です。まあ機械学習エンジニアとでも想像すればいいと思います。

教師あり学習：ラベル付きの examples を受け取り、任意の未知の点に対する予測を行う。
教師なし学習：ラベルのない examples を受け取り、任意の未知の点に対する予測を行う。クラスタリングや次元削減はこれに該当するんですね。であれば、空間内の任意の点に対して、どのクラスタに所属するかとか、低次元空間のどの点にマッピングされるかとかが決まっていないといけませんよね。しかしクラスタリングや次元削減というと、手元に既にあるデータに対して行う印象がありますが…。
半教師あり学習：ラベル付きの examples とラベルのない examples を受け取り、任意の未知の点に対する予測を行う。例．ラベルなしのデータは容易に手に入るがラベル付きのデータを得るにはコストがかかる場面など。ラベルのないデータの分布が教師あり学習の助けになることが期待されるが、実際にどのような条件下で有効なのかは近年盛んに研究されているとのことです。
トランスダクティブ学習：ラベル付きの examples とラベルのない examples を受け取り、特定のテスト対象の点に対する予測を行う。半教師あり学習より簡単そうにみえるが、半教師あり学習のように、どのような条件で上手くいくかはじゅうぶんには明らかにされていないと。
オンライン学習：学習とテストのフェーズが何ラウンドも繰り返される。各ラウンドでラベルのない訓練データを受け取り、それに対して予測し、真のラベルを受け取り、損失を受ける。全ラウンド通算の損失を最小限に抑えることが目標となる。言い換えると、regret（最も理想的な予測ができた場合との損失の差）を最小限に抑えることを目指すとのことです。
強化学習：これも学習とテストのフェーズが何ラウンドも繰り返される。オンライン学習との違いは行動の結果が環境に影響を与えるということなのでしょうか。なので、まだ結果がわからない行動をとってみるか、既にいい結果だとわかっている行動をとってみるか、探索と利用のジレンマが発生すると。
能動学習：もはや learner が能動的に訓練データを集めると。より少ない examples で教師あり学習と同等のパフォーマンスを達成することを目指すんでしょうか。これもラベル付きのデータが expensive なときにありうるシナリオであるということです。確かに、映画のレビューがポジティブかネガティブかをお金を払ってラベル付けしてもらうなら、どう考えてもポジティブ／ネガティブだろうなというレビューよりも、微妙なレビューにラベル付けしてもらう方がいいですよね。

つづいたらつづく

2021-05-31

雑記：連続的に変化する状態を捉えたい話（仮題）

雑記

キャラクターの原作とは無関係です。お気付きの点がありましたらご指摘いただけますと幸いです。

James Morrill, Cristopher Salvi, Patrick Kidger, James Foster, Terry Lyons. Neural Rough Differential Equations for Long Time Series. arXiv preprint arXiv:2012.07436, 2020.
[2009.08295] Neural Rough Differential Equations for Long Time Series
GitHub - jambo6/neuralRDEs: Code for: "Neural Rough Differential Equations for Long Time Series", (ICML 2021)

論文読みメモ： Latent Ordinary Differential Equations for Irregularly-Sampled Time Series（その1）

微分方程式って何？

$f(t)$ の $n\geqq1$ 次の導関数が満たす等式から $f(t)$ がどんな関数かを求めるような方程式ですね。例えば物理で習った運動方程式は速度（時刻の関数）という未知関数の1次導関数を含む微分方程式と捉えられます。自由落下する物体であったら常に一定の力（重力）がかかるので、その速度を求めるには「微分したら定数になるような関数は何？」という問を考えることになりますよね。これは微分方程式です。

「微分したらこれになる関数は何？」ってことか…でも、それをニューラルネットで時系列を扱うときに利用したいってなる？現状 RNN とか CNN とか Self-Attention とか、「現時点までの入力データから特徴を出力するニューラルネット構造」ってもう十分ある気がするんだけど。それで何か不満があるの？？

そうですね。

時間が連続的で入力が不等間隔であったとします。不等間隔であるともはや入力系列の値が同じでもその意味が同じであるとはなりませんよね。
等間隔であったとしてもです。それらのモデルでは入力がやってくる時刻にしか特徴が出力されませんよね。入力と入力の間の時刻に特徴がどうなっているのかに興味があるとき、それらのモデルは応えてくれません。
さらに時間が離散的であったとしても、それらのアーキテクチャで表現できるのは結局差分方程式になってしまうと思うんです。真の時間発展のメカニズムによっては差分方程式で表現しづらいということはありえます。 $h_t = \sin(t)$ を与える差分方程式を学習するのは面倒そうでしょう？でもそれを与える2階定数係数同次微分方程式ならずっとシンプルです。 $h''(t) = -h(t)$ なので。

すごい不満出たな…それで、参考文献1. の題は直訳すると「長い時系列のためのニューラルで粗い微分方程式」だけど（何が長いんだ？）、アブストラクトをみると Neural Controlled Differential Equations というのが RNN の連続時間のアナロジーで…Controlled 微分方程式？制御微分方程式？って何？？

というのは本文の冒頭に引用（以下）がありますね。数学に元々あった概念ではなくてニューラルネットの文脈で出てきた微分方程式だと思うんです（そうでなかったらすみません）。

[2005.08926] Neural Controlled Differential Equations for Irregular Time Series

参考文献1. の 1.1 節が Controlled Differential Equations なのでここを読めばわかると思います。いま、 $X: [a, b] \to \mathbb{R}^v$ なる有界変動な連続関数があるとします。 $f:\mathbb{R}^w \to \mathbb{R}^{w \times v}$ を連続関数とします。このとき未知関数 $Z: [a,b] \to \mathbb{R}^w$ に関する次の方程式を Controlled Differential Equations というようです。 $\xi \in \mathbb{R}^w$ は $Z$ の境界条件ですね。 $\displaystyle Z_a = \xi, \quad Z_t = Z_a + \int_a^t f(Z_s) dX_s$

$dX_s$ はリーマン・スティルチェス積分です。

待って待って、そもそも $f(Z_s) dX_s$ は行列とベクトルの積なんだな。それでこの $d X_s$ の $X$ は有界変動な連続関数…って？リーマン・スティルチェス積分ってのもわかんないし。普通の積分じゃないの？

1.1節の続きに、 $X$ が（有界変動連続に加えて）微分可能であれば普通の積分になることが示されていますよ。以下のようにかきかえられますので。

$\displaystyle \int_a^t f(Z_s) dX_s = \int_a^t f(Z_s) \left. \frac{d X_r}{dr} \right|_{r=s} ds$ これは何のことはない、数学で習った置換積分ですね。そしてこのとき Controlled Differential Equations は単に常微分方程式になるとあります。 $\dot{Z_t} = f(Z_t) \dot{X_t}$ ですからね。…では、 $X$ が微分可能でなければ積分を考えることなどできないのかというと、そうではありません。

つづいたらつづく

2021-04-19

雑記

お気付きの点がありましたらご指摘いただけますと幸いです。

Haoyi Zhou, Shanghang Zhang, Jieqi Peng, Shuai Zhang, Jianxin Li, Hui Xiong, Wancai Zhang. Informer: Beyond Efficient Transformer for Long Sequence Time-Series Forecasting. arXiv preprint arXiv:2012.07436, 2020.
[2012.07436] Informer: Beyond Efficient Transformer for Long Sequence Time-Series Forecasting
GitHub - zhouhaoyi/Informer2020: The GitHub repository for the paper "Informer" accepted by AAAI 2021.

論文読みメモ： Informer: Beyond Efficient Transformer for Long Sequence Time-Series Forecasting

Transformer は行列 ${\rm Softmax}(QK^\top /\sqrt{d})$ によって入力の特徴系列を「前後の文脈を考慮した」特徴系列に変えますが、系列長 $L$ が長くなるほどこの行列を用意して適用するのに $\mathcal{O}(L^2)$ の計算量がかかってしまうのですよね？文脈を考慮する先が増えるわけですから当然ですが。しかし、それでも何とか計算を間引いて Transformer に長い系列を流したいこともあるわけです。そのような手法としてこれまでどのようなものが提案されてきたのでしょう？それぞれの手法にどのような得手不得手があるのでしょうか？

Transformer の1ヘッドがやること

$x \in \mathbb{R}^{L \times d_{\rm in}}$ を受け取る．
$Q = x W_Q \in \mathbb{R}^{L \times d}$ ， $K = x W_K \in \mathbb{R}^{L \times d}$ ， $V = x W_V \in \mathbb{R}^{L \times d_{\rm out}}$ を計算する．
$y = {\rm Softmax}(QK^\top /\sqrt{d}) V \in \mathbb{R}^{L \times d_{\rm out}}$ を計算する（※ Softmax は各行を正規化する）．

まず Informer [1] の間引き方を復習しようか。考え方としては、 ${\rm Softmax}(QK^\top /\sqrt{d})$ の各行の中で一様分布から逸脱している $u$ 行を残したいんだね。逸脱度の指標は一様分布とその行との交差エントロピーだね（論文では KL 情報量といっているけど定数項を省いているから結局交差エントロピーなんだよね）。

なるほど…一様分布と $i$ 行目の交差エントロピーは、 $i$ 行目の確率分布に最適化した情報量の尺度で一様分布を受け取ったときの平均的な情報量… $Q$ の $i$ 行目 $q_i$ と $K$ の $j$ 行目 $k_j$ を縦ベクトルと考えると、

$\displaystyle {\rm CE}_i = \frac{1}{L} \sum_{j=1}^L \left[ \log \frac{\sum_{j'=1}^L \exp(q_i \cdot k_{j'} / \sqrt{d})}{\exp(q_i \cdot k_j / \sqrt{d})} \right] = \log \left[ \sum_{j=1}^L \exp \left( \frac{q_i \cdot k_j}{\sqrt{d}} \right) \right] - \frac{1}{L} \sum_{j=1}^L \frac{q_i \cdot k_j}{\sqrt{d}}$ ですね。すべての $i$ についてこの ${\rm CE}_i$ を計算してこれが大きい $u$ 行を残せば計算量を節約でき…って、これを計算するのにすべての $q_i \cdot k_j$ が必要ですよね？これでは計算量 $\mathcal{O}(L^2)$ じゃないですか…。

うんだから厳密に ${\rm CE}_i$ を計算するんじゃないんだよね。まず、その式から以下が成り立つことはわかるよね。下限の方は交差エントロピーが最小になるのは $i$ 行目の確率分布が一様分布に一致するときということからわかるし、上限はその行の最大値をつかって抑えただけだし。それでこの最右辺第2項と第3項を $\overline{\rm CE}_i$ とおくみたい。

$\displaystyle \log L \leqq {\rm CE}_i \leqq \log L + \max_j \left[ \frac{q_i \cdot k_j}{\sqrt{d}} \right] - \frac{1}{L} \sum_{j=1}^L \frac{q_i \cdot k_j}{\sqrt{d}}$ $k_j$ が多変量正規分布にしたがうと仮定すると、 $\overline{\rm CE}_i > \overline{\rm CE}_{i'}$ かつ $i$ 行目の分散の方が $i'$ 行目の分散より大きいなら高確率で ${\rm CE}_i > {\rm CE}_{i'}$ になるんだって（正確には「となるような $q_i, q_{i'}$ の領域が存在する」といっているけど）。

…うーんでも、その主張だと結局 ${\rm CE}_i$ と ${\rm CE}_{i'}$ を比較するのに $QK^\top$ の $i$ 行目と $i'$ 行目が完全に必要になりませんか？それでは意味が―

以下の実装をみると $QK^\top$ を完全に計算しているわけではないね。

https://github.com/zhouhaoyi/Informer2020/blob/main/models/attn.py#L47-L68

$QK^\top$ を計算するんじゃなくて、 $K$ のうち sample_k 行だけ残した $K'$ で代用している。いや、正確にいうと、 $Q$ の各行に対して sample_k 行の選び方を変えているから、 $L$ 通りの ${K'}_{1}, {K'}_{2}, \cdots, {K'}_{L}$ を用意して、以下の $QK^\top$ もどきを計算して、これに基づいて $\overline{\rm CE}_i$ が大きい n_top 行を選んでいるね（※ この記事では $Q$ の $i$ 行目を縦ベクトル $q_i$ と考えているから横ベクトルに戻すために転置しているよ）。 $\left( \begin{array}{c} q_1^\top {K'}_{1}^\top \\ q_2^\top {K'}_{2}^\top \\ \vdots \\ q_L^\top {K'}_{L}^\top \end{array} \right)$ それで、一度 n_top 行を選んだら改めてそれらの行に対しては $QK^\top$ をきちんと計算しているよ。実装を抜き出すと以下だね。

Informer のセルフアテンションの間引き方

f:id:cookie-box:20210419234518p:plain:w680

系列長 8 で間引きを発生させるには factor をデフォルト値の 5 より下げないといけない。factor を 2 にすると n_top = 2 * ceil( log(8) ) = 6 になるから、セルフアテンションの計算対象が一様分布から逸脱した 6 行に絞られるよ。上図では 2, 3 行目の計算が間引かれたけど、この 2 行が本当に一様分布に最も近い 2 行だったかは確認していない。

つづいたらつづく

2021-03-29

雑記

クロネッカー積と行列積の混合積の公式 $(A \otimes B)(C \otimes D) = AC \otimes BD$ を成分でかいただけです．

定義1（クロネッカー積）
命題1（クロネッカー積と行列積の混合積の公式）
命題1の証明0（ブロックごとに行列積をとる）
定義1'（クロネッカー積の成分；通常のインデックスでアクセス）
定義1''（クロネッカー積の成分；大インデックスと小インデックスでアクセス）
命題1の証明1（定義1' を使用）
命題1の証明2（定義1'' を使用）
おまけ

まず，クロネッカー積は以下のように定義されると思います．

定義1（クロネッカー積）

$A \in \mathbb{R}^{n_a \times m_a}, \; B \in \mathbb{R}^{n_b \times m_b}$ に対して $A \otimes B \in \mathbb{R}^{n_a n_b \times m_a m_b}$ を以下のように定義する．

$A \otimes B = \left( \begin{array}{cccc} a_{1,1}B & a_{1,2}B & \cdots & a_{1,m_a}B \\ a_{2,1}B & a_{2,2}B & \cdots & a_{2,m_a}B \\ \vdots & \vdots & \ddots & \vdots \\ a_{n_a,1}B & a_{n_a,2}B & \cdots & a_{n_a,m_a}B \end{array} \right)$

それで以下の公式が成り立ちます． $AC \otimes BD$ から $A, B$ を追放したいときなどにこれをつかうと思います．

命題1（クロネッカー積と行列積の混合積の公式）

$A \in \mathbb{R}^{n_a \times m_a}, \; B \in \mathbb{R}^{n_b \times m_b}, \; C \in \mathbb{R}^{m_a \times m_c}, \; D \in \mathbb{R}^{m_b \times m_d}$ に対して以下が成り立つ．

$(A \otimes B)(C \otimes D) = AC \otimes BD$

この公式は以下のように定義にあてはめれば示せます．

命題1の証明0（ブロックごとに行列積をとる）

$\begin{split} (A \otimes B)(C \otimes D) &= \left( \begin{array}{cccc} a_{1,1}B & a_{1,2}B & \cdots & a_{1,m_a}B \\ a_{2,1}B & a_{2,2}B & \cdots & a_{2,m_a}B \\ \vdots & \vdots & \ddots & \vdots \\ a_{n_a,1}B & a_{n_a,2}B & \cdots & a_{n_a,m_a}B \end{array} \right) \left( \begin{array}{cccc} c_{1,1}D & c_{1,2}D & \cdots & c_{1,m_c}D \\ c_{2,1}D & c_{2,2}D & \cdots & c_{2,m_c}D \\ \vdots & \vdots & \ddots & \vdots \\ c_{m_a,1}D & c_{m_a,2}D & \cdots & c_{m_a,m_c}D \end{array} \right) \\ &= \left( \begin{array}{cccc} \sum_{k=1}^{m_a} a_{1,k} c_{k,1} BD & \sum_{k=1}^{m_a} a_{1,k} c_{k,2} BD & \cdots & \sum_{k=1}^{m_a} a_{1,k} c_{k,m_c} BD \\ \sum_{k=1}^{m_a} a_{2,k} c_{k,1} BD & \sum_{k=1}^{m_a} a_{2,k} c_{k,2} BD & \cdots & \sum_{k=1}^{m_a} a_{2,k} c_{k,m_c} BD \\ \vdots & \vdots & \ddots & \vdots \\ \sum_{k=1}^{m_a} a_{n_a,k} c_{k,1} BD & \sum_{k=1}^{m_a} a_{n_a,k} c_{k,2} BD & \cdots & \sum_{k=1}^{m_a} a_{n_a,k} c_{k,m_c} BD \end{array} \right) \\ &= AC \otimes BD \end{split}$

完全に上の証明でいいんですが，より明示的に成分が等しいことに基づく証明もしておきたい気がします．なので，クロネッカー積の定義を成分にかき直します．ちなみに後で気付いたんですが，ここで「これ以降行列のインデックスをゼロ始まりでとることに決める」と宣言しておけばよかったです．以降では右肩に $(0)$ を付けたときにゼロ始まりのインデックスでとるとしていますが証明では全部右肩に $(0)$ が付いています．無駄です．

定義1'（クロネッカー積の成分；通常のインデックスでアクセス）

$x$ を超えない最大の整数を ${\rm floor}(x)$ ， $x$ を $y$ で割った余りを ${\rm mod}(x,y)$ とかくと， $A \otimes B$ の $i, \, j$ 成分は以下のようにかける（ $1 \leqq i \leqq n_a n_b$ ， $1 \leqq j \leqq m_a m_b$ ）．

$(A \otimes B)_{i,j} = a_{\, {\rm floor} ( (i-1) /n_b)+1, \, {\rm floor} ( (j-1) /m_b )+1 \, } b_{\, {\rm mod}( (i-1), n_b) + 1, \, {\rm mod}((j-1), m_b) + 1\, }$

以降，表記の便利のため，右肩に $(0)$ を付けたときはゼロ始まりのインデックスで成分をとることにする．すると以下のようになる（ $0 \leqq i' \leqq n_a n_b - 1$ ， $0 \leqq j' \leqq m_a m_b- 1$ ）．

$(A \otimes B)^{(0)}_{i',j'} = {a}^{(0)}_{\, {\rm floor} (i'/n_b), \, {\rm floor} ( j'/m_b ) \, } {b}^{(0)}_{\, {\rm mod}(i', n_b), \, {\rm mod}(j', m_b) \, }$

上の定義でクロネッカー積の成分にアクセスできると思うんですが， ${\rm floor}$ や ${\rm mod}$ が多用されていてみづらいという声もあると思うので最初から ${\rm floor}$ と ${\rm mod}$ の2重インデックス（行と列があるので4重インデックス）でアクセスする方法も用意します．

定義1''（クロネッカー積の成分；大インデックスと小インデックスでアクセス）

$A \otimes B$ の $n_b I' +i, \, m_b J' + j$ 成分は以下のようにかける（ $0 \leqq I' \leqq n_a - 1$ ， $0 \leqq J' \leqq m_a - 1$ ， $1 \leqq i \leqq n_b$ ， $1 \leqq j \leqq m_b$ ）．

$(A \otimes B)_{\, n_b I' + i, \, m_b J' + j \,} = a_{\, I' + 1, \, J' + 1 \, } b_{\, i, \, j \, }$

ゼロ始まりのインデックスだと以下のようになる（ $0 \leqq i' \leqq n_b - 1$ ， $0 \leqq j' \leqq m_b- 1$ ）．

$(A \otimes B)^{(0)}_{\, n_b I' + i', \, m_b J' + j' \,} = a^{(0)}_{\, I', \, J' \, } b^{(0)}_{\, i', \, j' \, }$

それで定義1' のアクセス方法で命題1を証明すると以下になります． ${\rm floor}$ と ${\rm mod}$ のせいで横幅が長くなってしまうことがわかります．

命題1の証明1（定義1' を使用）

$0 \leqq i' \leqq n_a n_b - 1$ ， $0 \leqq j' \leqq m_c m_d - 1$ について，以下が成り立つ．

$\begin{split} \displaystyle \bigl( (A \otimes B)(C \otimes D)\bigr)^{(0)}_{i',j'} &= \sum_{k'=0}^{m_a m_b - 1} {a}^{(0)}_{\, {\rm floor} (i'/n_b), \, {\rm floor} ( k'/m_b ) \, } {b}^{(0)}_{\, {\rm mod}(i', n_b), \, {\rm mod}(k', m_b) \, } {c}^{(0)}_{\, {\rm floor} (k'/m_b), \, {\rm floor} ( j'/m_d ) \, } {d}^{(0)}_{\, {\rm mod}(k', m_b), \, {\rm mod}(j', m_d) \, } \\ &= \sum_{k'=0}^{m_a m_b - 1} \Bigl( {a}^{(0)}_{\, {\rm floor} (i'/n_b), \, {\rm floor} ( k'/m_b ) \, } {c}^{(0)}_{\, {\rm floor} (k'/m_b), \, {\rm floor} ( j'/m_d ) \, } \Bigr) \Bigl( {b}^{(0)}_{\, {\rm mod}(i', n_b), \, {\rm mod}(k', m_b) \, } {d}^{(0)}_{\, {\rm mod}(k', m_b), \, {\rm mod}(j', m_d) \, } \Bigr) \\ &= \sum_{k'=0}^{m_b - 1} \Bigl( {a}^{(0)}_{\, {\rm floor} (i'/n_b), \, 0 \, } {c}^{(0)}_{\, 0, \, {\rm floor} ( j'/m_d ) \, } \Bigr) \Bigl( {b}^{(0)}_{\, {\rm mod}(i', n_b), \, k' \, } {d}^{(0)}_{\, k', \, {\rm mod}(j', m_d) \, } \Bigr) \\ & \quad \, + \sum_{k'=0}^{m_b - 1} \Bigl( {a}^{(0)}_{\, {\rm floor} (i'/n_b), \, 1 \, } {c}^{(0)}_{\, 1, \, {\rm floor} ( j'/m_d ) \, } \Bigr) \Bigl( {b}^{(0)}_{\, {\rm mod}(i', n_b), \, k' \, } {d}^{(0)}_{\, k', \, {\rm mod}(j', m_d) \, } \Bigr) \\ & \quad \, + \cdots + \sum_{k'=0}^{m_b - 1} \Bigl( {a}^{(0)}_{\, {\rm floor} (i'/n_b), \, m_a-1 \, } {c}^{(0)}_{\, m_a-1, \, {\rm floor} ( j'/m_d ) \, } \Bigr) \Bigl( {b}^{(0)}_{\, {\rm mod}(i', n_b), \, k' \, } {d}^{(0)}_{\, k', \, {\rm mod}(j', m_d) \, } \Bigr) \\ &= \left( \sum_{k''=0}^{m_a - 1} {a}^{(0)}_{\, {\rm floor} (i'/n_b) , \, k'' \,} {c}^{(0)}_{\, k'', \, {\rm floor} ( j'/m_d ) \,} \right) \left( \sum_{k'=0}^{m_b - 1} {b}^{(0)}_{\, {\rm mod}(i', n_b), \, k' \,} {d}^{(0)}_{\, k', \, {\rm mod}(j', m_d) \,} \right) \\ &= (AC)^{(0)}_{\, {\rm floor} (i'/n_b), \, {\rm floor} ( j'/m_d ) \, } (BD)^{(0)}_{\, {\rm mod}(i', n_b), \, {\rm mod}(j', m_d) \, } \\ &= (AC \otimes BD)^{(0)}_{i',j'} \end{split}$

以上より， $(A \otimes B)(C \otimes D) = AC \otimes BD$ である．□

他方，定義1'' のアクセス方法で命題1を証明すると以下になります．横幅が短いです．また，後から気付いたんですが以下のように右辺から出発した方が（2重ループを1重ループにまとめる方向になるので）すっきりする気がします．

命題1の証明2（定義1'' を使用）

$0 \leqq I' \leqq n_a - 1$ ， $0 \leqq J' \leqq m_c - 1$ ， $0 \leqq i' \leqq n_b-1$ ， $0 \leqq j' \leqq m_d-1$ について，以下が成り立つ．

$\begin{split} \displaystyle (AC \otimes BD)^{(0)}_{\, n_b I' +i', \, m_d J' + j' \,} &= \left( \sum_{k=0}^{m_a - 1} a^{(0)}_{\, I', \, k \,} c^{(0)}_{\, k, \, J' \,} \right) \left( \sum_{k'=0}^{m_b - 1} b^{(0)}_{\, i', \, k' \,} d^{(0)}_{\, k', \, j' \,} \right) \\ &= \sum_{k=0}^{m_a - 1} \sum_{k'=0}^{m_b - 1} \Bigl( a^{(0)}_{\, I', \, k \,} b^{(0)}_{\, i', \, k' \,} \Bigr) \Bigl( c^{(0)}_{\, k, \, J'\,} d^{(0)}_{\, k', \, j' \,} \Bigr) \\ &= \sum_{k=0}^{m_a - 1} \sum_{k'=0}^{m_b - 1} (A \otimes B)^{(0)}_{\, n_b I' +i', \, m_b k + k' \,} (C \otimes D)^{(0)}_{\, m_b k +k', \, m_d J' + j' \,} \\ &= \sum_{K=0}^{m_a m_b - 1} (A \otimes B)^{(0)}_{\, n_b I' +i', \, K \,} (C \otimes D)^{(0)}_{\, K, \, m_d J' + j' \,} \\ &= \bigl( (A \otimes B) (C \otimes D) \bigr)^{(0)}_{\, n_b I' +i', \, m_d J' + j' \,} \end{split}$

以上より， $(A \otimes B)(C \otimes D) = AC \otimes BD$ である．□

おまけ

クロネッカー積と行列積の混合積のイメージ図を描きました．クロネッカー積をとることは洗剤を指定の濃さに塗りながらタイルを敷き詰めることに似ていると思ったのですが，いうほど洗剤を塗りながらタイルを敷き詰めることをするかというとしないので完全に駄目です．
f:id:cookie-box:20210329190053p:plain