数学 › 計算機援用証明 › 行列計算の認証と最適化の証明書

成分ごとの評価からノルムの評価へ

補題 2.1（「行列計算の認証と最適化の証明書」§2）・ ✓公理まで証明済み

$|E|\le F$ （ $F$ は成分が非負）ならば $\|E\|\le\|F\|$ である。また $\boldsymbol{d}\in\mathbb{R}^n$ について $\|\boldsymbol{d}\boldsymbol{d}^{\mathsf{T}}\|=\|\boldsymbol{d}\|^2$ である。

本文で読む（証明と前後の説明）→

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています。

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

前提をたどる証明が使う定理・定義

証明は Rikai の他の定理を参照していません（定義と論理だけで示されています）。

これを使っている定理証明で参照している 2 件

Rump の正定値性検証✓定理 4.3・行列計算の認証と最適化の証明書
Cholesky 分解の後退安定性✓系 3.1・Cholesky 分解と帯行列・疎行列の直接法

関連するノック 1 問

計算機援用証明第 34 問