ExitSeries.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MatroidProphet.hasSum_hazardBandBound line 9
Source documentation
Exact sum of all hazard-band bounds beginning at any natural level.
```
theorem hasSum_hazardBandBound (start : ℕ) :
    HasSum (fun k : ℕ => hazardBandBound (start + k)) (hazardTailPotential start) := by
…
```
Mentions: OAI.MatroidProphet.hazardBandBound, OAI.MatroidProphet.hazardTailPotential
theorem OAI.MatroidProphet.tsum_hazardBandBound line 38
Source documentation
The infinite dyadic tail equals the source's explicit resource bound.
```
theorem tsum_hazardBandBound (start : ℕ) :
    (∑' k : ℕ, hazardBandBound (start + k)) = hazardTailPotential start :=
…
```
Mentions: OAI.MatroidProphet.hazardBandBound, OAI.MatroidProphet.hazardTailPotential

theorem OAI.MatroidProphet.dyadic_exit_series line 43

Source documentation

Source equation eq:dyadic-exit, including its strict numerical bound.

theorem dyadic_exit_series :
    (∑' k : ℕ, hazardBandBound (12 + k)) =
      ((2 : ℝ) ^ 11)⁻¹ * (14 * Real.log 2 + 1) ∧
    (∑' k : ℕ, hazardBandBound (12 + k)) < (1 : ℝ) / 2 := by
…

Mentions: OAI.MatroidProphet.hazardBandBound