Reference · Signed rationals

rainbow.math.rational.signed.convex-closure

Signed rationalssrc/rainbow/math/rational/signed/convex_closure.clj0 definitions, 3 theorems

Closure properties of signed-rational convexity -- the algebra that makes a convex objective composable from convex parts (the convex-optimization bedrock). signed/convex-sum : convex-on f -> convex-on g -> convex-on (x |-> f x + g x) signed/convex-nonneg-scale: 0 <= c -> convex-on f -> convex-on (x |-> c * f x) Each is the pointwise combination of the two-point inequalities: for w0+w1~1, add the two `f`/`g` convexity bounds (add-monotone) then reassociate (w0)fx+(w1)fy+(w0)gx+(w1)gy into (w0)(fx+gx)+(w1)(fy+gy) via add-four-reorder and multiply-distributes-add-left; scale multiplies the single bound by c>=0 (multiply-left-monotone) and moves the scalar inside each weighted term (a*(W*v) ~ W*(a*v)). Off the magnitude/reciprocal modulus -- no division, so no reduction wall (unlike n-point Jensen, whose weight renormalization needs a reciprocal). Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.convex-functionmath.rational.signed.distributivemath.linear.matrix.action-scalemath.rational.signed.multiply-associativemath.rational.signed.multiply-ringmath.rational.signed.map-sum-algebramath.rational.signed.multiply-monotonemath.rational.signed.order-monotonemath.rational.signed.order-transitivitymath.rational.signed.order-respectsmath.rational.signed.minmaxmath.rational.nnrat.farkas-elim-list

signed/convex-sum :
  (f g : ℚ → ℚ) (cf : signed/convex-on f) (cg : signed/convex-on g)
  → signed/convex-on (fun x => f x + g x)

signed/convex-nonneg-scale :
  (c : ℚ) (f : ℚ → ℚ)
  (hc : 0 ≤ c)
  (cf : signed/convex-on f)
  → signed/convex-on (fun x => c · f x)

signed/convex-max :
  (f g : ℚ → ℚ) (cf : signed/convex-on f) (cg : signed/convex-on g)
  → signed/convex-on (fun x => signed/max (f x) (g x))