数学 › 計算機援用証明 › 浮動小数と区間演算

浮動小数の間隔

補題 2.2（「浮動小数と区間演算」§2） ・ ✓公理まで証明済み

emin⁡≤e≤emax⁡e_{\min}\le e\le e_{\max} のとき、F∩[2e,2e+1]\mathbb{F}\cap[2^e,2^{e+1}] は間隔 2e−p+1=2u⋅2e2^{e-p+1}=2u\cdot2^e の等間隔な点列で、両端 2e2^e, 2e+12^{e+1} を含む（e=emax⁡e=e_{\max} のときは右端を除く）。[0,2emin⁡][0,2^{e_{\min}}] の中の F\mathbb{F} の元は間隔 2emin⁡−p+12^{e_{\min}-p+1} の等間隔な点列である。

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

閉包の状態

✓ 公理まで証明済み

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

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

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

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

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

関連するノック 6 問