Reference · Signed rationals

rainbow.math.rational.signed.square-convex

Signed rationalssrc/rainbow/math/rational/signed/square_convex.clj0 definitions, 6 theorems

Square convexity over signed rationals -- the canonical non-trivial convex function. signed/square-convex : convex-on (x |-> x*x) i.e. ((w0)x + (w1)y)^2 <= (w0)(x*x) + (w1)(y*y) for w0+w1~1. Via the variance identity csq + w0*w1*(x-y)^2 ~ RHS (signed/variance-identity), whose extra term is nonnegative, so csq <= RHS. The identity is assembled from three registered sub-lemmas so that no single kernel check carries the whole reduction cost (the monolithic proof exceeded the 1M default budget -- deep multiply-nesting): signed/multiply-cross-regroup : (P*u)*(Q*w) ~ (P*Q)*(u*w) -- reusable regroup signed/square-combination-expand: comb^2 ~ CE (four regrouped monomials) signed/variance-term-expand : w0*w1*(x-y)^2 ~ VE (four signed monomials) signed/variance-sum-collapse : CE + VE ~ RHS (reorder, cancel cross terms, factor) Each sub-lemma is opaque once registered, so the identity and square-convex reference them at O(1) instead of re-reducing their bodies. Off the magnitude/reciprocal modulus. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.convex-functionmath.rational.signed.square-of-summath.rational.signed.multiply-associativemath.rational.signed.multiply-ringmath.linear.matrix.action-scalemath.rational.signed.distributivemath.rational.signed.map-sum-algebramath.linear.matrix.affine-general-rate-certificatemath.rational.signed.geometric-bridgemath.rational.signed.unit-lawsmath.rational.signed.multiply-ordermath.rational.signed.order-monotonemath.rational.signed.order-transitivitymath.rational.signed.order-respectsmath.linear.vector.norm-nonnegativemath.rational.signed.absolute-multiplymath.rational.nnrat.farkas-elim-list

signed/multiply-cross-regroup :
  (P u Q w : ℚ)
  → P · u · (Q · w) = P · Q · (u · w)

signed/square-combination-expand :
  (w0 w1 : ℚ≥0) (x y : ℚ)
  → (signed/from-nnrat w0 · x + signed/from-nnrat w1 · y) · (signed/from-nnrat w0 · x + signed/from-nnrat w1 · y) = signed/from-nnrat w0 · signed/from-nnrat w0 · (x · x) + signed/from-nnrat w0 · signed/from-nnrat w1 · (x · y) + (signed/from-nnrat w1 · signed/from-nnrat w0 · (y · x) + signed/from-nnrat w1 · signed/from-nnrat w1 · (y · y))

signed/variance-term-expand :
  (w0 w1 : ℚ≥0) (x y : ℚ)
  → signed/from-nnrat w0 · signed/from-nnrat w1 · ((x - y) · (x - y)) = signed/from-nnrat w0 · signed/from-nnrat w1 · (x · x) + signed/negate (signed/from-nnrat w0 · signed/from-nnrat w1 · (x · y)) + (signed/negate (signed/from-nnrat w0 · signed/from-nnrat w1 · (y · x)) + signed/from-nnrat w0 · signed/from-nnrat w1 · (y · y))

signed/variance-sum-collapse :
  (w0 w1 : ℚ≥0) (x y : ℚ)
  (hw : w0 + w1 = 1)
  → signed/from-nnrat w0 · signed/from-nnrat w0 · (x · x) + signed/from-nnrat w0 · signed/from-nnrat w1 · (x · y) + (signed/from-nnrat w1 · signed/from-nnrat w0 · (y · x) + signed/from-nnrat w1 · signed/from-nnrat w1 · (y · y)) + (signed/from-nnrat w0 · signed/from-nnrat w1 · (x · x) + signed/negate (signed/from-nnrat w0 · signed/from-nnrat w1 · (x · y)) + (signed/negate (signed/from-nnrat w0 · signed/from-nnrat w1 · (y · x)) + signed/from-nnrat w0 · signed/from-nnrat w1 · (y · y))) = signed/from-nnrat w0 · (x · x) + signed/from-nnrat w1 · (y · y)

signed/variance-identity :
  (w0 w1 : ℚ≥0) (x y : ℚ)
  (hw : w0 + w1 = 1)
  → (signed/from-nnrat w0 · x + signed/from-nnrat w1 · y) · (signed/from-nnrat w0 · x + signed/from-nnrat w1 · y) + signed/from-nnrat w0 · signed/from-nnrat w1 · ((x - y) · (x - y)) = signed/from-nnrat w0 · (x · x) + signed/from-nnrat w1 · (y · y)

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