def network_utility_source_rate_objective {Source : Type u} {Link : Type v} (u : Source → ℝ → ℝ) (linksUsedBySource : Source → Finset Link) (lam : Link → NNReal) (s : Source) : ℝ → ℝ

The scalar objective maximized by source s in the NUM dual update, namely x_s ↦ u_s(x_s) - (∑_{ℓ ∈ L(s)} λ_ℓ) x_s.

@[simp]

theorem network_utility_source_rate_objective_apply {Source : Type u} {Link : Type v} (u : Source → ℝ → ℝ) (linksUsedBySource : Source → Finset Link) (lam : Link → NNReal) (s : Source) (x : ℝ) : network_utility_source_rate_objective u linksUsedBySource lam s x = u s x - (∑ ℓ ∈ linksUsedBySource s, ↑(lam ℓ)) * x

Evaluating network_utility_source_rate_objective u linksUsedBySource lam s at x gives the NUM source-rate objective u_s(x) - (∑_{ℓ ∈ L(s)} λ_ℓ) x.

def network_utility_dual_projected_subgradient_method_is_admissible {Source : Type u} {Link : Type v} (u : Source → ℝ → ℝ) (linksUsedBySource : Source → Finset Link) (I : Source → Set ℝ) (α : ℕ → ℝ) (xSel : (Link → NNReal) → Source → ℝ) : Prop

A source-rate selection rule is admissible for the NUM dual projected subgradient method when every stepsize is strictly positive and each selected source rate x_s^k attains the argmax from step (A) on the prescribed set I_s.

def network_utility_link_price_update {Source : Type u} {Link : Type v} [Fintype Source] [DecidableEq Link] (linksUsedBySource : Source → Finset Link) (c : Link → ℝ) (α : ℝ) (lam : Link → NNReal) (x : Source → ℝ) : Link → NNReal

The one-step link-price update λ_ℓ^+ = [λ_ℓ + α (∑_{s ∈ S(ℓ)} x_s - c_ℓ)]_+ from the NUM dual projected subgradient method.

@[simp]

theorem network_utility_link_price_update_apply {Source : Type u} {Link : Type v} [Fintype Source] [DecidableEq Link] (linksUsedBySource : Source → Finset Link) (c : Link → ℝ) (α : ℝ) (lam : Link → NNReal) (x : Source → ℝ) (ℓ : Link) : network_utility_link_price_update linksUsedBySource c α lam x ℓ = (↑(lam ℓ) + α * (network_link_load linksUsedBySource x ℓ - c ℓ)).toNNReal

Evaluating network_utility_link_price_update linksUsedBySource c α lam x at ℓ returns the positive-part link-price update for that link.

def network_utility_dual_projected_subgradient_method {Source : Type u} {Link : Type v} [Fintype Source] [DecidableEq Link] (linksUsedBySource : Source → Finset Link) (c : Link → ℝ) (α : ℕ → ℝ) (xSel : (Link → NNReal) → Source → ℝ) : ℕ → Link → NNReal

Algorithm 8.16: given a route-incidence map linksUsedBySource, link capacities c, stepsizes α_k, and a rule xSel selecting for each link-price vector λ^k the corresponding source-rate update from step (A), the NUM dual projected subgradient method starts from λ^0 = 0 and recursively generates the link-price sequence by λ^{k+1}_ℓ = [λ^k_ℓ + α_k (∑_{s ∈ S(ℓ)} x_s^k - c_ℓ)]_+.

def network_utility_dual_projected_subgradient_source_rate_iterate {Source : Type u} {Link : Type v} [Fintype Source] [DecidableEq Link] (linksUsedBySource : Source → Finset Link) (c : Link → ℝ) (α : ℕ → ℝ) (xSel : (Link → NNReal) → Source → ℝ) (k : ℕ) : Source → ℝ

The source-rate vector x^k selected from step (A) at the current link-price iterate λ^k.

@[simp]

theorem network_utility_dual_projected_subgradient_method_zero {Source : Type u} {Link : Type v} [Fintype Source] [DecidableEq Link] (linksUsedBySource : Source → Finset Link) (c : Link → ℝ) (α : ℕ → ℝ) (xSel : (Link → NNReal) → Source → ℝ) : network_utility_dual_projected_subgradient_method linksUsedBySource c α xSel 0 = 0

The NUM dual projected-subgradient link-price sequence starts from the zero multiplier vector.

@[simp]

theorem network_utility_dual_projected_subgradient_source_rate_iterate_eq {Source : Type u} {Link : Type v} [Fintype Source] [DecidableEq Link] (linksUsedBySource : Source → Finset Link) (c : Link → ℝ) (α : ℕ → ℝ) (xSel : (Link → NNReal) → Source → ℝ) (k : ℕ) : network_utility_dual_projected_subgradient_source_rate_iterate linksUsedBySource c α xSel k = xSel (network_utility_dual_projected_subgradient_method linksUsedBySource c α xSel k)

The source-rate iterate x^k is obtained by applying the selection rule xSel to the current link-price iterate λ^k.

theorem network_utility_dual_projected_subgradient_method_succ {Source : Type u} {Link : Type v} [Fintype Source] [DecidableEq Link] (linksUsedBySource : Source → Finset Link) (c : Link → ℝ) (α : ℕ → ℝ) (xSel : (Link → NNReal) → Source → ℝ) (k : ℕ) : network_utility_dual_projected_subgradient_method linksUsedBySource c α xSel (k + 1) = network_utility_link_price_update linksUsedBySource c (α k) (network_utility_dual_projected_subgradient_method linksUsedBySource c α xSel k) (network_utility_dual_projected_subgradient_source_rate_iterate linksUsedBySource c α xSel k)

One step of the NUM dual projected subgradient method applies the link-price update from Algorithm 8.16 to the current link-price iterate λ^k and source-rate iterate x^k.

theorem network_utility_dual_projected_subgradient_source_rate_iterate_isMaxOn {Source : Type u} {Link : Type v} [Fintype Source] [DecidableEq Link] (linksUsedBySource : Source → Finset Link) (c : Link → ℝ) (α : ℕ → ℝ) (xSel : (Link → NNReal) → Source → ℝ) {u : Source → ℝ → ℝ} {I : Source → Set ℝ} (h : network_utility_dual_projected_subgradient_method_is_admissible u linksUsedBySource I α xSel) (k : ℕ) (s : Source) : IsMaxOn (network_utility_source_rate_objective u linksUsedBySource (network_utility_dual_projected_subgradient_method linksUsedBySource c α xSel k) s) (I s) (network_utility_dual_projected_subgradient_source_rate_iterate linksUsedBySource c α xSel k s)

Under the admissibility condition, the selected source-rate component x_s^k attains the argmax from step (A) of Algorithm 8.16 on the set I_s.

theorem network_utility_dual_projected_subgradient_method_stepsize_pos {Source : Type u} {Link : Type v} (linksUsedBySource : Source → Finset Link) (α : ℕ → ℝ) (xSel : (Link → NNReal) → Source → ℝ) {u : Source → ℝ → ℝ} {I : Source → Set ℝ} (h : network_utility_dual_projected_subgradient_method_is_admissible u linksUsedBySource I α xSel) (k : ℕ) : 0 < α k

Under the admissibility condition, every stepsize in the NUM dual projected subgradient method is strictly positive.