Harmony evaluation

Evaluation and order lemmas for Constraints.harmonyScore and Constraints.weightedViolations.

Main results

• weightedViolations_cons, harmonyScore_cons: @[simp] cons-recursion evaluating harmony on literal grammars ![C₀, …], ![w₀, …].
• weightedViolations_mono: for 0 ≤ w, the weighted violation sum is monotone in the violation profile.
• harmonyScore_le_of_forall_le, harmonyDominates_of_lt: harmonic bounding — a Pareto-dominant candidate has at least, and given a strict advantage on a positively weighted constraint strictly greater, harmony ([PS93]).

Evaluation by cons-recursion

@[simp]

theorem Constraints.weightedViolations_nil (w : Fin 0 → ℝ) (v : Fin 0 → ℕ) : weightedViolations w v = 0

@[simp]

theorem Constraints.weightedViolations_cons {n : ℕ} (w₀ : ℝ) (w : Fin n → ℝ) (v₀ : ℕ) (v : Fin n → ℕ) : weightedViolations (Matrix.vecCons w₀ w) (Matrix.vecCons v₀ v) = w₀ * ↑v₀ + weightedViolations w v

@[simp]

theorem Constraints.harmonyScore_nil {C : Type u_1} (con : CON C 0) (w : Fin 0 → ℝ) (x : C) : harmonyScore con w x = 0

@[simp]

theorem Constraints.harmonyScore_cons {C : Type u_1} {n : ℕ} (c₀ : Constraint C) (con : CON C n) (w₀ : ℝ) (w : Fin n → ℝ) (x : C) : harmonyScore (Matrix.vecCons c₀ con) (Matrix.vecCons w₀ w) x = -(w₀ * ↑(c₀ x)) + harmonyScore con w x

Harmonic bounding (Pareto dominance)

theorem Constraints.weightedViolations_mono {n : ℕ} {w : Fin n → ℝ} (hw : 0 ≤ w) : Monotone (weightedViolations w)

For non-negative weights, the weighted violation sum is monotone in the violation profile.

theorem Constraints.weightedViolations_lt_weightedViolations {n : ℕ} {w : Fin n → ℝ} {va vb : Fin n → ℕ} (hw : 0 ≤ w) (hle : va ≤ vb) (hlt : ∃ (i : Fin n), 0 < w i ∧ va i < vb i) : weightedViolations w va < weightedViolations w vb

Pointwise ≤ with a strict advantage on a positively weighted coordinate gives a strictly smaller weighted violation sum.

theorem Constraints.harmonyScore_le_of_forall_le {C : Type u_1} {n : ℕ} {con : CON C n} {w : Fin n → ℝ} {a b : C} (hw : 0 ≤ w) (h : ∀ (i : Fin n), con i a ≤ con i b) : harmonyScore con w b ≤ harmonyScore con w a

Harmonic bounding: with non-negative weights, a candidate incurring no more violations than b on every constraint has at least b's harmony ([PS93]).

theorem Constraints.harmonyDominates_of_lt {C : Type u_1} {n : ℕ} {con : CON C n} {w : Fin n → ℝ} {a b : C} (hw : 0 ≤ w) (hle : ∀ (i : Fin n), con i a ≤ con i b) (hlt : ∃ (i : Fin n), 0 < w i ∧ con i a < con i b) : harmonyDominates con w a b

Strict harmonic bounding: strictly fewer violations on some positively weighted constraint gives strictly greater harmony.