Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.qp-kkt

Lemmas behind operations-research checkssrc/rainbow/math/lemmas/qp_kkt.clj0 definitions, 11 theorems

General lemmas: qp kkt. 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-boundmath.rational.signed.order-cancellation

signed/qp-gram-action :
  (Q R : ℕ → ℕ → ℚ) (x : ℕ → ℚ) (n : ℕ)
  (gram : ∀ (gi : ℕ), ∀ (gi-lt : nat/strict-below gi n), ∀ (gj : ℕ), ∀ (gj-lt : nat/strict-below gj n), Q gi gj = signed/expr-sum-value (fun g => R g gi · R g gj) n)
  (column-index : ℕ) (column-indexb : nat/strict-below column-index n)
  → signed/expr-sum-value (fun j => Q column-index j · x j) n = signed/expr-sum-value (fun i => (fun r => signed/expr-sum-value (fun j => R r j · x j) n) i · R i column-index) n

signed/qp-gram-bilinear :
  (Q R : ℕ → ℕ → ℚ) (x z : ℕ → ℚ) (n : ℕ)
  (gram : ∀ (gi : ℕ), ∀ (gi-lt : nat/strict-below gi n), ∀ (gj : ℕ), ∀ (gj-lt : nat/strict-below gj n), Q gi gj = signed/expr-sum-value (fun g => R g gi · R g gj) n)
  → signed/expr-sum-value (fun i => z i · signed/expr-sum-value (fun j => Q i j · x j) n) n = signed/expr-sum-value (fun d => (fun r => signed/expr-sum-value (fun j => R r j · x j) n) d · (fun r => signed/expr-sum-value (fun j => R r j · z j) n) d) n

signed/qp-square-difference-rearrange :
  (a b : ℚ)
  → a · a + (a · b + a · b) + (a + signed/negate b) · (a + signed/negate b) = b · b + (a · a + a · a)

signed/qp-square-tangent :
  (a b : ℚ)
  → signed/from-nnrat nnrat/half · (a · a) + a · b ≤ signed/from-nnrat nnrat/half · (b · b) + a · a

signed/qp-gram-tangent :
  (Q R : ℕ → ℕ → ℚ) (x z : ℕ → ℚ) (n : ℕ)
  (gram : ∀ (gi : ℕ), ∀ (gi-lt : nat/strict-below gi n), ∀ (gj : ℕ), ∀ (gj-lt : nat/strict-below gj n), Q gi gj = signed/expr-sum-value (fun g => R g gi · R g gj) n)
  → signed/from-nnrat nnrat/half · value + signed/expr-sum-value (fun i => z i · signed/expr-sum-value (fun j => Q i j · x j) n) n ≤ signed/from-nnrat nnrat/half · signed/expr-sum-value (fun i => z i · signed/expr-sum-value (fun j => Q i j · z j) n) n + value
  where value := signed/expr-sum-value (fun i => x i · signed/expr-sum-value (fun j => Q i j · x j) n) n

signed/qp-stationary-dot :
  (Q A : ℕ → ℕ → ℚ) (c x y z : ℕ → ℚ) (m n : ℕ)
  (stat : ∀ (st : ℕ), ∀ (st-lt : nat/strict-below st n), signed/expr-sum-value (fun j => Q st j · x j) n + c st + signed/expr-sum-value (fun i => y i · A i st) m = 0)
  → signed/expr-sum-value (fun i => z i · signed/expr-sum-value (fun j => Q i j · x j) n) n + signed/expr-sum-value (fun d => c d · z d) n + signed/expr-sum-value (fun i => y i · signed/expr-sum-value (fun j => A i j · z j) n) m = 0

signed/qp-complementary-product :
  (y b r : ℚ)
  (h : y · (b + signed/negate r) = 0)
  → y · r = y · b

signed/qp-complementary-sum :
  (A : ℕ → ℕ → ℚ) (b x y : ℕ → ℚ) (m n : ℕ)
  (comp : ∀ (cp : ℕ), ∀ (cp-lt : nat/strict-below cp m), y cp · (b cp + signed/negate (signed/expr-sum-value (fun j => A cp j · x j) n)) = 0)
  → signed/expr-sum-value (fun i => y i · signed/expr-sum-value (fun j => A i j · x j) n) m = signed/expr-sum-value (fun d => y d · b d) m

signed/qp-balance-order :
  (a b p q : ℚ)
  (ha : a + p = 0)
  (hb : b + q = 0)
  (hq : q ≤ p)
  → a ≤ b

signed/qp-combine-bounds :
  (xx zx zz cx cz : ℚ)
  (tangent : signed/from-nnrat nnrat/half · xx + zx ≤ signed/from-nnrat nnrat/half · zz + xx)
  (linear : xx + cx ≤ zx + cz)
  → signed/from-nnrat nnrat/half · xx + cx ≤ signed/from-nnrat nnrat/half · zz + cz

signed/expr-sum-qp-kkt-optimal :
  (Q R A : ℕ → ℕ → ℚ) (b c x y : ℕ → ℚ) (m n : ℕ)
  (gram : ∀ (gi : ℕ), ∀ (gi-lt : nat/strict-below gi n), ∀ (gj : ℕ), ∀ (gj-lt : nat/strict-below gj n), Q gi gj = signed/expr-sum-value (fun g => R g gi · R g gj) n)
  (stat : ∀ (st : ℕ), ∀ (st-lt : nat/strict-below st n), signed/expr-sum-value (fun j => Q st j · x j) n + c st + signed/expr-sum-value (fun i => y i · A i st) m = 0)
  (comp : ∀ (cp : ℕ), ∀ (cp-lt : nat/strict-below cp m), y cp · (b cp + signed/negate (signed/expr-sum-value (fun j => A cp j · x j) n)) = 0)
  (yn : ∀ (yn : ℕ), ∀ (yn-lt : nat/strict-below yn m), 0 ≤ y yn)
  (z : ℕ → ℚ)
  (feasible : ∀ (pf : ℕ), ∀ (pf-lt : nat/strict-below pf m), signed/expr-sum-value (fun j => A pf j · z j) n ≤ b pf)
  → signed/from-nnrat nnrat/half · signed/expr-sum-value (fun i => x i · signed/expr-sum-value (fun j => Q i j · x j) n) n + signed/expr-sum-value (fun d => c d · x d) n ≤ signed/from-nnrat nnrat/half · signed/expr-sum-value (fun i => z i · signed/expr-sum-value (fun j => Q i j · z j) n) n + signed/expr-sum-value (fun d => c d · z d) n