Equivalence of Pareto frontier definitions

ink

def pareto_nondom {α : Type} (F : Factory α) (ms : List Meas) : Prop

The traditional definition of Pareto frontier based on non-domination

Equations

• One or more equations did not get rendered due to their size.

ink

theorem pareto_nondom_iff_pareto : ∀ {α : Type} {F : Factory α} {ms : List Meas}, pareto F ms ↔ pareto_nondom F ms ∧ last_decreasing ms

Our formalized definition of Pareto frontier is equivalent to the one in the paper based on non-domination.