Reference · Signed rationals

rainbow.math.rational.signed.square-strict-convex

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

Strict convexity of the square, the capstone of the no-zero-divisors work: signed/strict-convex-on f := forall w0 w1 x y, 0<w0 -> 0<w1 -> (w0+w1 ~ 1) -> x !~ y -> f(wsum) < wsum(f x, f y) signed/square-strict-convex : strict-convex-on (\x. x*x). Reuses signed/square-convex for the non-strict <= and the registered signed/variance-identity csq + w0*w1*(x-y)^2 ~ RHS. Strictness = the gap var = w0*w1*(x-y)^2 is nonzero: if csq ~ RHS then csq + var ~ csq, so var ~ 0 (equivalent-add-left-cancel), contradicting var !~ 0. The gap is nonzero by signed/multiply-nonzero on the (embedded, hence nonzero) weights and (x-y) !~ 0. Helper signed/from-nnrat-nonzero lifts nnrat w !~ 0 to fnn(w) !~ 0.

Depends onmath.rational.signed.square-convexmath.rational.signed.square-nonzeromath.rational.signed.multiply-nonzeromath.rational.nnrat.strict-orderalgorithms.proofs.counterfactual-distance-separationmath.linear.matrix.least-squares-equality

signed/from-nnrat-nonzero :
  (w : ℚ≥0) (hw : proposition/negation (w = 0))
  → proposition/negation (signed/from-nnrat w = 0)

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

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