Skip to content
Rainbow docs menu

Reference · Signed rationals

rainbow.math.rational.signed.absolute-convex

Signed rationalssrc/rainbow/math/rational/signed/absolute_convex.clj0 definitions, 1 theorems

Absolute value is convex -- the canonical non-smooth convex function, the basis of L1 / robust / minimax objectives. signed/absolute-convex : convex-on (x |-> |x|) i.e. |(w0)x + (w1)y| <= (w0)|x| + (w1)|y| for w0+w1~1. The triangle inequality bounds |(w0)x + (w1)y| by |(w0)x| + |(w1)y|; each term rewrites via |a*b| ~ |a|*|b| and |from-nnrat w| ~ from-nnrat w (weights are nonnegative) to (w0)|x| + (w1)|y|. Wall-free (no reciprocal); does not touch the LP checker.

Depends onmath.rational.signed.convex-functionmath.rational.signed.absolutemath.rational.signed.distance-trianglemath.rational.signed.absolute-multiplymath.rational.signed.absolute-signmath.rational.signed.multiply-ringmath.rational.signed.map-sum-algebramath.rational.signed.multiply-ordermath.rational.signed.order-respectsmath.rational.nnrat.farkas-elim-list

signed/absolute-convex

TheoremWorked exampleNo axiomsSource, line 57

signed/absolute-convex :
  → signed/convex-on (fun x => signed/absolute x)