Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.indep-set-dual

Lemmas behind operations-research checkssrc/rainbow/math/lemmas/indep_set_dual.clj0 definitions, 8 theorems

General lemmas: indep set dual. 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.sums.nonneg-zeromath.rational.signed.multiply-associativemath.rational.signed.multiply-ring

signed/at-most-total :
  (a b : ℚ)
  → proposition/disjunction (a ≤ b) (b ≤ a)

signed/one-minus-nonnegative :
  (a : ℚ)
  (h : a ≤ 1)
  → 0 ≤ 1 + signed/negate a

signed/zero-one-at-most-one :
  (x : ℚ)
  (h : x · (1 + signed/negate x) = 0)
  → x ≤ 1

signed/multiply-subtract-expand :
  (p q t : ℚ)
  → p · (q + signed/negate t) = p · q + signed/negate (p · t)

signed/square-at-most-self-at-most-one :
  (s : ℚ)
  (h0 : 0 ≤ s)
  (h : s · s ≤ s)
  → s ≤ 1

signed/multiply-split-at :
  (y t a : ℚ)
  → y · t = y · a + y · (t + signed/negate a)

signed/independent-meets-clique-at-most-once :
  (A M : ℕ → ℕ → ℚ) (z : ℕ → ℚ) (n C : ℕ)
  (hz0 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ z idx)
  (hz1 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), z idx ≤ 1)
  (hM0 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ (fun rv => M C rv) idx)
  (hM1 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), (fun rv => M C rv) idx ≤ 1)
  (hA0 : ∀ (au : ℕ), ∀ (au-lt : nat/strict-below au n), ∀ (av : ℕ), ∀ (av-lt : nat/strict-below av n), 0 ≤ A au av)
  (hA1 : ∀ (au : ℕ), ∀ (au-lt : nat/strict-below au n), ∀ (av : ℕ), ∀ (av-lt : nat/strict-below av n), A au av ≤ 1)
  (hcl : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun kv => M C idx · (M C kv · (1 + signed/negate (A idx kv)))) n ≤ 0)
  (hind : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun iv => z idx · (z iv · A idx iv)) n ≤ z idx)
  → signed/expr-sum-value (fun mv => z mv · M C mv) n ≤ 1

signed/clique-cover-weak-duality :
  (A M : ℕ → ℕ → ℚ) (w z y : ℕ → ℚ) (n m : ℕ)
  (hz0 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ z idx)
  (hz1 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), z idx ≤ 1)
  (hA0 : ∀ (au : ℕ), ∀ (au-lt : nat/strict-below au n), ∀ (av : ℕ), ∀ (av-lt : nat/strict-below av n), 0 ≤ A au av)
  (hA1 : ∀ (au : ℕ), ∀ (au-lt : nat/strict-below au n), ∀ (av : ℕ), ∀ (av-lt : nat/strict-below av n), A au av ≤ 1)
  (hM0 : ∀ (mc : ℕ), ∀ (mc-lt : nat/strict-below mc m), ∀ (mv : ℕ), ∀ (mv-lt : nat/strict-below mv n), 0 ≤ M mc mv)
  (hM1 : ∀ (mc : ℕ), ∀ (mc-lt : nat/strict-below mc m), ∀ (mv : ℕ), ∀ (mv-lt : nat/strict-below mv n), M mc mv ≤ 1)
  (hcl : ∀ (lc : ℕ), ∀ (lc-lt : nat/strict-below lc m), ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun kv => M lc idx · (M lc kv · (1 + signed/negate (A idx kv)))) n ≤ 0)
  (hind : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun iv => z idx · (z iv · A idx iv)) n ≤ z idx)
  (hy0 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), 0 ≤ y idx)
  (hcov : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), w idx ≤ signed/expr-sum-value (fun dc => y dc · M dc idx) m)
  → signed/expr-sum-value (fun dv => w dv · z dv) n ≤ signed/expr-sum-value (fun dy => y dy) m