数学 › 計算機援用証明 › 無限次元の固有値の包含

Nyström 行列は補間核の作用素

命題 7.2(「無限次元の固有値の包含」§7) ・ ✓公理まで証明済み

xix_i, wiw_i を nn 点 Gauss–Legendre 求積の節点と重み、ℓi\ell_i を Lagrange 基底とし、k~(x,y)=∑i,jk(xi,xj)ℓi(x)ℓj(y)\tilde k(x,y)=\sum_{i,j}k(x_i,x_j)\ell_i(x)\ell_j(y) とする。k~\tilde k を核とする作用素 K~\widetilde K の 00 でない固有値は、重複度も込めて、Nyström 行列 (wi k(xi,xj)wj)i,j\bigl(\sqrt{w_i}\,k(x_i,x_j)\sqrt{w_j}\bigr)_{i,j} の 00 でない固有値に一致する。

本文で読む(証明と前後の説明)→

閉包の状態

✓ 公理まで証明済み

証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理(物理では基本仮定)までつながっています(前提の定理類 3 件、定義なども含めて 3 件)。

印の意味: ✓公理まで証明済み ・ △証明あり(閉包未完)・ ※主張のみ。テーマごとの集計は 閉包の状況。

前提をたどる 証明が使う定理・定義(直接 1 件)

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

これを使っている定理

証明で明示的に参照している定理は、まだありません。

関連するノック 2 問