def signed_row_score {m : ℕ+} {n : ℕ} (A : Matrix (Fin ↑m) (Fin n) ℝ) (b : EuclideanSpace ℝ (Fin ↑m)) (x : EuclideanSpace ℝ (Fin n)) : Fin ↑m ⊕ Fin ↑m → ℝ

Helper for Proposition 6.20: the signed affine row score on the stacked row index type.

theorem sup_abs_row_pairing_sub_offset_eq_signed_row_sup {m : ℕ+} {n : ℕ} (A : Matrix (Fin ↑m) (Fin n) ℝ) (b : EuclideanSpace ℝ (Fin ↑m)) (x : EuclideanSpace ℝ (Fin n)) : (Finset.univ.sup' ⋯ fun (j : Fin ↑m) => |A j ⬝ᵥ x.ofLp| - b.ofLp j) = Finset.univ.sup' ⋯ (signed_row_score A b x)

Helper for Proposition 6.20: the absolute-value row objective is the finite maximum of the corresponding signed row scores.

theorem finset_sup'_eq_sSup_stdSimplex_weighted_sum {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : ι → ℝ) : Finset.univ.sup' ⋯ f = sSup (Set.range fun (u : StdSimplex ℝ ι) => ∑ i : ι, u.weights i * f i)

Helper for Proposition 6.20: a finite maximum equals the supremum of all simplex-weighted averages of the same finite family.

theorem signed_row_weighted_sum_eq_matrix_dotProduct_sub {m : ℕ+} {n : ℕ} (A : Matrix (Fin ↑m) (Fin n) ℝ) (b : EuclideanSpace ℝ (Fin ↑m)) (x : EuclideanSpace ℝ (Fin n)) (u : StdSimplex ℝ (Fin ↑m ⊕ Fin ↑m)) : ∑ k : Fin ↑m ⊕ Fin ↑m, u.weights k * signed_row_score A b x k = (A.fromRows (-A)).mulVec x.ofLp ⬝ᵥ ⇑u.weights - Sum.elim b.ofLp b.ofLp ⬝ᵥ ⇑u.weights

Helper for Proposition 6.20: the simplex-weighted signed score is the dot-product expression coming from the stacked matrix Matrix.fromRows A (-A) and duplicated offset Sum.elim b b.

theorem max_abs_row_pairing_sub_offset_eq_sSup_signed_simplex {m : ℕ+} {n : ℕ} (A : Matrix (Fin ↑m) (Fin n) ℝ) (b : EuclideanSpace ℝ (Fin ↑m)) (x : EuclideanSpace ℝ (Fin n)) : (Finset.univ.sup' ⋯ fun (j : Fin ↑m) => |A j ⬝ᵥ x.ofLp| - b.ofLp j) = sSup (Set.range fun (u : StdSimplex ℝ (Fin ↑m ⊕ Fin ↑m)) => (A.fromRows (-A)).mulVec x.ofLp ⬝ᵥ ⇑u.weights - Sum.elim b.ofLp b.ofLp ⬝ᵥ ⇑u.weights)

Proposition 6.20: stacking A and -A and duplicating b identifies max_j (|⟪a_j, x⟫| - b_j) with the supremum of the corresponding affine functional over the standard simplex on the signed row index set.