def isEqui (Que : queue) : Prop

Equations

• One or more equations did not get rendered due to their size.

def SameSpeedUp (Q P : SchedulePolicy) (h : P.dim = Q.dim) : Prop

Equations

• SameSpeedUp Q P h = ∀ (i : PiLp 1 fun (x : Fin P.dim) => ℝ) (j : PiLp 1 fun (x : Fin Q.dim) => ℝ) (k : Fin P.dim), i k = j (Fin.cast h k) ∧ P.speedupF i = Q.speedupF j

theorem EQUIOptimal (Que : queue) (Equi : MeanResponseTimePolicy) : isEqui Equi.Q → ∀ (x : MeanResponseTimePolicy) (h : x.Q.P.dim = Que.P.dim), SameSpeedUp Que.P x.Q.P h → Equi.L ≤ x.L