球と球の演算

定義 4.8（「浮動小数と区間演算」§4）

$m\in\mathbb{F}$ , $r\in\mathbb{F}$ , $r\ge0$ に対し $B(m,r)=[m-r,m+r]$ と書く。2 つの球 $B_i=B(m_i,r_i)$ に対し

\begin{aligned} B_1\oplus B_2&=B(m,r),\quad m=\mathrm{fl}(m_1+m_2),\ r\ge r_1+r_2+u|m|,\\ B_1\otimes B_2&=B(m,r),\quad m=\mathrm{fl}(m_1m_2),\ r\ge|m_1|r_2+|m_2|r_1+r_1r_2+u|m| \end{aligned}

と定める。 $r$ は右辺を上向き丸め（またはその代わりの succ）で計算した浮動小数とする。

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

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

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