Reference · Signed rationals

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

Signed rationalssrc/rainbow/math/rational/signed/strict_convex_unique.clj0 definitions, 2 theorems

Uniqueness of the minimizer for a strictly convex function -- the OR-Commons payoff of the convexity lane: a strictly convex objective has at most one minimizer (up to equivalence). signed/is-minimizer f x := forall z, f x <= f z signed/strict-convex-minimizer-unique : strict-convex-on f -> is-minimizer f x -> is-minimizer f y -> 0 < w0 -> 0 < w1 -> (w0 + w1 ~ 1) -> not(x ~ y) -> falsity. Proof: strict convexity at (w0,w1) gives f(wsum) < wsum(f x, f y); both minima are equal (antisymmetry) so wsum collapses to f x; but f x <= f(wsum), so f(wsum) < f(wsum) -- absurd. Stated over ABSTRACT positive weights (any convex-combination witness), so the check is symbolic.

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

signed/is-minimizer :
  (x₁ : ℚ → ℚ) (x₂ : ℚ)
  → Prop

signed/strict-convex-minimizer-unique :
  (f : ℚ → ℚ) (x y : ℚ) (w0 w1 : ℚ≥0) (hf : signed/strict-convex-on f)
  (hx : signed/is-minimizer f x) (hy : signed/is-minimizer f y)
  (hw0 : nnrat/less-than 0 w0) (hw1 : nnrat/less-than 0 w1)
  (hw : w0 + w1 = 1)
  (hxy : proposition/negation (x = y))
  → proposition/falsity