Pareto dominance and positive linearizations

Pointwise (Pareto) dominance between ℕ-valued cost vectors over finitely many dimensions is characterized by weighted sums: f < g pointwise iff every strictly positive weighting ranks ∑ i, w i * f i below ∑ i, w i * g i. Monotonicity of weighted sums gives one direction; a weighting concentrated on a violating coordinate separates the other. Consequently two vectors are incomparable iff two positive weightings disagree about them — the exact sense in which a weighted-sum model can, and Pareto reasoning cannot, break ties.

Companion to Core.Optimization.Pareto (the pullback-preorder view of the pointwise order); weighted aggregation itself stays in consuming layers (Core.Optimization.System). [UPSTREAM] candidate: mathlib provides the pointwise order and the engine Finset.sum_lt_sum, but not the characterization; on upstreaming, generalize the codomain from ℕ.

Main results

• sum_mul_lt_sum_mul — pointwise ≤ and strictness at one positively weighted coordinate give a strict weighted-sum inequality.
• exists_pos_weight_sum_mul_lt — a coordinate-wise strict inequality admits a strictly positive weighting whose weighted sums order strictly.
• le_iff_forall_pos_weight, lt_iff_forall_pos_weight — Pareto ≤ / < coincide with agreement of all strictly positive weightings.
• exists_pos_weights_disagree — incomparable vectors are ordered oppositely by two positive weightings.

theorem Core.Optimization.sum_mul_le_sum_mul {ι : Type u_1} [Fintype ι] {f g w : ι → ℕ} (hle : f ≤ g) : ∑ i : ι, w i * f i ≤ ∑ i : ι, w i * g i

Weighted sums are monotone in the pointwise order.

theorem Core.Optimization.sum_mul_lt_sum_mul {ι : Type u_1} [Fintype ι] {f g w : ι → ℕ} (hle : f ≤ g) (h : ∃ (i : ι), 0 < w i ∧ f i < g i) : ∑ i : ι, w i * f i < ∑ i : ι, w i * g i

Pointwise ≤ with strictness at a positively weighted coordinate gives a strict weighted-sum inequality.

theorem Core.Optimization.exists_pos_weight_sum_mul_lt {ι : Type u_1} [Fintype ι] {f g : ι → ℕ} (h : ∃ (i : ι), f i < g i) : ∃ (w : ι → ℕ), (∀ (j : ι), 0 < w j) ∧ ∑ j : ι, w j * f j < ∑ j : ι, w j * g j

A coordinate-wise strict inequality admits a strictly positive weighting whose weighted sums order the vectors strictly: weight ∑ k, f k + 1 on the strict coordinate, 1 elsewhere.

theorem Core.Optimization.le_iff_forall_pos_weight {ι : Type u_1} [Fintype ι] {f g : ι → ℕ} : f ≤ g ↔ ∀ (w : ι → ℕ), (∀ (i : ι), 0 < w i) → ∑ i : ι, w i * f i ≤ ∑ i : ι, w i * g i

Pareto ≤ is agreement of every strictly positive weighting.

theorem Core.Optimization.lt_iff_forall_pos_weight {ι : Type u_1} [Fintype ι] {f g : ι → ℕ} : f < g ↔ ∀ (w : ι → ℕ), (∀ (i : ι), 0 < w i) → ∑ i : ι, w i * f i < ∑ i : ι, w i * g i

Pareto dominance is strict agreement of every strictly positive weighting.

theorem Core.Optimization.exists_pos_weights_disagree {ι : Type u_1} [Fintype ι] {f g : ι → ℕ} (h₁ : ¬f ≤ g) (h₂ : ¬g ≤ f) : ∃ (w : ι → ℕ) (w' : ι → ℕ), (∀ (i : ι), 0 < w i) ∧ (∀ (i : ι), 0 < w' i) ∧ ∑ i : ι, w i * f i < ∑ i : ι, w i * g i ∧ ∑ i : ι, w' i * g i < ∑ i : ι, w' i * f i

Pareto-incomparable vectors are ordered oppositely by two strictly positive weightings: weighted-sum models can, and Pareto reasoning cannot, break the tie.