Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.constrained-ls

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/constrained_ls.clj3 definitions, 4 theorems

Kochenderfer 'Algorithms for Optimization' Ch.11/13 constrained least-squares / distributed cores as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: O13.2 least squares w/ inequalities (LSI) : feasibility test g.x >= h (decidable) O13.3 least distance programming (LDP) : minimum-norm feasible point (min) O11.8 consensus ADMM : consensus variable = weighted average LSI feasibility reuses the decidable order (soundness via decide-at-most-true-sound); LDP reuses nnrat-minmax min; the consensus average reuses nnrat/wsum2 and inherits the convex bound. Native and axiom-free; chains nnrat-convex (-> wsum2, minmax) on d63.

Depends onmath.rational.nnrat.convex

opt/lsi-feasible :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

opt/ldp-min-norm :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

opt/admm-consensus :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

opt/lsi-feasible-sound :
  (gx h : ℚ≥0)
  (ok : bo/is-safe gx h = data/true)
  → h ≤ gx

opt/ldp-below-left :
  (n0 n1 : ℚ≥0)
  → opt/ldp-min-norm n0 n1 ≤ n0

opt/ldp-below-right :
  (n0 n1 : ℚ≥0)
  → opt/ldp-min-norm n0 n1 ≤ n1

opt/admm-consensus-within-max :
  (w0 w1 x0 x1 : ℚ≥0)
  (hw : w0 + w1 = 1)
  → bo/bootstrap-632 w0 w1 x0 x1 ≤ minmax/max x0 x1