Menu

Rainbow docs menu

Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.state-price

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

General lemmas: state price. 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.sums.two-terms math.rational.signed.multiply-positive math.rational.signed.multiply-associative math.rational.signed.multiply-ring

signed/state-price-pricing

TheoremFor all inputsNo axiomsSource

signed/state-price-pricing :
  (D : ℕ → ℕ → ℚ) (pi q theta : ℕ → ℚ) (S J : ℕ)
  (hpi : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx J), signed/expr-sum-value (fun ps => q ps · D ps idx) S = pi idx)
  → signed/expr-sum-value (fun cj => pi cj · theta cj) J = signed/expr-sum-value (fun vs => q vs · signed/expr-sum-value (fun pj => D vs pj · theta pj) J) S

= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational

signed/state-price-no-arbitrage

TheoremFor all inputsNo axiomsSource

signed/state-price-no-arbitrage :
  (D : ℕ → ℕ → ℚ) (pi q theta : ℕ → ℚ) (S J : ℕ)
  (hpi : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx J), signed/expr-sum-value (fun ps => q ps · D ps idx) S = pi idx)
  (hq : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx S), 0 ≤ q idx)
  (hD : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx S), 0 ≤ signed/expr-sum-value (fun pj => D idx pj · theta pj) J)
  → 0 ≤ signed/expr-sum-value (fun cj => pi cj · theta cj) J

0 = signed/zero= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most

signed/state-price-no-arbitrage-strict

TheoremFor all inputsNo axiomsSource

signed/state-price-no-arbitrage-strict :
  (D : ℕ → ℕ → ℚ) (pi q theta : ℕ → ℚ) (S J : ℕ)
  (hpi : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx J), signed/expr-sum-value (fun ps => q ps · D ps idx) S = pi idx)
  (hq : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx S), 0 ≤ q idx)
  (hD : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx S), 0 ≤ signed/expr-sum-value (fun pj => D idx pj · theta pj) J)
  (s0 : ℕ) (s0-lt : nat/strict-below s0 S)
  (hq0 : 0 < q s0)
  (hD0 : 0 < signed/expr-sum-value (fun pj => D s0 pj · theta pj) J)
  → 0 < signed/expr-sum-value (fun cj => pi cj · theta cj) J

0 = signed/zero< = signed/less-than= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most