def coreSpace (n : ℕ) (c : PiLp 1 fun (x : Fin n) => ℕ) : Set (PiLp 1 fun (x : Fin n) => ℝ)

Equations

• coreSpace n c = {x : PiLp 1 fun (x : Fin n) => ℝ | ∀ {i : Fin n}, x i ≤ ↑(c i) ∧ ∀ (i : Fin n), x i ≥ 0}

def myConcave (n : ℕ) (c : PiLp 1 fun (x : Fin n) => ℕ) (f : (PiLp 1 fun (x : Fin n) => ℝ) → ℝ) : Prop

Equations

• myConcave n c f = ∀ x ∈ coreSpace n c, ∀ y ∈ coreSpace n c, ∀ {a b : ℝ}, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)

def Sublinear (n : ℕ) (speedvec : PiLp 1 fun (x : Fin n) => ℝ) (f : (PiLp 1 fun (x : Fin n) => ℝ) → ℝ) : Prop

Equations

• Sublinear n speedvec f = ((∀ (x : PiLp 1 fun (x : Fin n) => ℝ), ‖x‖ ≥ 0 → ‖f x‖ ≤ speedvec ⬝ᵥ x) ∧ ∃ c > 0, ∀ (x : PiLp 1 fun (x : Fin n) => ℝ), ‖x‖ ≥ 0 → ‖f x‖ ≤ c)

def nonDecreasing (n : ℕ) (f : (PiLp 1 fun (x : Fin n) => ℝ) → ℝ) : Prop

Equations

• nonDecreasing n f = ∀ (x : PiLp 1 fun (x : Fin n) => ℝ), ‖x‖ ≥ 0 → ∀ (ε : PiLp 1 fun (x : Fin n) => ℝ), ‖ε‖ > 0 → f x ≤ f (x + ε)

def SpeedUpFunction (n : ℕ) (speedvec : PiLp 1 fun (x : Fin n) => ℝ) (c : PiLp 1 fun (x : Fin n) => ℕ) (f : (PiLp 1 fun (x : Fin n) => ℝ) → ℝ) : Prop

Equations

• SpeedUpFunction n speedvec c f = (Sublinear n speedvec f ∧ myConcave n c f ∧ nonDecreasing n f)

structure RateMatrix : Type

• Q : ℕ → ℕ → ℝ
• sum_eq_zero_at_zero : self.Q 0 1 = -self.Q 0 0
• sum_eq_zero_at_non_zero (n : ℕ) : n ≠ 0 → self.Q n (n + 1) + self.Q n (n - 1) = -self.Q n n
• non_nbr_eq_zero (n k : ℕ) : k ≥ n + 2 → self.Q n k = 0 ∧ self.Q k n = 0
• arrival_rate_non_neg (n : ℕ) : 0 ≤ self.Q n (n + 1)
• departure_rate_non_neg (n : ℕ) : 0 ≤ self.Q (n + 1) n

def Policy (n : ℕ) (c : PiLp 1 fun (x : Fin n) => ℕ) (distributionpolicy : ℕ → ℕ) (p : ℕ → ℕ → PiLp 1 fun (x : Fin n) => ℝ) : Prop

Equations

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

structure SchedulePolicy : Type

• dim : ℕ
• μ : ℝ
• cN : PiLp 1 fun (x : Fin self.dim) => ℕ
• cR : PiLp 1 fun (x : Fin self.dim) => ℝ
• speedvector : PiLp 1 fun (x : Fin self.dim) => ℝ
• speedupF : (PiLp 1 fun (x : Fin self.dim) => ℝ) → ℝ
• distributionpolicy : ℕ → ℕ
• policy : ℕ → ℕ → PiLp 1 fun (x : Fin self.dim) => ℝ
• departurerates : ℕ → ℝ
• speedupF_is_speedup : SpeedUpFunction self.dim self.speedvector self.cN self.speedupF
• ispolicy : Policy self.dim self.cN self.distributionpolicy self.policy
• departurerates_uses_speedup (n : ℕ) : self.μ * ∑ i : Fin (self.distributionpolicy n), self.speedupF (self.policy n ↑i) = self.departurerates n
• cR_eq_cN (i : Fin self.dim) : ↑(self.cN i) = self.cR i

def IsStable (P : SchedulePolicy) (Λ : ℝ) : Prop

Equations

• IsStable P Λ = ∃ (c : ℝ), c > 0 → ∃ (N : ℕ), ∀ n ≥ N, Λ / P.departurerates n ≤ 1 - c

def ConstantArrival (Q : RateMatrix) (Λ : ℝ) : Prop

Equations

• ConstantArrival Q Λ = ∀ (i : ℕ), Q.Q i (i + 1) = Λ

structure queue : Type

• state_space : ℕ
• Λ : ℝ
• μ : ℝ
• Q : RateMatrix
• P : SchedulePolicy
• policy_mu_eq_queue_mu : self.P.μ = self.μ
• stable_policy : IsStable self.P self.Λ
• isConstant : ConstantArrival self.Q self.Λ

def InvariantDistribution (Que : RateMatrix) (lambda : ℕ → ℝ) : Prop

Equations

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

noncomputable def MeanNumberInSystem (Que : RateMatrix) (lambda : ℕ → ℝ) : InvariantDistribution Que lambda → ℝ

Equations

• MeanNumberInSystem Que lambda x✝ = ∑' (i : ℕ), ↑i * lambda i

noncomputable def MeanResponseTime (lambda : ℕ → ℝ) (Q : queue) : InvariantDistribution Q.Q lambda → ℝ

Equations

• MeanResponseTime lambda Q x✝ = (∑' (i : ℕ), lambda i * ↑i) / Q.Λ

structure MeanResponseTimePolicy : Type

• L : ℝ
• lambda : ℕ → ℝ
• Q : queue
• isID : InvariantDistribution self.Q.Q self.lambda
• isMRT : MeanResponseTime self.lambda self.Q ⋯ = self.L