Menu

Rainbow docs menu

Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.xol-readings

Lemmas behind operations-research checks src/rainbow/math/lemmas/xol_readings.clj0 definitions, 2 theorems

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

Depends onmath.sums.value-append math.nat.infinite math.rational.nnrat.identities math.nat.at-most-cancellation math.rational.nnrat.order-equivalence math.rational.nnrat.archimedean math.rational.nnrat.add-monotone math.rational.nnrat.add-cancellation math.rational.nnrat.additive-reassociation math.rational.signed.order-transitivity math.rational.signed.convergence math.rational.signed.order-respects math.rational.signed.limit-uniqueness math.rational.signed.strict-order math.rational.signed.multiply math.rational.nnrat.multiply-commute math.rational.nnrat.product-reassociation math.rational.nnrat.distribute-right math.rational.nnrat.ring math.rational.nnrat.multiply-monotone math.rational.nnrat.order-difference math.rational.signed.multiply-order math.rational.signed.equivalence-laws math.rational.nnrat.minmax math.rational.nnrat.farkas-elim-list math.rational.signed.no-zero-divisors math.rational.signed.decide-order math.rational.signed.decide-reflexive math.logic.boolean-and math.rational.signed.decide-equivalence math.rational.signed.decide-completeness math.rational.signed.unit-laws math.nat.strict-below-split math.nat.strict-below-more math.checks math.nat.at-most-add math.rational.nnrat.harmonic-convergence math.nat.divmod math.rational.signed.minmax math.rational.signed.minmax-algebra math.rational.signed.clamp math.rational.signed.deviation-rows math.rational.signed.absolute math.rational.signed.absolute-algebra math.rational.signed.distance math.nat.linear-order math.rational.signed.add-associative math.nat.semiring math.nat.multiply-zero-split math.rational.nnrat.multiply-zero-split math.nat.monus math.rational.nnrat.monus math.rational.nnrat.add-zero-split math.rational.nnrat.add-cancel-zero math.finite.rational-argmax math.rational.nnrat.order-total math.rational.nnrat.multiply-difference-zero math.linear.vector.norm-nonnegative math.linear.vector.norm-zero-reflection algorithms.proofs.counterfactual-distance-separation algorithms.proofs.counterfactual-distance-laws math.finite.matrix math.linear.matrix.equivalence math.linear.matrix.transpose math.linear.matrix.transpose-equivalence math.linear.matrix.multiply math.linear.matrix.multiply-shape math.linear.matrix.composable math.linear.matrix.composable-multiply math.linear.vector.additive-units math.linear.vector.shape-cancellation math.linear.vector.shape-map math.linear.vector.shape-add math.linear.vector.dot-additive math.linear.vector.dot-bilinear math.linear.vector.dot-negate math.linear.vector.dot-subtract math.linear.vector.dot-scale math.linear.matrix.action-scale math.rational.signed.multiply-nonzero math.rational.signed.order-monotone math.rational.signed.list-sum math.rational.signed.multiply-monotone math.rational.signed.map-sum-algebra math.rational.signed.negate-additive math.rational.signed.lp-objective-negate math.nat.pair-index-inverse math.sums.flow-cut math.sums.nonneg-zero math.rational.signed.multiply-ring math.rational.signed.distributive math.linear.matrix.row-length-shape math.linear.matrix.row-length-decider math.rational.signed.structural-equality math.linear.vector.equivalence math.linear.vector.uniform-clamp math.linear.vector.pointwise-order math.linear.matrix.action-prepend math.linear.matrix.action-associative math.linear.matrix.transpose-multiply math.linear.matrix.transpose-shape math.linear.matrix.transpose-involution math.linear.matrix.transpose-involution-positive math.linear.matrix.transpose-multiply-reverse math.linear.matrix.composable-transpose math.linear.matrix.associativity-counterexample math.linear.matrix.signed-scale math.linear.matrix.signed-scale-right math.linear.matrix.add math.linear.matrix.add-shape math.linear.matrix.prepend-add math.linear.matrix.add-right math.linear.matrix.add-algebra math.linear.matrix.additive-group math.linear.matrix.negate-linear math.linear.matrix.subtract-linear math.linear.matrix.signed-scale-algebra math.linear.matrix.signed-scale-units math.linear.matrix.signed-scale-congruence math.linear.matrix.signed-scale-subtract math.rational.signed.distance-multiply-nonnegative math.rational.signed.vector-sup-distance algorithms.proofs.inner-product math.rational.signed.distance-triangle math.rational.signed.distance-translation math.rational.signed.distance-additive math.linear.vector.dot-distance-bound math.linear.vector.row-sum-lipschitz math.linear.matrix.action-sup-bound math.linear.matrix.signed-scale-order math.linear.matrix.pointwise-order-laws math.linear.matrix.signed-scale-antitone math.linear.matrix.add-order math.linear.matrix.signed-scale-positive math.linear.matrix.signed-scale-sign math.linear.matrix.positive-action math.linear.matrix.transpose-order math.linear.matrix.positive-multiply math.linear.matrix.gram-positive math.linear.matrix.gram-kernel math.linear.matrix.row-gram math.linear.matrix.row-gram-kernel math.linear.vector.norm-pythagorean math.linear.matrix.least-squares-normal math.linear.matrix.least-squares-equality math.linear.matrix.mixed-sign-action math.linear.matrix.mixed-sign-multiply math.linear.matrix.antitone math.linear.matrix.interval-order math.linear.matrix.affine-order math.linear.matrix.linear math.rational.signed.vector-sup-congruence math.finite.vector math.linear.vector.pointwise-order-laws math.linear.vector.add-order math.rational.signed.vector-sup-translation math.linear.matrix.affine-sup-distance math.linear.matrix.row-sum-lipschitz math.linear.matrix.row-sum-fixed-point-uniqueness math.linear.matrix.half-row-sum-fixed-point-uniqueness math.linear.matrix.affine-half-iterate-contraction math.linear.matrix.affine-half-iterate-rate math.rational.signed.geometric-bridge math.linear.matrix.affine-half-iterate-converges math.linear.matrix.affine-strong-row-contraction math.linear.matrix.affine-residual-certificate math.linear.matrix.affine-inverse-gap-certificate math.linear.matrix.affine-general-rate-certificate math.sums.of-nat math.lemmas.one-center

signed/layer-clamp-cases

TheoremFor all inputsNo axiomsSource

signed/layer-clamp-cases :
  (lc-e lc-l : ℚ)
  (lc-hl : 0 ≤ lc-l)
  → proposition/conjunction (0 ≤ data/Bool.rec (fun x₁₁₉₆ => ℚ) (data/Bool.rec (fun x₁₂₀₀ => ℚ) lc-l lc-e (signed/decide-at-most lc-e lc-l)) 0 (signed/decide-at-most lc-e 0)) (proposition/conjunction (data/Bool.rec (fun x₁₇₉₆ => ℚ) (data/Bool.rec (fun x₁₈₀₀ => ℚ) lc-l lc-e (signed/decide-at-most lc-e lc-l)) 0 (signed/decide-at-most lc-e 0) ≤ lc-l) (proposition/disjunction (proposition/conjunction (lc-e ≤ 0) (data/Bool.rec (fun x₂₁₁₆ => ℚ) (data/Bool.rec (fun x₂₁₂₀ => ℚ) lc-l lc-e (signed/decide-at-most lc-e lc-l)) 0 (signed/decide-at-most lc-e 0) = 0)) (proposition/disjunction (proposition/conjunction (0 ≤ lc-e) (proposition/conjunction (lc-e ≤ lc-l) (data/Bool.rec (fun x₂₃₁₆ => ℚ) (data/Bool.rec (fun x₂₃₂₀ => ℚ) lc-l lc-e (signed/decide-at-most lc-e lc-l)) 0 (signed/decide-at-most lc-e 0) = lc-e))) (proposition/conjunction (lc-l ≤ lc-e) (data/Bool.rec (fun x₂₃₅₆ => ℚ) (data/Bool.rec (fun x₂₃₆₀ => ℚ) lc-l lc-e (signed/decide-at-most lc-e lc-l)) 0 (signed/decide-at-most lc-e 0) = lc-l)))))

0 = signed/zero= = signed/equivalent: equality of rational valuesℚ = signed/SignedRational≤ = signed/at-most

signed/layer-recovery-cell

TheoremFor all inputsNo axiomsSource

signed/layer-recovery-cell :
  (rc-x rc-d rc-l rc-R : ℚ)
  (rc-hx : 0 ≤ rc-x)
  (rc-hd : 0 ≤ rc-d)
  (rc-hl : 0 ≤ rc-l)
  (rc-h : rc-R = data/Bool.rec (fun x₁₆ => ℚ) (data/Bool.rec (fun x₂₀ => ℚ) rc-l (rc-x + signed/negate rc-d) (most)) 0 (most₃))
  → proposition/conjunction (disjunction) (conjunction)
  where conjunction := proposition/conjunction (0 ≤ rc-R) (proposition/conjunction (rc-R ≤ rc-l) (rc-R ≤ rc-x))
  where disjunction := proposition/disjunction (proposition/conjunction (rc-x + signed/negate rc-d ≤ 0) (rc-R = 0)) (proposition/disjunction (proposition/conjunction (0 ≤ rc-x + signed/negate rc-d) (proposition/conjunction (rc-x + signed/negate rc-d ≤ rc-l) (rc-R = rc-x + signed/negate rc-d))) (proposition/conjunction (rc-l ≤ rc-x + signed/negate rc-d) (rc-R = rc-l)))
  where most := signed/decide-at-most (rc-x + signed/negate rc-d) rc-l
  where most₃ := signed/decide-at-most (rc-x + signed/negate rc-d) 0

+ = signed/add0 = signed/zero= = signed/equivalent: equality of rational valuesℚ = signed/SignedRational≤ = signed/at-most