RosterTails.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.UniformKServer.RosterTails.cubic_exp_bound line 11
Source documentation
The Taylor cubic suffices for both lifetime tail estimates; retaining an explicit (loose) absolute constant avoids a separate asymptotic hypothesis.
```
theorem cubic_exp_bound (x : ℝ) (hx : 0 ≤ x) : x^3*Real.exp (-x/2) ≤ 48 := by
…
```
theorem OAI.UniformKServer.RosterTails.geometric_exp_bound line 22
theorem OAI.UniformKServer.RosterTails.actual_tail line 30
Source documentation
Actual (long) lifetimes: deterministic through age K-1, probability 1/K at ages K through K²-1, and compulsory retirement at K².
```
theorem actual_tail (K : ℕ) (hK : 2 ≤ K) :
    1/(K:ℝ)+(K:ℝ)^2*(1-1/(K:ℝ))^(K^2-K) ≤ 49/(K:ℝ) := by
…
```
theorem OAI.UniformKServer.RosterTails.short_tail line 54
Source documentation
Auxiliary short lifetimes: probability K^-1/2 at every age increment and compulsory retirement at K. This is distinct from the actual partition law.
```
theorem short_tail (K : ℕ) (hK : 2 ≤ K) :
    1/Real.sqrt K+(K:ℝ)*(1-1/Real.sqrt K)^(K-1) ≤ 49/Real.sqrt K := by
…
```