Reference · Signed rationals

rainbow.math.rational.signed.fubini

Signed rationalssrc/rainbow/math/rational/signed/fubini.clj0 definitions, 3 theorems

Finite Fubini for signed sums, and the double-counting weak-duality theorem it powers. signed/map-sum-swap : sum_i sum_j T i j ~ sum_j sum_i T i j Induction on the outer list: the empty case is a sum of empty sums, which `signed/map-sum-zero` collapses, and the cons step splits the inner sum with `signed/map-sum-add` and applies the induction hypothesis. The payoff is DOUBLE-COUNTING WEAK DUALITY. Given a term family T i j (think T i j = A_ij x_j y_i), if every column's total dominates the primal contribution and every row's total is dominated by the dual contribution, c_j * x_j <= sum_i T i j (each column) sum_j T i j <= b_i * y_i (each row) then the primal objective is below the dual objective: sum_j c_j*x_j <= sum_i b_i*y_i. Summing the column bounds, swapping the order of summation, and applying the row bounds is the entire argument -- weak duality is double counting, and Fubini is the only nontrivial ingredient. Unlike the nnrat LP stack this holds over SIGNED data, so the matrix, costs and right-hand side may all be negative. `optimization/signed-row-bound-of-primal-feasibility` discharges the row hypothesis from ordinary primal feasibility (Ax)_i <= b_i together with a nonnegative dual variable, by pulling y_i out of the row sum with `signed/map-sum-scale-right`. The mirrored discharge of the column hypothesis additionally needs signed multiplicative associativity, which is not yet proved; callers supplying their own T must reassociate themselves. Native and axiom-free; chains the signed distributive toolkit on D63.

Depends onmath.rational.signed.distributive

signed/map-sum-swap.{u} :
  (A B : Type u) (T : A → B → ℚ) (is : List A) (js : List B)
  → Σ i∈is, Σ j∈js, T i j = Σ j∈js, Σ i∈is, T i j

optimization/signed-double-counting-weak-duality.{u} :
  (A B : Type u) (T : A → B → ℚ) (primal : B → ℚ) (dual : A → ℚ) (is : List A)
  (js : List B)
  (column : ∀ (j : B), primal j ≤ Σ i∈is, T i j)
  (row : ∀ (i : A), Σ j∈js, T i j ≤ dual i)
  → Σ j∈js, primal j ≤ Σ j∈is, dual j

optimization/signed-row-bound-of-primal-feasibility.{u} :
  (B : Type u) (activity : B → ℚ) (bound weight : ℚ) (js : List B)
  (feasible : Σ j∈js, activity j ≤ bound)
  (nonnegative : 0 ≤ weight)
  → Σ j∈js, activity j · weight ≤ bound · weight