情報科学 › 研究のための計算の実務 › 長時間ジョブの管理

最適なチェックポイント間隔（Young の近似）

定理 4.3（「長時間ジョブの管理」§4）・ ✓公理まで証明済み

$\lambda \gt 0$ 、 $\mu = 1/\lambda$ 、 $C \gt 0$ 、 $R \ge 0$ とする。 $h(\tau)$ （ $\tau \gt 0$ ）について次が成り立つ。

$h$ はただ 1 点 $\tau^{*}$ で最小値をとる。 $\tau^{*}$ は $0 \lt \tau \lt \mu$ の範囲での方程式 $(1 - \lambda\tau)e^{\lambda(\tau + C)} = 1$ のただ 1 つの解で、 $R$ によらない。 $h$ は $(0, \tau^{*}]$ で狭義単調減少、 $[\tau^{*}, \infty)$ で狭義単調増加である。
$\tau^{*} \le \sqrt{2C\mu}$ 。さらに $2C \le \mu$ ならば $\sqrt{2C\mu} - 2C \le \tau^{*} \le \sqrt{2C\mu}.$

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

閉包の状態

✓ 公理まで証明済み

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

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

前提をたどる証明が使う定理・定義（直接 2 件）

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

導関数の符号と単調性✓系 3.4・平均値の定理とテイラーの定理
- ラグランジュの平均値の定理✓定理 3.3・平均値の定理とテイラーの定理
  - ロルの定理✓定理 3.1・平均値の定理とテイラーの定理
    最大値・最小値の定理✓定理 2.3・平均値の定理とテイラーの定理この先をたどる →
    極大・極小定義 2.1・平均値の定理とテイラーの定理
    フェルマーの補題✓補題 2.5・平均値の定理とテイラーの定理この先をたどる →
中間値の定理✓定理 5.7・極限と連続性
- 実数の連続性公理（上限性質）公理 5.1・数とは何か

これを使っている定理

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

関連するノック 3 問