Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.transport-dual

Lemmas behind operations-research checkssrc/rainbow/math/lemmas/transport_dual.clj0 definitions, 3 theorems

General lemmas: transport dual. The mathematical facts the corresponding checks rest on, each checked by the kernel.

Depends onmath.lemmas.ufl-gapmath.lemmas.lp-dualitymath.nat.infinitemath.nat.strict-below-splitmath.nat.strict-below-moremath.nat.at-most-addmath.rational.nnrat.harmonic-convergencemath.rational.signed.decide-ordermath.rational.signed.decide-reflexivemath.nat.at-most-cancellationmath.rational.nnrat.order-equivalencemath.rational.nnrat.archimedeanmath.rational.nnrat.add-monotonemath.rational.nnrat.add-cancellationmath.rational.nnrat.additive-reassociationmath.rational.signed.order-transitivitymath.rational.signed.convergencemath.rational.signed.order-respectsmath.rational.nnrat.identitiesmath.rational.signed.limit-uniquenessmath.logic.boolean-andmath.rational.signed.decide-equivalencemath.rational.signed.decide-completenessmath.nat.divmodmath.nat.pair-index-inversemath.rational.signed.strict-ordermath.rational.signed.multiplymath.rational.nnrat.multiply-commutemath.rational.nnrat.product-reassociationmath.rational.nnrat.distribute-rightmath.rational.nnrat.ringmath.rational.nnrat.multiply-monotonemath.rational.nnrat.order-differencemath.rational.signed.multiply-ordermath.rational.signed.equivalence-lawsmath.rational.nnrat.minmaxmath.rational.nnrat.farkas-elim-listmath.rational.signed.no-zero-divisorsmath.rational.signed.unit-lawsmath.checksmath.rational.signed.minmaxmath.rational.signed.minmax-algebramath.rational.signed.clampmath.rational.signed.deviation-rowsmath.rational.signed.absolutemath.rational.signed.absolute-algebramath.rational.signed.distancemath.nat.linear-ordermath.lemmas.bb-leaf-bound

signed/rect-double-sum-row-supplies :
  (w : ℕ → ℚ) (X : ℕ → ℕ → ℚ) (s : ℕ → ℚ) (m n : ℕ)
  (hrows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), signed/expr-sum-value (fun rj => X idx rj) n = s idx)
  → signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun wr => fun wc => w wr · X wr wc) i column-index) n) m = signed/expr-sum-value (fun si => s si · w si) m

signed/rect-double-sum-col-demands :
  (w : ℕ → ℚ) (X : ℕ → ℕ → ℚ) (d : ℕ → ℚ) (m n : ℕ)
  (hcols : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun ci => X ci idx) m = d idx)
  → signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun wr => fun wc => w wc · X wr wc) i column-index) n) m = signed/expr-sum-value (fun dj => d dj · w dj) n

signed/transport-weak-duality :
  (c : ℕ → ℕ → ℚ) (u v s d : ℕ → ℚ) (X : ℕ → ℕ → ℚ) (m n : ℕ)
  (hdual : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai m), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj n), u ai + v aj ≤ c ai aj)
  (x0 : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai m), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj n), 0 ≤ X ai aj)
  (hrows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), signed/expr-sum-value (fun rj => X idx rj) n = s idx)
  (hcols : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun ci => X ci idx) m = d idx)
  → signed/expr-sum-value (fun di => s di · u di) m + signed/expr-sum-value (fun dj => d dj · v dj) n ≤ signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun ki => fun kj => c ki kj · X ki kj) i column-index) n) m