TierInsertion.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.UniformKServer.TierInsertion.gainCoefficient line 13
def OAI.UniformKServer.TierInsertion.lifetimeExponent line 15
theorem OAI.UniformKServer.TierInsertion.coefficient_bounds line 20
theorem OAI.UniformKServer.TierInsertion.exponent_bounds line 24

theorem OAI.UniformKServer.TierInsertion.weighted_short_gain line 87

Source documentation

The literal weighted insertion payment, with the auxiliary roster built by independent lifetime experiments and a single fixed lifetime exponent.

theorem weighted_short_gain (P : Parameters) (D : State I) (S : Finset I)
    (c : I → X) (r h : ℝ) (hr : 0 < r) (hh : 1 ≤ h) (K : ℕ) (hK : 2 ≤ K)
    (hlarge : Real.exp (lifetimeExponent P*h) ≤ K)
    (hq : 1/Real.sqrt (K:ℝ) ∈ Set.Icc (0:ℝ) 1)
    (n : I) (hD : D.Valid S c r K (1/Real.sqrt (K:ℝ)))
    (hn : ∀ i ∈ S, i < n)
    (htest : ∀ i ∈ young S c r K, r/2 < dist (c n) (c i))
    (μ : X → ℝ) (hμ : ∀ p, 0 ≤ μ p)
    (hM : 0 < ballMass r P.gammaH μ (c n))
    (hqual : ballMass r 20480000 μ (c n) ≤ Real.exp h*ballMass r P.gammaL μ (c n)) :
    r*insertionMass P r μ (c n)/(K:ℝ) ≤
      Real.exp (-h)*(value r P.sigma 204800 μ (D.parameter c r)-
…

Mentions: OAI.UniformKServer.TierInsertion.lifetimeExponent