OAI/Combinatorics/UniformKServer/TierRetirement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.TierRetirement.event line 17
2. theorem OAI.UniformKServer.TierRetirement.probability_bound line 28

   Source documentation

   Averaged under the true old survivor distribution. Conditioning on a realized surviving old record (which would invalidate this bound) is not used.

   theorem probability_bound (r : ℝ) (hr : 0<r) (K : ℕ) (hK : 2≤K)
       (hq : 1/(K:ℝ) ∈ Set.Icc (0:ℝ) 1) (q : Fin N → Prop) (c : Fin N → X) (n : Fin N)
       (ω : Fin N → TierRadius.Sample (X:=X) (Real.log (1+(K:ℝ)^2)) r) (p : X) :
   …

   Mentions: OAI.UniformKServer.TierRadius.Sample