Daleckii–Krein 公式

定理 7.3（「作用素不等式と積分作用素」§7）・ ✓公理まで証明済み

$A,B$ を Hermite 行列、 $A=\sum_i\lambda_iP_i$ とし、 $f\in C^1(\mathbb{R})$ とする。このとき

\frac{d}{dt}f(A+tB)\Big|_{t=0}=T^{A,A}_{f^{[1]}}(B)=\sum_{i,j}f^{[1]}(\lambda_i,\lambda_j)P_iBP_j .

とくに $\frac{d}{dt}\mathrm{tr}f(A+tB)|_{t=0}=\mathrm{tr}\bigl(f'(A)B\bigr)$ 。

閉包の状態

✓ 公理まで証明済み

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

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

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

二重作用素積分の基本性質✓補題 7.1・作用素不等式と積分作用素
Stone–Weierstrass の定理（実数値）✓定理 4.3・Arzelà–Ascoli と Stone–Weierstrass
- 絶対値関数の多項式による一様近似✓補題 4.1・Arzelà–Ascoli と Stone–Weierstrass
  - ディニの定理✓定理 4.3・関数列と一様収束
    一様収束定義 3.2・関数列と一様収束
    ボルツァーノ・ワイエルシュトラスの定理✓定理 6.3・実数の完備性とコーシー列この先をたどる →

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