数学 › 計算機援用証明 › 無限次元の固有値の包含
Nyström 行列は補間核の作用素
, を 点 Gauss–Legendre 求積の節点と重み、 を Lagrange 基底とし、 とする。 を核とする作用素 の でない固有値は、重複度も込めて、Nyström 行列 の でない固有値に一致する。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理(物理では基本仮定)までつながっています(前提の定理類 3 件、定義なども含めて 3 件)。
印の意味: ✓公理まで証明済み ・ △証明あり(閉包未完)・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義(直接 1 件)
▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。
Gauss 求積✓定理 6.1・直交多項式
Christoffel–Darboux の公式✓定理 4.1・直交多項式
- 三項漸化式✓定理 3.1・直交多項式
これを使っている定理
証明で明示的に参照している定理は、まだありません。