Theorem 4.1 — optimal capacity allocation φ_j = a_j + √(a_j f_j)/∑√(a_k f_k) · (F − ∑ a_k f_k)/f_j
ProvedKellyReversibility.Allocation.optimal_capacity_allocationA communication network has channels. Channel has average arrival rate and, if given capacity , holds on average customers. Capacity on channel costs per unit, and the capacities must satisfy the cost constraint (4.2)
where the budget satisfies . Among all capacity vectors with for every and satisfying (4.2), the mean number of customers in the network
is minimized by the allocation
Precisely: is feasible, it attains the minimum over the feasible set, and every other feasible gives a strictly larger mean number of customers.
Each channel first receives the capacity needed to carry its traffic; the excess budget is then shared in proportion to . As the book observes, minimizing the mean number of customers in the network is equivalent to minimizing the average time a customer spends in it.
Formalization Note The book leaves implicit that , , and ; without the last the feasible set is empty. The stability condition is part of the feasible set. The uniqueness clause (strict inequality for every other feasible point) slightly strengthens the book's "The optimal allocation is"; it holds because the objective is strictly convex.
import Mathlib import Definitions.Def_KellyReversibility_Allocation_CapacityAllocation
namespace KellyReversibility.Allocation
theorem optimal_capacity_allocation {J : ℕ} (hJ : 0 < J) (a f : Fin J → ℝ) (F : ℝ)
(ha : ∀ j, 0 < a j) (hf : ∀ j, 0 < f j) (hF : ∑ k, a k * f k < F) :
optimalAllocation a f F ∈ FeasibleCapacities a f F ∧
IsMinOn (meanNumberInNetwork a) (FeasibleCapacities a f F) (optimalAllocation a f F) ∧
∀ φ ∈ FeasibleCapacities a f F, φ ≠ optimalAllocation a f F →
meanNumberInNetwork a (optimalAllocation a f F) < meanNumberInNetwork a φ := by sorry
end KellyReversibility.Allocation
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.