Reference · Signed rationals

rainbow.math.rational.signed.gap-quality

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

Universal additive quality from a certified endpoint and reported gap. Arbitrary feasible sets/objectives; no optimizer existence or absolute-distance assertion. The conclusion includes feasibility of the submitted point.

Depends onmath.rational.signed.lp-objective-negate

optimization/signed-upper-gap-epsilon-optimal.{u} :
  (A : Type u) (objective : A → ℚ) (feasible : A → Prop) (x : A)
  (achieved endpoint gap epsilon : ℚ) (x-member : feasible x)
  (achieved-same : objective x = achieved)
  (gap-same : endpoint = achieved + gap)
  (bound : ∀ (y : A), ∀ (member : feasible y), objective y ≤ endpoint)
  (budget : gap ≤ epsilon)
  → proposition/conjunction (feasible x) (∀ (y : A), ∀ (member : feasible y), objective y - objective x ≤ epsilon)

optimization/signed-lower-gap-epsilon-optimal.{u} :
  (A : Type u) (objective : A → ℚ) (feasible : A → Prop) (x : A)
  (achieved endpoint gap epsilon : ℚ) (x-member : feasible x)
  (achieved-same : objective x = achieved)
  (gap-same : achieved = endpoint + gap)
  (bound : ∀ (y : A), ∀ (member : feasible y), endpoint ≤ objective y)
  (budget : gap ≤ epsilon)
  → proposition/conjunction (feasible x) (∀ (y : A), ∀ (member : feasible y), objective x - objective y ≤ epsilon)