Reference · Finite sums

rainbow.math.sums.budgeted-protection

Finite sumssrc/rainbow/math/sums/budgeted_protection.clj0 definitions, 2 theorems

Weak duality for a budgeted box: 0<=w<=1, sum w<=Gamma and d_j<=z+p_j, z,p>=0 imply sum w_j*d_j<=Gamma*z+sum p_j.

Depends onmath.sums.lp-boundsmath.rational.signed.order-monotonemath.rational.signed.multiply-monotonemath.rational.signed.distributive

signed/budgeted-protection-split :
  (w p : ℕ → ℚ) (z : ℚ) (n : ℕ)
  → signed/expr-sum-value (fun j => w j · (z + p j)) n = signed/expr-sum-value w n · z + signed/expr-sum-value (fun z₁ => w z₁ · p z₁) n

signed/budgeted-protection-bound :
  (w d p : ℕ → ℚ) (z gamma : ℚ) (n : ℕ)
  (wn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ w idx)
  (wu : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), w idx ≤ 1)
  (budget : signed/expr-sum-value w n ≤ gamma)
  (zn : 0 ≤ z)
  (pn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ p idx)
  (cover : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), d idx ≤ z + p idx)
  → signed/expr-sum-value (fun z₁ => w z₁ · d z₁) n ≤ gamma · z + signed/expr-sum-value p n