Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.benders-cut

Lemmas behind operations-research checkssrc/rainbow/math/lemmas/benders_cut.clj0 definitions, 2 theorems

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

Depends onmath.sums.value-appendmath.nat.infinitemath.rational.nnrat.identitiesmath.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.signed.limit-uniquenessmath.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.decide-ordermath.rational.signed.decide-reflexivemath.logic.boolean-andmath.rational.signed.decide-equivalencemath.rational.signed.decide-completenessmath.rational.signed.unit-lawsmath.nat.strict-below-splitmath.nat.strict-below-moremath.checksmath.nat.at-most-addmath.rational.nnrat.harmonic-convergencemath.nat.divmodmath.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.rational.signed.add-associativemath.nat.semiringmath.nat.multiply-zero-splitmath.rational.nnrat.multiply-zero-splitmath.nat.monusmath.rational.nnrat.monusmath.rational.nnrat.add-zero-splitmath.rational.nnrat.add-cancel-zeromath.finite.rational-argmaxmath.rational.nnrat.order-totalmath.rational.nnrat.multiply-difference-zeromath.linear.vector.norm-nonnegativemath.linear.vector.norm-zero-reflectionalgorithms.proofs.counterfactual-distance-separationalgorithms.proofs.counterfactual-distance-lawsmath.finite.matrixmath.linear.matrix.equivalencemath.linear.matrix.transposemath.linear.matrix.transpose-equivalencemath.linear.matrix.multiplymath.linear.matrix.multiply-shapemath.linear.matrix.composablemath.linear.matrix.composable-multiplymath.linear.vector.additive-unitsmath.linear.vector.shape-cancellationmath.linear.vector.shape-mapmath.linear.vector.shape-addmath.linear.vector.dot-additivemath.linear.vector.dot-bilinearmath.linear.vector.dot-negatemath.linear.vector.dot-subtractmath.linear.vector.dot-scalemath.linear.matrix.action-scalemath.rational.signed.multiply-nonzeromath.rational.signed.order-monotonemath.rational.signed.list-summath.rational.signed.multiply-monotonemath.rational.signed.map-sum-algebramath.rational.signed.negate-additivemath.rational.signed.lp-objective-negatemath.nat.pair-index-inversemath.sums.flow-cutmath.lemmas.game-valuemath.lemmas.lp-dualitymath.lemmas.bb-leaf-bound

signed/recourse-weak-duality :
  (q : ℕ → ℚ) (W : ℕ → ℕ → ℚ) (pi y r : ℕ → ℚ) (m2 n2 : ℕ)
  (hdual : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n2), signed/expr-sum-value (fun i => pi i · W i idx) m2 ≤ q idx)
  (y0 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n2), 0 ≤ y idx)
  (feas : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m2), signed/expr-sum-value (fun j => W idx j · y j) n2 = r idx)
  → signed/expr-sum-value (fun ri => pi ri · r ri) m2 ≤ signed/expr-sum-value (fun qj => q qj · y qj) n2

signed/benders-cut-valid :
  (q : ℕ → ℚ) (W H : ℕ → ℕ → ℚ) (T : ℕ → ℕ → ℕ → ℚ) (PI : ℕ → ℕ → ℚ) (p : ℕ → ℚ)
  (alpha : ℚ) (beta x : ℕ → ℚ) (Y : ℕ → ℕ → ℚ) (S m2 n2 n1 : ℕ)
  (hdual : ∀ (sc : ℕ), ∀ (sc-bound : nat/strict-below sc S), ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n2), signed/expr-sum-value (fun i => (fun sr => PI sc sr) i · W i idx) m2 ≤ q idx)
  (p0 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx S), 0 ≤ p idx)
  (halpha : alpha = signed/expr-sum-value (fun as => p as · signed/expr-sum-value (fun hi => PI as hi · H as hi) m2) S)
  (hbeta : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n1), beta idx = signed/expr-sum-value (fun i => p i · (fun gs => fun gk => signed/expr-sum-value (fun i₁ => (fun sr => …⟨1⟩ …⟨1⟩ …⟨1⟩) i₁ · (fun ti => fun tj => …⟨7⟩) i₁ gk) m2) i idx) S)
  (Y0 : ∀ (sc : ℕ), ∀ (sc-bound : nat/strict-below sc S), ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n2), 0 ≤ Y sc idx)
  (feas : ∀ (sc : ℕ), ∀ (sc-bound : nat/strict-below sc S), ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m2), signed/expr-sum-value (fun j => W idx j · (fun sr => Y sc sr) j) n2 = (fun hi => H sc hi + signed/negate (signed/expr-sum-value (fun j => (fun ti => fun tj => …⟨7⟩) hi j · x j) n1)) idx)
  → alpha + signed/negate (signed/expr-sum-value (fun di => beta di · x di) n1) ≤ signed/expr-sum-value (fun es => p es · signed/expr-sum-value (fun di => q di · (fun sr => Y es sr) di) n2) S