Reference · Signed rationals

rainbow.math.rational.signed.convex-function

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

The two-point convex-function representation over signed rationals, and its first witnesses -- the base for Jensen's inequality and for connecting convexity to the KKT / Lagrangian optimization lane. signed/convex-on f := for all nnrat weights w0,w1 with w0+w1~1 and signed x,y, f((w0)x + (w1)y) <= (w0) f(x) + (w1) f(y) (weights injected by from-nnrat; the combination is the same as signed/convex-*). signed/identity-convex : convex-on (x |-> x) -- trivial (equality, reflexive) signed/constant-convex : convex-on (x |-> c) -- via the weight-sum collapse identity: both sides reduce to the same combination, so at-most-reflexive closes it. constant: f collapses each side to c, and (w0)c + (w1)c ~ (w0+w1)c ~ 1*c ~ c via distributes-add-right + from-nnrat-add + (w0+w1~1) + multiply-one-left. Off the magnitude/reciprocal modulus (no reduction wall). Next: affine and square convexity (the variance inequality), then n-point Jensen by induction. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.distributivemath.linear.matrix.affine-general-rate-certificatemath.rational.signed.geometric-bridgemath.rational.signed.unit-lawsmath.rational.signed.multiply-ringmath.rational.signed.order-transitivitymath.rational.signed.order-respects

signed/convex-on :
  (x₁ : ℚ → ℚ)
  → Prop

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

signed/constant-convex :
  (c : ℚ)
  → signed/convex-on (fun x₁ => c)