rainbow.math.rational.signed.square-minimizer-unique

Signed rationals src/rainbow/math/rational/signed/square_minimizer_unique.clj0 definitions, 1 theorems

Concrete OR-Commons decision object: the square objective (\x. x*x) has at most one minimizer (up to equivalence). A direct instance of signed/strict-convex-minimizer-unique at the proved signed/square-strict-convex witness -- demonstrates the general uniqueness theorem on a named objective. Light: square-strict-convex is cited opaquely, so no square-instance reduction.

Depends onmath.rational.signed.strict-convex-unique math.rational.signed.square-strict-convex

signed/square-minimizer-unique

TheoremFor all inputsNo axiomsSource, line 31

signed/square-minimizer-unique :
  (x y : ℚ) (w0 w1 : ℚ≥0) (hx : signed/is-minimizer (fun x₁ => x₁ · x₁) x)
  (hy : signed/is-minimizer (fun x₁ => x₁ · x₁) y) (hw0 : nnrat/less-than 0 w0)
  (hw1 : nnrat/less-than 0 w1)
  (hw : w0 + w1 = 1)
  (hxy : proposition/negation (x = y))
  → proposition/falsity

+ = nnrat/add0 = nnrat/zero1 = nnrat/one= = signed/equivalent: equality of rational values· = signed/multiplyℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational