Reference · Signed rationals

rainbow.math.rational.signed.affine-convex

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

Affine functions are convex (indeed the convexity inequality is an equality) -- the first substantive instance of signed/convex-on, and the fact that makes linear/affine LP objectives convex (KKT/Lagrangian relevance). signed/affine-convex : forall a b, convex-on (x |-> a*x + b) For weights w0+w1~1: a*((w0)x+(w1)y)+b ~ (w0)(a*x+b) + (w1)(a*y+b), an EQUALITY, so <= holds by reflexivity. Both sides expand (multiply-distributes-add-left), the scalar reassociates a*(W*v) ~ W*(a*v) (multiply assoc + comm), the constant term collapses (w0)b+(w1)b ~ b, and the four summands reorder (add-four-reorder). Off the magnitude/ reciprocal modulus (no reduction wall). Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.convex-functionmath.linear.matrix.action-scalemath.rational.signed.distributivemath.rational.signed.multiply-associativemath.rational.signed.multiply-ringmath.rational.signed.map-sum-algebramath.linear.matrix.affine-general-rate-certificatemath.rational.signed.geometric-bridgemath.rational.signed.unit-lawsmath.rational.signed.order-transitivitymath.rational.signed.order-respects

signed/affine-convex :
  (a b : ℚ)
  → signed/convex-on (fun x => a · x + b)