theorem helperForTheorem_19_1_cone_polyhedral_of_finite_generators {m : ℕ} {T : Set (Fin m → ℝ)} (hT : T.Finite) : IsPolyhedralConvexSet m (cone m T)

Helper for Theorem 19.1: cones generated by finite sets are polyhedral.

theorem helperForTheorem_19_1_mixedConvexHull_polyhedral_of_finite_generators {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} (hS₀ : S₀.Finite) (hS₁ : S₁.Finite) : IsPolyhedralConvexSet n (mixedConvexHull S₀ S₁)

Helper for Theorem 19.1: mixed convex hull of finitely many generators is polyhedral.

theorem helperForTheorem_19_1_finitelyGenerated_imp_polyhedral {n : ℕ} {C : Set (Fin n → ℝ)} (hc : Convex ℝ C) : IsFinitelyGeneratedConvexSet n C → IsPolyhedralConvexSet n C

Helper for Theorem 19.1: finitely generated convex sets are polyhedral.

theorem polyhedral_closed_finiteFaces_finitelyGenerated_equiv {n : ℕ} {C : Set (Fin n → ℝ)} (hc : Convex ℝ C) : [IsPolyhedralConvexSet n C, IsClosed C ∧ {C' : Set (Fin n → ℝ) | IsFace C C'}.Finite, IsFinitelyGeneratedConvexSet n C].TFAE

Theorem 19.1: The following properties of a convex set C are equivalent: (a) C is polyhedral; (b) C is closed and has only finitely many faces; (c) C is finitely generated.

theorem helperForCorollary_19_1_1_isDirectionOf_posMul {n : ℕ} {C' : Set (Fin n → ℝ)} {d : Fin n → ℝ} (hd : IsDirectionOf C' d) {t : ℝ} (ht : 0 < t) : IsDirectionOf C' (t • d)

Helper for Corollary 19.1.1: positive multiples preserve IsDirectionOf.

theorem helperForCorollary_19_1_1_extremeDirection_posMul_closed {n : ℕ} {C : Set (Fin n → ℝ)} {d : Fin n → ℝ} (hd : IsExtremeDirection C d) {t : ℝ} (ht : 0 < t) : IsExtremeDirection C (t • d)

Helper for Corollary 19.1.1: positive multiples of an extreme direction are extreme directions.

theorem helperForCorollary_19_1_1_extremeDirection_ne_zero {n : ℕ} {C : Set (Fin n → ℝ)} {d : Fin n → ℝ} (hd : IsExtremeDirection C d) : d ≠ 0

Helper for Corollary 19.1.1: extreme directions are nonzero.

theorem helperForCorollary_19_1_1_infinite_extremeDirections_of_exists {n : ℕ} {C : Set (Fin n → ℝ)} : (∃ (d : Fin n → ℝ), IsExtremeDirection C d) → {d : Fin n → ℝ | IsExtremeDirection C d}.Infinite

Helper for Corollary 19.1.1: if any extreme direction exists, then there are infinitely many extreme-direction vectors.

theorem helperForCorollary_19_1_1_finite_extremeDirections_iff_not_exists {n : ℕ} {C : Set (Fin n → ℝ)} : {d : Fin n → ℝ | IsExtremeDirection C d}.Finite ↔ ¬∃ (d : Fin n → ℝ), IsExtremeDirection C d

Helper for Corollary 19.1.1: finiteness of extreme-direction vectors is equivalent to the absence of extreme directions.

theorem helperForCorollary_19_1_1_correct_direction_statement_via_representatives {n : ℕ} {C : Set (Fin n → ℝ)} : IsPolyhedralConvexSet n C → ∃ (S : Set (Fin n → ℝ)), S.Finite ∧ (∀ (d : Fin n → ℝ), IsExtremeDirection C d → ∃ d0 ∈ S, ∃ (t : ℝ), 0 < t ∧ d = t • d0) ∧ S ⊆ {d : Fin n → ℝ | IsExtremeDirection C d}

Helper for Corollary 19.1.1: polyhedral sets admit finitely many extreme-direction representatives up to positive scaling.

theorem helperForCorollary_19_1_1_fin1_eq_smul_one (x : Fin 1 → ℝ) : x = x 0 • fun (x : Fin 1) => 1

Helper for Corollary 19.1.1: in Fin 1 → ℝ, every vector is a multiple of the all-ones vector.

theorem helperForCorollary_19_1_1_dotProduct_neg_one (x : Fin 1 → ℝ) : (x ⬝ᵥ fun (x : Fin 1) => -1) = -x 0

Helper for Corollary 19.1.1: compute the dot product with the constant -1 vector in Fin 1 → ℝ.

theorem helperForCorollary_19_1_1_polyhedral_halfspace_fin1 : IsPolyhedralConvexSet 1 (closedHalfSpaceLE 1 (fun (x : Fin 1) => -1) 0)

Helper for Corollary 19.1.1: the nonnegative half-space in Fin 1 → ℝ is polyhedral.

theorem helperForCorollary_19_1_1_halfspace_fin1_isDirectionOf : IsDirectionOf (closedHalfSpaceLE 1 (fun (x : Fin 1) => -1) 0) fun (x : Fin 1) => 1

Helper for Corollary 19.1.1: the nonnegative half-space in Fin 1 → ℝ has direction vector 1.

theorem helperForCorollary_19_1_1_halfspace_fin1_extremeDirection : IsExtremeDirection (closedHalfSpaceLE 1 (fun (x : Fin 1) => -1) 0) fun (x : Fin 1) => 1

Helper for Corollary 19.1.1: the nonnegative half-space in Fin 1 → ℝ has an extreme direction.

theorem helperForCorollary_19_1_1_counterexample_polyhedral_has_extremeDirection : ∃ (C : Set (Fin 1 → ℝ)), IsPolyhedralConvexSet 1 C ∧ ∃ (d : Fin 1 → ℝ), IsExtremeDirection C d

Helper for Corollary 19.1.1: a polyhedral half-space in Fin 1 → ℝ has an extreme direction.

theorem helperForCorollary_19_1_1_counterexample_infinite_extremeDirections : ∃ (C : Set (Fin 1 → ℝ)), IsPolyhedralConvexSet 1 C ∧ {d : Fin 1 → ℝ | IsExtremeDirection C d}.Infinite

Helper for Corollary 19.1.1: a polyhedral set can have infinitely many extreme-direction vectors.

theorem helperForCorollary_19_1_1_counterexample_not_finite_extremeDirections : ∃ (C : Set (Fin 1 → ℝ)), IsPolyhedralConvexSet 1 C ∧ ¬{d : Fin 1 → ℝ | IsExtremeDirection C d}.Finite

Helper for Corollary 19.1.1: the extreme-direction set for a polyhedral half-space in Fin 1 → ℝ is not finite.

theorem helperForCorollary_19_1_1_statement_false_fin1 : ¬∀ (C : Set (Fin 1 → ℝ)), IsPolyhedralConvexSet 1 C → {x : Fin 1 → ℝ | IsExtremePoint C x}.Finite ∧ {d : Fin 1 → ℝ | IsExtremeDirection C d}.Finite

Helper for Corollary 19.1.1: the statement fails already in dimension 1.

theorem helperForCorollary_19_1_1_statement_false_global : ¬∀ (n : ℕ) (C : Set (Fin n → ℝ)), IsPolyhedralConvexSet n C → {x : Fin n → ℝ | IsExtremePoint C x}.Finite ∧ {d : Fin n → ℝ | IsExtremeDirection C d}.Finite

Helper for Corollary 19.1.1: the global finite-extreme-direction-vector claim is false, as witnessed by the dimension-1 counterexample.

theorem helperForCorollary_19_1_1_finite_extremePoints_of_polyhedral {n : ℕ} {C : Set (Fin n → ℝ)} : IsPolyhedralConvexSet n C → {x : Fin n → ℝ | IsExtremePoint C x}.Finite

Helper for Corollary 19.1.1: polyhedral sets have finitely many extreme points.

theorem polyhedralConvexSet_finite_extremePoints_extremeDirectionRepresentatives (n : ℕ) (C : Set (Fin n → ℝ)) : IsPolyhedralConvexSet n C → {x : Fin n → ℝ | IsExtremePoint C x}.Finite ∧ ∃ (S : Set (Fin n → ℝ)), S.Finite ∧ (∀ (d : Fin n → ℝ), IsExtremeDirection C d → ∃ d0 ∈ S, ∃ (t : ℝ), 0 < t ∧ d = t • d0) ∧ S ⊆ {d : Fin n → ℝ | IsExtremeDirection C d}

Helper for Corollary 19.1.1: corrected direction claim via finitely many extreme-direction representatives up to positive scaling.

theorem polyhedralConvexSet_finite_extremePoints_extremeDirections (n : ℕ) (C : Set (Fin n → ℝ)) : IsPolyhedralConvexSet n C → {x : Fin n → ℝ | IsExtremePoint C x}.Finite ∧ ∃ (S : Set (Fin n → ℝ)), S.Finite ∧ (∀ (d : Fin n → ℝ), IsExtremeDirection C d → ∃ d0 ∈ S, ∃ (t : ℝ), 0 < t ∧ d = t • d0) ∧ S ⊆ {d : Fin n → ℝ | IsExtremeDirection C d}

Corollary 19.1.1 (formalized via rays): A polyhedral convex set has at most a finite number of extreme points and finitely many extreme-direction representatives up to positive scaling.

def IsPolyhedralConvexFunction (n : ℕ) (f : (Fin n → ℝ) → EReal) : Prop

Text 19.0.8: A convex function f : ℝ^n → (-∞, +∞] is called polyhedral convex if its epigraph epi f = {(x, μ) ∈ ℝ^{n+1} | f x ≤ μ} is a polyhedral convex set in ℝ^{n+1}.

Equations

• IsPolyhedralConvexFunction n f = (ConvexFunctionOn Set.univ f ∧ IsPolyhedralConvexSet (n + 1) ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ f))

theorem helperForText_19_0_9_rhsRepresentation_ne_bot {n k m : ℕ} {b : Fin m → Fin n → ℝ} {β : Fin m → ℝ} {x : Fin n → ℝ} : ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x ≠ ⊥

Helper for Text 19.0.9: every value of the max-affine-plus-indicator expression is different from ⊥.

theorem helperForText_19_0_9_representable_pointwise_ne_bot {n : ℕ} {f : (Fin n → ℝ) → EReal} (hrepr : ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x) (x : Fin n → ℝ) : f x ≠ ⊥

Helper for Text 19.0.9: any function with the theorem's max-affine-plus-indicator representation never takes the value ⊥.

theorem helperForText_19_0_9_constBot_ne_rhsRepresentation {n k m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) : (fun (x : Fin n → ℝ) => ⊥) ≠ fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x

Helper for Text 19.0.9: the max-affine-plus-indicator schema is never the constant ⊥ function.

theorem helperForText_19_0_9_representable_ne_constBot {n : ℕ} {f : (Fin n → ℝ) → EReal} (hrepr : ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x) : f ≠ fun (x : Fin n → ℝ) => ⊥

Helper for Text 19.0.9: any function admitting the theorem's max-affine-plus-indicator representation is not the constant bottom function.

theorem helperForText_19_0_9_representation_implies_nonbot_and_ne_constBot {n : ℕ} {f : (Fin n → ℝ) → EReal} (hrepr : ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x) : (∀ (x : Fin n → ℝ), f x ≠ ⊥) ∧ f ≠ fun (x : Fin n → ℝ) => ⊥

Helper for Text 19.0.9: a max-affine-plus-indicator representation yields both pointwise non-⊥ values and global non-constancy at ⊥.

theorem helperForText_19_0_9_constBot_isPolyhedralConvexFunction (n : ℕ) : IsPolyhedralConvexFunction n fun (x : Fin n → ℝ) => ⊥

Helper for Text 19.0.9: the constant function x ↦ ⊥ satisfies IsPolyhedralConvexFunction in the present formalization.

theorem helperForText_19_0_9_constBot_not_representable (n : ℕ) : ¬∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ (fun (x : Fin n → ℝ) => ⊥) = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x

Helper for Text 19.0.9: the constant function x ↦ ⊥ cannot be represented by the max-affine-plus-indicator normal form from the theorem statement.

theorem helperForText_19_0_9_constBot_counterexample_data (n : ℕ) : (IsPolyhedralConvexFunction n fun (x : Fin n → ℝ) => ⊥) ∧ ¬∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ (fun (x : Fin n → ℝ) => ⊥) = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x

Helper for Text 19.0.9: the constant function x ↦ ⊥ provides both sides of the counterexample data used to refute the biconditional schema.

theorem helperForText_19_0_9_schema_at_polyhedral_function_implies_pointwise_ne_bot {n : ℕ} {f : (Fin n → ℝ) → EReal} (hSchemaAtF : IsPolyhedralConvexFunction n f ↔ ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x) (hPoly : IsPolyhedralConvexFunction n f) (x : Fin n → ℝ) : f x ≠ ⊥

Helper for Text 19.0.9: if the biconditional schema is assumed at a fixed polyhedral-convex function f, then f must be pointwise non-⊥.

theorem helperForText_19_0_9_constBot_schema_implies_false (n : ℕ) (hSchemaAtConstBot : (IsPolyhedralConvexFunction n fun (x : Fin n → ℝ) => ⊥) ↔ ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ (fun (x : Fin n → ℝ) => ⊥) = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x) : False

Helper for Text 19.0.9: the constant-⊥ instance of the biconditional schema forces a contradiction with pointwise non-⊥.

theorem helperForText_19_0_9_constBot_breaks_biconditional (n : ℕ) : ¬((IsPolyhedralConvexFunction n fun (x : Fin n → ℝ) => ⊥) ↔ ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ (fun (x : Fin n → ℝ) => ⊥) = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x)

Helper for Text 19.0.9: instantiating the theorem schema at the constant-⊥ function yields a contradiction in the current EReal formalization.

theorem helperForText_19_0_9_exists_function_counterexample_at_dimension (n : ℕ) : ∃ (f : (Fin n → ℝ) → EReal), ¬(IsPolyhedralConvexFunction n f ↔ ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x)

Helper for Text 19.0.9: in each fixed dimension n, the constant-⊥ function is an explicit witness where the biconditional schema fails.

theorem helperForText_19_0_9_not_forall_function_schema (n : ℕ) : ¬∀ (f : (Fin n → ℝ) → EReal), IsPolyhedralConvexFunction n f ↔ ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x

Helper for Text 19.0.9: the target biconditional schema cannot hold for all functions f : ℝ^n → EReal, since it fails at the constant-⊥ function.

theorem helperForText_19_0_9_exists_counterexample_to_schema : ∃ (n : ℕ) (f : (Fin n → ℝ) → EReal), ¬(IsPolyhedralConvexFunction n f ↔ ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x)

Helper for Text 19.0.9: a concrete (n, f) witness shows the target schema fails at the constant-⊥ function.

theorem helperForText_19_0_9_global_schema_implies_false (hGlobal : ∀ (n : ℕ) (f : (Fin n → ℝ) → EReal), IsPolyhedralConvexFunction n f ↔ ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x) : False

Helper for Text 19.0.9: if the biconditional schema held for all dimensions and functions, it would contradict the explicit counterexample.

theorem helperForText_19_0_9_no_global_theorem_schema : ¬∀ (n : ℕ) (f : (Fin n → ℝ) → EReal), IsPolyhedralConvexFunction n f ↔ ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x

Helper for Text 19.0.9: a theorem-schema claiming the biconditional for all dimensions and functions is refuted by the constant-⊥ counterexample.

theorem helperForText_19_0_9_affineConstraintSet_polyhedral {n k m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) : IsPolyhedralConvexSet (n + 1) {z : Fin (n + 1) → ℝ | ∀ (i : Fin m), ↑i < k → (z ⬝ᵥ fun (i_1 : Fin (n + 1)) => Fin.cases (-1) (b i) i_1) ≤ β i}

Helper for Text 19.0.9: the finite family of affine-epigraph inequalities with normals (b_i, -1) defines a polyhedral set in ℝ^(n+1).

theorem helperForText_19_0_9_liftedIndicatorConstraintSet_polyhedral {n k m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) : IsPolyhedralConvexSet (n + 1) {z : Fin (n + 1) → ℝ | ∀ (i : Fin m), k ≤ ↑i → (z ⬝ᵥ fun (i_1 : Fin (n + 1)) => Fin.cases 0 (b i) i_1) ≤ β i}

Helper for Text 19.0.9: the finite family of domain inequalities with normals (b_i, 0) defines a polyhedral set in ℝ^(n+1).

theorem helperForText_19_0_9_liftedConstraintIntersection_polyhedral {n k m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) : IsPolyhedralConvexSet (n + 1) ({z : Fin (n + 1) → ℝ | ∀ (i : Fin m), ↑i < k → (z ⬝ᵥ fun (i_1 : Fin (n + 1)) => Fin.cases (-1) (b i) i_1) ≤ β i} ∩ {z : Fin (n + 1) → ℝ | ∀ (i : Fin m), k ≤ ↑i → (z ⬝ᵥ fun (i_1 : Fin (n + 1)) => Fin.cases 0 (b i) i_1) ≤ β i})

Helper for Text 19.0.9: intersecting the affine-epigraph and lifted-domain constraint families yields a polyhedral set in ℝ^(n+1).

theorem helperForText_19_0_9_empty_transformedEpigraph_implies_representation {n : ℕ} {f : (Fin n → ℝ) → EReal} (hEmpty : (fun (p : (Fin n → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ f = ∅) : ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x

Helper for Text 19.0.9: if the transformed epigraph image is empty, then f admits the max-affine-plus-indicator representation (the f = ⊤ branch).

theorem helperForText_19_0_9_polyhedral_nonbot_implies_representation_of_empty_transformedEpigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} (_hpolyNonbot : IsPolyhedralConvexFunction n f ∧ ∀ (x : Fin n → ℝ), f x ≠ ⊥) (hEmpty : (fun (p : (Fin n → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ f = ∅) : ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x

Helper for Text 19.0.9: in the forward direction, the empty transformed-epigraph branch is discharged by the dedicated f = ⊤ representation lemma.

theorem helperForText_19_0_9_representation_implies_pointwise_nonbot_sideCondition {n : ℕ} {f : (Fin n → ℝ) → EReal} (hrepr : ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x) (x : Fin n → ℝ) : f x ≠ ⊥

Helper for Text 19.0.9: any represented function satisfies the theorem's pointwise non-⊥ side condition.

theorem helperForText_19_0_9_mem_transformedImage_coordEuclid_transport {n : ℕ} {S : Set (EuclideanSpace ℝ (Fin (n + 1)))} {z : Fin (n + 1) → ℝ} : WithLp.toLp 2 z ∈ S ↔ z ∈ WithLp.toLp 2 ⁻¹' S

Helper for Text 19.0.9: membership in a transformed-image subset of Euclidean space can be transported to function coordinates via WithLp.toLp.

theorem helperForText_19_0_9_prodLinearEquivAppendCoord_symm_eq {n : ℕ} (z : Fin (n + 1) → ℝ) : (prodLinearEquiv_append_coord n).symm z = prodLinearEquiv_append.symm (WithLp.toLp 2 z)

Helper for Text 19.0.9: unpacking prodLinearEquiv_append_coord equals unpacking prodLinearEquiv_append after the coordinate-to-Euclidean coercion.

theorem helperForText_19_0_9_prodLinearEquivAppendCoord_castSucc {n : ℕ} (x0 : Fin n → ℝ) (μ0 : ℝ) (j0 : Fin n) : x0 j0 = (prodLinearEquiv_append_coord n) (x0, μ0) j0.castSucc

Helper for Text 19.0.9: the packed-coordinate embedding recovers each base coordinate at Fin.castSucc.

theorem helperForText_19_0_9_prodLinearEquivAppendCoord_last {n : ℕ} (x0 : Fin n → ℝ) (μ0 : ℝ) : μ0 = (prodLinearEquiv_append_coord n) (x0, μ0) (Fin.last n)

Helper for Text 19.0.9: the last packed coordinate equals the appended scalar.

theorem helperForText_19_0_9_dotProduct_prodLinearEquivAppendCoord {n : ℕ} (p q : (Fin n → ℝ) × ℝ) : (prodLinearEquiv_append_coord n) p ⬝ᵥ (prodLinearEquiv_append_coord n) q = p.1 ⬝ᵥ q.1 + p.2 * q.2

Helper for Text 19.0.9: dot product in packed coordinates splits as base dot product plus product of the appended scalar coordinates.

theorem helperForText_19_0_9_dotPacked_point {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m) (y : Fin (n + 1) → ℝ) : y ⬝ᵥ (prodLinearEquiv_append_coord n) (b i, -1) = b i ⬝ᵥ ((prodLinearEquiv_append_coord n).symm y).1 - ((prodLinearEquiv_append_coord n).symm y).2

Helper for Text 19.0.9: dot products against packed normals (b_i, -1) decode to the affine expression dotProduct (b_i) x - μ at pulled-back coordinates.

theorem helperForText_19_0_9_dotPacked_direction {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m) (y : Fin (n + 1) → ℝ) : y ⬝ᵥ (prodLinearEquiv_append_coord n) (b i, 0) = b i ⬝ᵥ ((prodLinearEquiv_append_coord n).symm y).1

Helper for Text 19.0.9: dot products against packed normals (b_i, 0) decode to dotProduct (b_i) x at pulled-back coordinates.

theorem helperForText_19_0_9_transformedEpigraphImage_upwardClosed_lastCoord {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ t : ℝ} (hy : prodLinearEquiv_append (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ f) (ht : 0 ≤ t) : prodLinearEquiv_append (x, μ + t) ∈ (fun (p : (Fin n → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ f

Helper for Text 19.0.9: the transformed-epigraph image is upward closed in the last coordinate at fixed base point.

theorem helperForText_19_0_9_nonempty_transformedEpigraphImage_unpack {n : ℕ} {f : (Fin n → ℝ) → EReal} (hNonempty : ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ f).Nonempty) : ∃ (x : Fin n → ℝ) (μ : ℝ), f x ≤ ↑μ

Helper for Text 19.0.9: nonemptiness of the transformed-epigraph image yields a base point and scalar with finite-epigraph inequality data.

theorem helperForText_19_0_9_mem_transformedEpigraphImage_iff_mem_epigraph_univ {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ} : prodLinearEquiv_append (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ f ↔ (x, μ) ∈ epigraph Set.univ f

Helper for Text 19.0.9: transformed-epigraph image membership at a packed point is equivalent to ordinary epigraph membership at the unpacked point.

theorem helperForText_19_0_9_nonempty_polyhedral_transformedImage_extract_rawHalfspaces {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpoly : IsPolyhedralConvexFunction n f) : ∃ (m : ℕ) (a : Fin m → Fin (n + 1) → ℝ) (α : Fin m → ℝ), (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ f = ⋂ (i : Fin m), closedHalfSpaceLE (n + 1) (a i) (α i)

Helper for Text 19.0.9: polyhedrality of the transformed epigraph image yields a finite raw halfspace presentation.

theorem helperForText_19_0_9_kZero_splitHalfspaces_allow_negativeLastCoord {n m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) (hfeas : ∃ (x0 : Fin n → ℝ), ∀ (i : Fin m), ∑ j : Fin n, x0 j * b i j ≤ β i) : have g := fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < 0 ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), 0 ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x; have _Simg := (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ g; have Ssplit := {z : Fin (n + 1) → ℝ | ∀ (i : Fin m), ↑i < 0 → (z ⬝ᵥ fun (i_1 : Fin (n + 1)) => Fin.cases (-1) (b i) i_1) ≤ β i} ∩ {z : Fin (n + 1) → ℝ | ∀ (i : Fin m), 0 ≤ ↑i → (z ⬝ᵥ fun (i_1 : Fin (n + 1)) => Fin.cases 0 (b i) i_1) ≤ β i}; ∃ (y0 : Fin (n + 1) → ℝ), y0 ∈ Ssplit

Helper for Text 19.0.9: in the k = 0 branch, feasibility of the domain-inequality family yields a witness that the split-halfspace set is nonempty.

theorem helperForText_19_0_9_transformedImage_eq_implies_function_eq {n : ℕ} {f g : (Fin n → ℝ) → EReal} (hImageEq : (fun (p : (Fin n → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ f = (fun (p : (Fin n → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ g) : f = g

Helper for Text 19.0.9: equality of transformed-epigraph images determines the underlying EReal-valued function uniquely.

theorem helperForText_19_0_9_transformedImageCoord_eq_implies_function_eq {n : ℕ} {f g : (Fin n → ℝ) → EReal} (hImageEq : (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f = (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ g) : f = g

Helper for Text 19.0.9: equality of packed-coordinate transformed-epigraph images determines the underlying EReal-valued function uniquely.

theorem helperForText_19_0_9_lastCoordGuard_polyhedral {n : ℕ} : IsPolyhedralConvexSet (n + 1) {z : Fin (n + 1) → ℝ | 0 ≤ ((prodLinearEquiv_append_coord n).symm z).2}

Helper for Text 19.0.9: the lower-bound guard on the unpacked scalar coordinate is a polyhedral halfspace in packed coordinates.

theorem helperForText_19_0_9_guardedSplitConstraintSet_polyhedral {n k m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) : IsPolyhedralConvexSet (n + 1) ({z : Fin (n + 1) → ℝ | ∀ (i : Fin m), ↑i < k → z ⬝ᵥ (prodLinearEquiv_append_coord n) (b i, -1) ≤ β i} ∩ {z : Fin (n + 1) → ℝ | ∀ (i : Fin m), k ≤ ↑i → z ⬝ᵥ (prodLinearEquiv_append_coord n) (b i, 0) ≤ β i} ∩ if k = 0 then {z : Fin (n + 1) → ℝ | 0 ≤ ((prodLinearEquiv_append_coord n).symm z).2} else Set.univ)

Helper for Text 19.0.9: the guarded packed-normal constraint form is polyhedral.

theorem helperForText_19_0_9_dotPacked_point_finCases_normalForm {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m) (y : Fin (n + 1) → ℝ) : y ⬝ᵥ (prodLinearEquiv_append_coord n) (b i, -1) = b i ⬝ᵥ ((prodLinearEquiv_append_coord n).symm y).1 - ((prodLinearEquiv_append_coord n).symm y).2

Helper for Text 19.0.9: packed normals with last coordinate -1 decode to the split affine expression after unpacking coordinates.

theorem helperForText_19_0_9_dotPacked_direction_finCases_normalForm {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m) (y : Fin (n + 1) → ℝ) : y ⬝ᵥ (prodLinearEquiv_append_coord n) (b i, 0) = b i ⬝ᵥ ((prodLinearEquiv_append_coord n).symm y).1

Helper for Text 19.0.9: packed-direction normals with last coordinate 0 decode to the base-coordinate dot product after unpacking.

theorem helperForText_19_0_9_packedNormal_point_eq_finCases {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m) (j : Fin n) : (prodLinearEquiv_append_coord n) (b i, -1) j.castSucc = b i j

Helper for Text 19.0.9: evaluating the packed normal (b_i, -1) at base coordinates recovers the coefficient function b_i.

theorem helperForText_19_0_9_packedNormal_direction_eq_finCases {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m) (j : Fin n) : (prodLinearEquiv_append_coord n) (b i, 0) j.castSucc = b i j

Helper for Text 19.0.9: evaluating the packed normal (b_i, 0) at base coordinates recovers the coefficient function b_i.

theorem helperForText_19_0_9_representation_le_implies_domain_membership {n k m : ℕ} {b : Fin m → Fin n → ℝ} {β : Fin m → ℝ} {x : Fin n → ℝ} {μ : ℝ} (hgμ : ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x ≤ ↑μ) : x ∈ {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i}

Helper for Text 19.0.9: an epigraph upper bound on the represented value at x forces x to satisfy all domain-side inequalities.

theorem helperForText_19_0_9_representation_le_implies_sup_bound {n k m : ℕ} {b : Fin m → Fin n → ℝ} {β : Fin m → ℝ} {x : Fin n → ℝ} {μ : ℝ} (hgμ : ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x ≤ ↑μ) : sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i} ≤ μ

Helper for Text 19.0.9: the same represented upper bound yields an upper bound on the corresponding affine supremum term.

theorem helperForText_19_0_9_representation_le_implies_active_affine_bound {n k m : ℕ} {b : Fin m → Fin n → ℝ} {β : Fin m → ℝ} {x : Fin n → ℝ} {μ : ℝ} (hgμ : ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x ≤ ↑μ) (i : Fin m) (hi : ↑i < k) : ∑ j : Fin n, x j * b i j - β i ≤ μ

Helper for Text 19.0.9: each active affine piece (i < k) is bounded above by μ whenever the represented value at x is bounded by μ.

theorem helperForText_19_0_9_dotFinCasesNormals_unpacked_normalForm {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m) (z : Fin (n + 1) → ℝ) : (z ⬝ᵥ fun (i_1 : Fin (n + 1)) => Fin.cases (-1) (b i) i_1) = z 0 * -1 + ∑ j : Fin n, z j.succ * b i j ∧ (z ⬝ᵥ fun (i_1 : Fin (n + 1)) => Fin.cases 0 (b i) i_1) = ∑ j : Fin n, z j.succ * b i j

Helper for Text 19.0.9: dot products against the Fin.cases split normals expand into the zero-coordinate term plus the succ-indexed base sum.

theorem helperForText_19_0_9_counterexample_mem_transformedImage : have g := fun (x : Fin 1 → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin 1), ↑i < 1 ∧ r = ∑ j : Fin 1, x j * 0 - 0}) + indicatorFunction {y : Fin 1 → ℝ | ∀ (i : Fin 1), 1 ≤ ↑i → ∑ j : Fin 1, y j * 0 ≤ 0} x; have z0 := (prodLinearEquiv_append (fun (x : Fin 1) => -1, 0)).ofLp; z0 ∈ (fun (p : (Fin 1 → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ g

Helper for Text 19.0.9: for n = 1, k = m = 1, and zero coefficients, the packed point corresponding to (x, μ) = (-1, 0) belongs to the transformed epigraph image of the represented function.

theorem helperForText_19_0_9_counterexample_not_mem_finCases_split : have z0 := (prodLinearEquiv_append (fun (x : Fin 1) => -1, 0)).ofLp; z0 ∉ {z : Fin 2 → ℝ | ∀ (i : Fin 1), ↑i < 1 → (z ⬝ᵥ fun (i : Fin (1 + 1)) => Fin.cases (-1) (fun (x : Fin 1) => 0) i) ≤ 0} ∩ {z : Fin 2 → ℝ | ∀ (i : Fin 1), 1 ≤ ↑i → (z ⬝ᵥ fun (i : Fin (1 + 1)) => Fin.cases 0 (fun (x : Fin 1) => 0) i) ≤ 0}

Helper for Text 19.0.9: under the same concrete data, the point above violates the split Fin.cases affine-constraint family.

theorem helperForText_19_0_9_counterexample_transformedImage_ne_finCases_split : have g := fun (x : Fin 1 → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin 1), ↑i < 1 ∧ r = ∑ j : Fin 1, x j * 0 - 0}) + indicatorFunction {y : Fin 1 → ℝ | ∀ (i : Fin 1), 1 ≤ ↑i → ∑ j : Fin 1, y j * 0 ≤ 0} x; have Simg := (fun (p : (Fin 1 → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ g; have Ssplit := {z : Fin 2 → ℝ | ∀ (i : Fin 1), ↑i < 1 → (z ⬝ᵥ fun (i : Fin (1 + 1)) => Fin.cases (-1) (fun (x : Fin 1) => 0) i) ≤ 0} ∩ {z : Fin 2 → ℝ | ∀ (i : Fin 1), 1 ≤ ↑i → (z ⬝ᵥ fun (i : Fin (1 + 1)) => Fin.cases 0 (fun (x : Fin 1) => 0) i) ≤ 0}; Simg ≠ Ssplit

Helper for Text 19.0.9: the concrete one-dimensional witness separates the transformed epigraph image from the split Fin.cases constraints.

theorem helperForText_19_0_9_representation_transformedImage_eq_constraints_with_lastCoord_guard {n k m : ℕ} (hk : k ≤ m) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) : have g := fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x; have Simg := (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ g; have Ssplit := {z : Fin (n + 1) → ℝ | ∀ (i : Fin m), ↑i < k → z ⬝ᵥ (prodLinearEquiv_append_coord n) (b i, -1) ≤ β i} ∩ {z : Fin (n + 1) → ℝ | ∀ (i : Fin m), k ≤ ↑i → z ⬝ᵥ (prodLinearEquiv_append_coord n) (b i, 0) ≤ β i}; have Sguard := {z : Fin (n + 1) → ℝ | 0 ≤ ((prodLinearEquiv_append_coord n).symm z).2}; Simg = Ssplit ∩ if k = 0 then Sguard else Set.univ

Helper for Text 19.0.9: a max-affine-plus-indicator representation has transformed epigraph image equal to packed-normal constraints with the k = 0 last-coordinate guard.

theorem helperForText_19_0_9_convexFunctionOn_of_polyhedralTransformedEpigraph {n : ℕ} {g : (Fin n → ℝ) → EReal} (hpoly : IsPolyhedralConvexSet (n + 1) ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ g)) : ConvexFunctionOn Set.univ g

Helper for Text 19.0.9: polyhedrality of the transformed-epigraph image implies convexity of the represented function on univ.

theorem helperForText_19_0_9_rawHalfspaces_lastCoord_nonpos {n m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin (n + 1) → ℝ} {α : Fin m → ℝ} (hRaw : (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ f = ⋂ (i : Fin m), closedHalfSpaceLE (n + 1) (a i) (α i)) (hNonempty : ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ f).Nonempty) (i : Fin m) : a i (Fin.last n) ≤ 0

Helper for Text 19.0.9: in a nonempty raw halfspace presentation of the transformed epigraph image, each raw normal has nonpositive last coordinate.

theorem helperForText_19_0_9_nonempty_nonbot_forces_negative_lastCoeff_constraint {n m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin (n + 1) → ℝ} {α : Fin m → ℝ} (hRaw : (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ f = ⋂ (i : Fin m), closedHalfSpaceLE (n + 1) (a i) (α i)) (hNonempty : ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ f).Nonempty) (hnonbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) : ∃ (i : Fin m), a i (Fin.last n) < 0

Helper for Text 19.0.9: from a nonempty transformed epigraph image and the repaired polyhedral/non-⊥ hypotheses, reconstruct a max-affine-plus-indicator representation.

theorem helperForText_19_0_9_lastCoord_nonpos_partition_neg_or_zero {n m : ℕ} {a : Fin m → Fin (n + 1) → ℝ} (hLastCoeffNonpos : ∀ (i : Fin m), a i (Fin.last n) ≤ 0) (i : Fin m) : a i (Fin.last n) < 0 ∨ a i (Fin.last n) = 0

Helper for Text 19.0.9: under a nonpositive last-coordinate hypothesis, each raw normal is classified as either strictly negative or exactly zero on the last coordinate.

theorem helperForText_19_0_9_negativeIndex_nonempty_implies_k_ne_zero_for_blockData {n m : ℕ} {a : Fin m → Fin (n + 1) → ℝ} (hHasNegativeLastCoeff : ∃ (i : Fin m), a i (Fin.last n) < 0) : let Ineg := { i : Fin m // a i (Fin.last n) < 0 }; have k := Fintype.card Ineg; k ≠ 0

Helper for Text 19.0.9: if one raw halfspace has strictly negative last coefficient, then the subtype of negative-index constraints is nonempty, so its finite cardinal is nonzero.

theorem helperForText_19_0_9_rawHalfspaces_to_finBlockPackedRepresentationData {n : ℕ} {f : (Fin n → ℝ) → EReal} {m : ℕ} {a : Fin m → Fin (n + 1) → ℝ} {α : Fin m → ℝ} (hRawPresentation : (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ f = ⋂ (i : Fin m), closedHalfSpaceLE (n + 1) (a i) (α i)) (hLastCoeffNonpos : ∀ (i : Fin m), a i (Fin.last n) ≤ 0) (hHasNegativeLastCoeff : ∃ (i : Fin m), a i (Fin.last n) < 0) : ∃ (k : ℕ) (m' : ℕ) (b : Fin m' → Fin n → ℝ) (β : Fin m' → ℝ), 0 < k ∧ k ≤ m' ∧ (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ f = {z : Fin (n + 1) → ℝ | ∀ (i : Fin m'), ↑i < k → z ⬝ᵥ (prodLinearEquiv_append_coord n) (b i, -1) ≤ β i} ∩ {z : Fin (n + 1) → ℝ | ∀ (i : Fin m'), k ≤ ↑i → z ⬝ᵥ (prodLinearEquiv_append_coord n) (b i, 0) ≤ β i} ∩ if k = 0 then {z : Fin (n + 1) → ℝ | 0 ≤ ((prodLinearEquiv_append_coord n).symm z).2} else Set.univ

Helper for Text 19.0.9: convert a nonempty transformed-epigraph raw halfspace presentation with nonpositive/negative last-coordinate data into finite split packed constraints in the exact guarded normal form.

theorem helperForText_19_0_9_nonempty_forward_branch_finish_from_finBlockData {n : ℕ} {f : (Fin n → ℝ) → EReal} {k m' : ℕ} {b : Fin m' → Fin n → ℝ} {β : Fin m' → ℝ} (hk_le_m' : k ≤ m') (hSimgEqGuarded : (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ f = {z : Fin (n + 1) → ℝ | ∀ (i : Fin m'), ↑i < k → z ⬝ᵥ (prodLinearEquiv_append_coord n) (b i, -1) ≤ β i} ∩ {z : Fin (n + 1) → ℝ | ∀ (i : Fin m'), k ≤ ↑i → z ⬝ᵥ (prodLinearEquiv_append_coord n) (b i, 0) ≤ β i} ∩ if k = 0 then {z : Fin (n + 1) → ℝ | 0 ≤ ((prodLinearEquiv_append_coord n).symm z).2} else Set.univ) : ∃ (k' : ℕ) (m'' : ℕ) (b' : Fin m'' → Fin n → ℝ) (β' : Fin m'' → ℝ), k' ≤ m'' ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m''), ↑i < k' ∧ r = ∑ j : Fin n, x j * b' i j - β' i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m''), k' ≤ ↑i → ∑ j : Fin n, y j * b' i j ≤ β' i} x

Helper for Text 19.0.9: once finite split packed-constraint data is available for the transformed epigraph image, transport through the representation-image identity and conclude equality of functions.

theorem helperForText_19_0_9_polyhedral_nonbot_implies_representation_of_nonempty_transformedEpigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpolyNonbot : IsPolyhedralConvexFunction n f ∧ ∀ (x : Fin n → ℝ), f x ≠ ⊥) (hNonempty : ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ f).Nonempty) : ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x

Helper for Text 19.0.9: from a nonempty transformed epigraph image and the repaired polyhedral/non-⊥ hypotheses, reconstruct a max-affine-plus-indicator representation.

theorem helperForText_19_0_9_representation_implies_polyhedralConvexFunction_via_transformedImage {n : ℕ} {f : (Fin n → ℝ) → EReal} (hrepr : ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x) : IsPolyhedralConvexFunction n f

Helper for Text 19.0.9: any max-affine-plus-indicator representation induces IsPolyhedralConvexFunction via transformed-epigraph polyhedrality.

theorem polyhedral_convex_function_iff_max_affine_plus_indicator (n : ℕ) (f : (Fin n → ℝ) → EReal) : (IsPolyhedralConvexFunction n f ∧ ∀ (x : Fin n → ℝ), f x ≠ ⊥) ↔ ∃ (k : ℕ) (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), k ≤ m ∧ f = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction {y : Fin n → ℝ | ∀ (i : Fin m), k ≤ ↑i → ∑ j : Fin n, y j * b i j ≤ β i} x

Text 19.0.9: A convex function f on ℝ^n is polyhedral convex iff it can be expressed as f = h + δ(· | C), where h(x) is the maximum of finitely many affine functions ⟨x, b_i⟩ - β_i, and C is the intersection of finitely many closed half-spaces ⟨x, b_i⟩ ≤ β_i. In this EReal formalization, the codomain condition f : ℝ^n → (-∞, +∞] is encoded by the pointwise non-⊥ hypothesis.

def IsFinitelyGeneratedConvexFunction (n : ℕ) (f : (Fin n → ℝ) → EReal) : Prop

Text 19.0.10: A convex function f is finitely generated if there exist vectors a₁, …, a_m and scalars α_i such that for every x, f x is the infimum of ∑ i, λ i * α i over coefficients λ_i with ∑ i, λ i • a_i = x, ∑_{i < k} λ_i = 1, and λ_i ≥ 0 for all i = 1, …, m.

Equations

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

theorem helperForText_19_0_10_constraintBundle_wellTyped {n k m : ℕ} {a : Fin m → Fin n → ℝ} {x : Fin n → ℝ} {lam : Fin m → ℝ} (hlin : ∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) (hnorm : ∑ i : Fin m with ↑i < k, lam i = 1) (hnonneg : ∀ (i : Fin m), 0 ≤ lam i) : (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ ∀ (i : Fin m), 0 ≤ lam i

Helper for Text 19.0.10: the coefficient constraints appearing in the finitely generated representation can be read as one bundled conjunction.

theorem helperForText_19_0_10_objective_cast_toEReal {m : ℕ} {lam α : Fin m → ℝ} {r : EReal} (hr : r = ↑(∑ i : Fin m, lam i * α i)) : ∃ (q : ℝ), r = ↑q

Helper for Text 19.0.10: the linear objective naturally provides an EReal value via coercion from ℝ.

theorem helperForText_19_0_10_objective_mem_representationSet {n k m : ℕ} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} {x : Fin n → ℝ} {lam : Fin m → ℝ} (hlin : ∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) (hnorm : ∑ i : Fin m with ↑i < k, lam i = 1) (hnonneg : ∀ (i : Fin m), 0 ≤ lam i) : ↑(∑ i : Fin m, lam i * α i) ∈ {r : EReal | ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ r = ↑(∑ i : Fin m, lam i * α i)}

Helper for Text 19.0.10: any feasible coefficient family contributes its linear objective value as an element of the representation infimum set.

theorem helperForText_19_0_10_noProofObligation {n : ℕ} {f : (Fin n → ℝ) → EReal} : IsFinitelyGeneratedConvexFunction n f → ConvexFunctionOn Set.univ f

Helper for Text 19.0.10: unpacking the definition immediately yields convexity on univ, so this definition introduces no extra proof obligation beyond its fields.

theorem helperForCorollary_19_1_2_unpack_finitelyGeneratedData {n : ℕ} {f : (Fin n → ℝ) → EReal} : IsFinitelyGeneratedConvexFunction n f → ∃ (k : ℕ) (m : ℕ) (a : Fin m → Fin n → ℝ) (α : Fin m → ℝ), k ≤ m ∧ ∀ (x : Fin n → ℝ), f x = sInf {r : EReal | ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ r = ↑(∑ i : Fin m, lam i * α i)}

Helper for Corollary 19.1.2: unpack the global finite-generation data from the definition.

theorem helperForCorollary_19_1_2_exists_feasibleCoeffs_lt_mu {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hrepr : ∀ (x : Fin n → ℝ), f x = sInf {r : EReal | ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ r = ↑(∑ i : Fin m, lam i * α i)}) {x : Fin n → ℝ} {μ : ℝ} (hfx_lt : f x < ↑μ) : ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ ↑(∑ i : Fin m, lam i * α i) < ↑μ

Helper for Corollary 19.1.2: strict epigraph inequality at (x, μ) yields feasible Text 19.0.10 coefficients whose objective value is strictly below μ.

theorem helperForCorollary_19_1_2_mem_epigraph_univ_of_feasible_obj_le {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hrepr : ∀ (x : Fin n → ℝ), f x = sInf {r : EReal | ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ r = ↑(∑ i : Fin m, lam i * α i)}) {x : Fin n → ℝ} {μ : ℝ} {lam : Fin m → ℝ} (hlin : ∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) (hnorm : ∑ i : Fin m with ↑i < k, lam i = 1) (hnonneg : ∀ (i : Fin m), 0 ≤ lam i) (hobj_le : ∑ i : Fin m, lam i * α i ≤ μ) : (x, μ) ∈ epigraph Set.univ f

Helper for Corollary 19.1.2: any feasible Text 19.0.10 coefficients whose objective value is bounded above by μ certify epigraph membership at (x, μ).

theorem helperForCorollary_19_1_2_mem_epigraph_univ_of_feasible_obj_lt {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hrepr : ∀ (x : Fin n → ℝ), f x = sInf {r : EReal | ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ r = ↑(∑ i : Fin m, lam i * α i)}) {x : Fin n → ℝ} {μ : ℝ} {lam : Fin m → ℝ} (hlin : ∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) (hnorm : ∑ i : Fin m with ↑i < k, lam i = 1) (hnonneg : ∀ (i : Fin m), 0 ≤ lam i) (hobj_lt : ↑(∑ i : Fin m, lam i * α i) < ↑μ) : (x, μ) ∈ epigraph Set.univ f

Helper for Corollary 19.1.2: any feasible Text 19.0.10 coefficients whose objective value is strictly below μ certify epigraph membership at (x, μ).

theorem helperForCorollary_19_1_2_mem_transformedEpigraphImage_iff_mem_epigraph_univ {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ} : (prodLinearEquiv_append_coord n) (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f ↔ (x, μ) ∈ epigraph Set.univ f

Helper for Corollary 19.1.2: membership of (x, μ) in the transformed epigraph image is equivalent to ordinary epigraph membership at (x, μ) via the append-coordinate linear equivalence.

theorem helperForCorollary_19_1_2_mem_epigraph_univ_of_mem_transformedEpigraphImage {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ} (hmem : (prodLinearEquiv_append_coord n) (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f) : (x, μ) ∈ epigraph Set.univ f

Helper for Corollary 19.1.2: transformed-epigraph image membership directly yields ordinary epigraph membership at (x, μ).

theorem helperForCorollary_19_1_2_fx_leEReal_of_mem_transformedEpigraphImage {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ} (hmem : (prodLinearEquiv_append_coord n) (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f) : f x ≤ ↑μ

Helper for Corollary 19.1.2: transformed-epigraph image membership implies the defining epigraph inequality f x ≤ μ after coercion to EReal.

theorem helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_decodedFeasible {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hrepr : ∀ (x : Fin n → ℝ), f x = sInf {r : EReal | ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ r = ↑(∑ i : Fin m, lam i * α i)}) {x : Fin n → ℝ} {μ : ℝ} (hdecode : ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ ↑(∑ i : Fin m, lam i * α i) ≤ ↑μ) : (prodLinearEquiv_append_coord n) (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f

Helper for Corollary 19.1.2: packing coefficient-representation data into finite generation of the transformed epigraph.

theorem helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_directFeasible_le {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hrepr : ∀ (x : Fin n → ℝ), f x = sInf {r : EReal | ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ r = ↑(∑ i : Fin m, lam i * α i)}) {x : Fin n → ℝ} {μ : ℝ} {lam : Fin m → ℝ} (hlin : ∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) (hnorm : ∑ i : Fin m with ↑i < k, lam i = 1) (hnonneg : ∀ (i : Fin m), 0 ≤ lam i) (hobj_le : ↑(∑ i : Fin m, lam i * α i) ≤ ↑μ) : (prodLinearEquiv_append_coord n) (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f

Helper for Corollary 19.1.2: non-strict direct feasible objective data yields membership in the transformed epigraph image.

theorem helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_directFeasible_lt {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hrepr : ∀ (x : Fin n → ℝ), f x = sInf {r : EReal | ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ r = ↑(∑ i : Fin m, lam i * α i)}) {x : Fin n → ℝ} {μ : ℝ} {lam : Fin m → ℝ} (hlin : ∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) (hnorm : ∑ i : Fin m with ↑i < k, lam i = 1) (hnonneg : ∀ (i : Fin m), 0 ≤ lam i) (hobj_lt : ↑(∑ i : Fin m, lam i * α i) < ↑μ) : (prodLinearEquiv_append_coord n) (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f

Helper for Corollary 19.1.2: strict objective feasibility data directly yields membership in the transformed epigraph image.

theorem helperForCorollary_19_1_2_exists_feasibleCoeffs_le_mu_of_strictIneq {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hrepr : ∀ (x : Fin n → ℝ), f x = sInf {r : EReal | ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ r = ↑(∑ i : Fin m, lam i * α i)}) {x : Fin n → ℝ} {μ : ℝ} (hfx_lt : f x < ↑μ) : ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ ↑(∑ i : Fin m, lam i * α i) ≤ ↑μ

Helper for Corollary 19.1.2: strict epigraph inequality gives feasible coefficients with a non-strict objective upper bound.

theorem helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_strictIneq {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hrepr : ∀ (x : Fin n → ℝ), f x = sInf {r : EReal | ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ r = ↑(∑ i : Fin m, lam i * α i)}) {x : Fin n → ℝ} {μ : ℝ} (hfx_lt : f x < ↑μ) : (prodLinearEquiv_append_coord n) (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f

Helper for Corollary 19.1.2: strict epigraph inequality yields transformed-epigraph membership by extracting feasible coefficients and weakening < to ≤.

theorem helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_finitelyGenerated_strictIneq {n : ℕ} {f : (Fin n → ℝ) → EReal} (hfg : IsFinitelyGeneratedConvexFunction n f) {x : Fin n → ℝ} {μ : ℝ} (hfx_lt : f x < ↑μ) : (prodLinearEquiv_append_coord n) (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f

Helper for Corollary 19.1.2: unpacking finite-generation data and applying the strict inequality decode step yields transformed-epigraph membership.

theorem helperForCorollary_19_1_2_objective_dropVertical_le {qCore tVert μ : ℝ} (hdecomp : qCore + tVert ≤ μ) (htVert_nonneg : 0 ≤ tVert) : qCore ≤ μ ∧ ↑qCore ≤ ↑μ

Helper for Corollary 19.1.2: dropping a nonnegative vertical term from an objective decomposition preserves an upper bound, both in ℝ and after coercion to EReal.

theorem helperForCorollary_19_1_2_sum_filter_lt_eq_sum_castAdd {k m : ℕ} (g : Fin (k + m) → ℝ) : ∑ i : Fin (k + m) with ↑i < k, g i = ∑ i : Fin k, g (Fin.castAdd m i)

Helper for Corollary 19.1.2: summing over indices < k in Fin (k + m) is the same as summing over Fin k via Fin.castAdd.

theorem helperForCorollary_19_1_2_sum_filter_lt_eq_sum_leftBlock_cast {k m : ℕ} (hk : k ≤ m) (lam : Fin m → ℝ) : ∑ i : Fin m with ↑i < k, lam i = ∑ i : Fin k, lam (Fin.cast ⋯ (Fin.castAdd (m - k) i))

Helper for Corollary 19.1.2: transport the < k filtered sum on Fin m to the left block of Fin (k + (m - k)) via the canonical cast induced by k ≤ m.

theorem helperForCorollary_19_1_2_sum_filter_not_lt_eq_sum_natAdd {k m : ℕ} (g : Fin (k + m) → ℝ) : ∑ i : Fin (k + m) with ¬↑i < k, g i = ∑ j : Fin m, g (Fin.natAdd k j)

Helper for Corollary 19.1.2: summing over indices not < k in Fin (k + m) is the same as summing over the right block via Fin.natAdd.

theorem helperForCorollary_19_1_2_sum_filter_not_lt_eq_sum_rightBlock_cast {k m : ℕ} (hk : k ≤ m) (lam : Fin m → ℝ) : ∑ i : Fin m with ¬↑i < k, lam i = ∑ j : Fin (m - k), lam (Fin.cast ⋯ (Fin.natAdd k j))

Helper for Corollary 19.1.2: transport the ¬(< k) filtered sum on Fin m to the right block of Fin (k + (m - k)) via the canonical cast induced by k ≤ m.

theorem helperForCorollary_19_1_2_sum_filter_split_eq_pair_leftRight_cast {k m : ℕ} (hk : k ≤ m) (lam : Fin m → ℝ) : ∑ i : Fin m with ↑i < k, lam i = ∑ i : Fin k, lam (Fin.cast ⋯ (Fin.castAdd (m - k) i)) ∧ ∑ i : Fin m with ¬↑i < k, lam i = ∑ j : Fin (m - k), lam (Fin.cast ⋯ (Fin.natAdd k j))

Helper for Corollary 19.1.2: transport both filtered coefficient sums from Fin m to the left and right packed blocks in one statement via the canonical cast from k ≤ m.

theorem helperForCorollary_19_1_2_transport_normalization_to_leftBlock {k m : ℕ} (hk : k ≤ m) {lam : Fin m → ℝ} (hnorm : ∑ i : Fin m with ↑i < k, lam i = 1) : ∑ i : Fin k, lam (Fin.cast ⋯ (Fin.castAdd (m - k) i)) = 1

Helper for Corollary 19.1.2: the Text 19.0.10 normalization constraint transports to the left packed block via the canonical cast induced by k ≤ m.

theorem helperForCorollary_19_1_2_decodeSymmSecondCoord_of_appendPacked {n r : ℕ} (uLeft : Fin 1 → (Fin n → ℝ) × ℝ) (uRight : Fin r → (Fin n → ℝ) × ℝ) : (fun (j : Fin (1 + r)) => ((prodLinearEquiv_append_coord n).symm (Fin.append (fun (i : Fin 1) => (prodLinearEquiv_append_coord n) (uLeft i)) (fun (i : Fin r) => (prodLinearEquiv_append_coord n) (uRight i)) j)).2) = Fin.append (fun (i : Fin 1) => (uLeft i).2) fun (i : Fin r) => (uRight i).2

Helper for Corollary 19.1.2: decoding second coordinates after packing by Fin.append and prodLinearEquiv_append_coord recovers the appended second-coordinate family.

theorem helperForCorollary_19_1_2_splitPackedIndexSums_atVertical {k m : ℕ} (g : Fin (k + (1 + (m - k))) → ℝ) : ∑ i : Fin (k + (1 + (m - k))), g i = ∑ i : Fin k, g (Fin.castAdd (1 + (m - k)) i) + g (Fin.natAdd k (Fin.castAdd (m - k) 0)) + ∑ j : Fin (m - k), g (Fin.natAdd k (Fin.natAdd 1 j))

Helper for Corollary 19.1.2: split a packed-index sum into the left block, the vertical singleton slot, and the right block.

theorem helperForCorollary_19_1_2_packedLinearSum_eq_originalLinearSum {n k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (uLeft : Fin k → Fin n → ℝ) (uRight : Fin (m - k) → Fin n → ℝ) (j0 : Fin n) : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append uLeft (Fin.append (fun (x : Fin 1) => 0) uRight) i j0 = ∑ i : Fin k, aFix i * uLeft i j0 + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * uRight j j0

Helper for Corollary 19.1.2: decoding a packed three-block linear sum (left points, vertical singleton, right directions) recovers the original first-coordinate linear sum, since the vertical block contributes 0.

theorem helperForCorollary_19_1_2_packedObjectiveSum_eq_originalPlusVertical {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i = ∑ i : Fin k, aFix i * αLeft i + bFix (Fin.castAdd (m - k) 0) + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j

Helper for Corollary 19.1.2: decoding a packed three-block objective sum yields the original objective plus the vertical coefficient contribution.

theorem helperForCorollary_19_1_2_packedObjective_eq_iff_originalPlusVertical_eq {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) {μ : ℝ} : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i = μ ↔ ∑ i : Fin k, aFix i * αLeft i + bFix (Fin.castAdd (m - k) 0) + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j = μ

Helper for Corollary 19.1.2: a packed-objective equality is equivalent to equality of the decoded left-plus-vertical-plus-right objective decomposition.

theorem helperForCorollary_19_1_2_originalObjective_le_of_packedObjective_le {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) {μ : ℝ} (hpacked_le : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i ≤ μ) (hvertical_nonneg : 0 ≤ bFix (Fin.castAdd (m - k) 0)) : ∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j ≤ μ ∧ ↑(∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ ↑μ

Helper for Corollary 19.1.2: a packed-objective upper bound and nonnegativity of the vertical singleton coefficient imply the corresponding upper bound for the original objective, both in ℝ and after coercion to EReal.

theorem helperForCorollary_19_1_2_originalObjective_le_pair_of_packedObjective_eq {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) {μ : ℝ} (hpacked_eq : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i = μ) (hvertical_nonneg : 0 ≤ bFix (Fin.castAdd (m - k) 0)) : ∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j ≤ μ ∧ ↑(∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ ↑μ

Helper for Corollary 19.1.2: if the packed objective equals μ and the vertical singleton coefficient is nonnegative, then the decoded original objective is at most μ both in ℝ and, after coercion, in EReal.

theorem helperForCorollary_19_1_2_verticalAndRightBlock_nonneg_of_allPackedNonneg {k m : ℕ} (bFix : Fin (1 + (m - k)) → ℝ) (hpacked_nonneg : ∀ (i : Fin (1 + (m - k))), 0 ≤ bFix i) : 0 ≤ bFix (Fin.castAdd (m - k) 0) ∧ ∀ (j : Fin (m - k)), 0 ≤ bFix (Fin.natAdd 1 j)

Helper for Corollary 19.1.2: nonnegativity of all packed right-block coefficients yields both nonnegativity of the distinguished vertical singleton and nonnegativity of every shifted right-block coefficient.

theorem helperForCorollary_19_1_2_verticalSingleton_nonneg_of_allPackedNonneg {k m : ℕ} (bFix : Fin (1 + (m - k)) → ℝ) (hpacked_nonneg : ∀ (i : Fin (1 + (m - k))), 0 ≤ bFix i) : 0 ≤ bFix (Fin.castAdd (m - k) 0)

Helper for Corollary 19.1.2: if all packed right-block coefficients are nonnegative, then the distinguished vertical singleton coefficient is nonnegative.

theorem helperForCorollary_19_1_2_originalObjective_le_pair_of_packedObjective_eq_of_allPackedNonneg {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) {μ : ℝ} (hpacked_eq : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i = μ) (hpacked_nonneg : ∀ (i : Fin (1 + (m - k))), 0 ≤ bFix i) : ∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j ≤ μ ∧ ↑(∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ ↑μ

Helper for Corollary 19.1.2: a packed objective equality together with nonnegativity of all packed right-block coefficients yields the decoded original-objective bounds in ℝ and EReal.

theorem helperForCorollary_19_1_2_originalObjective_le_of_packedObjective_eq_of_allPackedNonneg {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) {μ : ℝ} (hpacked_eq : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i = μ) (hpacked_nonneg : ∀ (i : Fin (1 + (m - k))), 0 ≤ bFix i) : ∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j ≤ μ

Helper for Corollary 19.1.2: if the packed objective equals μ and all packed right-block coefficients are nonnegative, then the decoded original objective is at most μ in ℝ.

theorem helperForCorollary_19_1_2_originalObjective_leEReal_of_packedObjective_eq_of_allPackedNonneg {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) {μ : ℝ} (hpacked_eq : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i = μ) (hpacked_nonneg : ∀ (i : Fin (1 + (m - k))), 0 ≤ bFix i) : ↑(∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ ↑μ

Helper for Corollary 19.1.2: if the packed objective equals μ and all packed right-block coefficients are nonnegative, then the decoded original objective is at most μ after coercion to EReal.

theorem helperForCorollary_19_1_2_transport_originalCoeffs_of_packedDecode {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) {μ : ℝ} (hpacked_eq : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i = μ) (hvertical_nonneg : 0 ≤ bFix (Fin.castAdd (m - k) 0)) : ∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j ≤ μ ∧ ↑(∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ ↑μ

Helper for Corollary 19.1.2: transporting a packed decoded objective equality and nonnegative vertical singleton coefficient yields the decoded original-objective bound in both ℝ and EReal.

theorem helperForCorollary_19_1_2_transport_originalCoeffs_of_packedDecode_of_allPackedNonneg {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) {μ : ℝ} (hpacked_eq : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i = μ) (hpacked_nonneg : ∀ (i : Fin (1 + (m - k))), 0 ≤ bFix i) : ∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j ≤ μ ∧ ↑(∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ ↑μ

Helper for Corollary 19.1.2: transporting a packed decoded objective equality together with nonnegativity of all packed right-block coefficients yields the decoded original-objective bound in both ℝ and EReal.

theorem helperForCorollary_19_1_2_transport_originalCoeffs_le_of_packedDecode_of_allPackedNonneg {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) {μ : ℝ} (hpacked_eq : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i = μ) (hpacked_nonneg : ∀ (i : Fin (1 + (m - k))), 0 ≤ bFix i) : ∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j ≤ μ

Helper for Corollary 19.1.2: transporting packed decoded objective data together with nonnegativity of all packed right-block coefficients yields the decoded original-objective bound in ℝ.

theorem helperForCorollary_19_1_2_transport_originalCoeffs_leEReal_of_packedDecode_of_allPackedNonneg {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) {μ : ℝ} (hpacked_eq : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i = μ) (hpacked_nonneg : ∀ (i : Fin (1 + (m - k))), 0 ≤ bFix i) : ↑(∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ ↑μ

Helper for Corollary 19.1.2: transporting packed decoded objective data together with nonnegativity of all packed right-block coefficients yields the decoded original-objective bound after coercion to EReal.

theorem helperForCorollary_19_1_2_originalObjective_le_of_packedObjective_eq {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) {μ : ℝ} (hpacked_eq : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i = μ) (hvertical_nonneg : 0 ≤ bFix (Fin.castAdd (m - k) 0)) : ∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j ≤ μ

Helper for Corollary 19.1.2: if the packed objective equals μ and the vertical singleton coefficient is nonnegative, then the decoded original objective is at most μ in ℝ.

theorem helperForCorollary_19_1_2_originalObjective_leEReal_of_packedObjective_eq {k m : ℕ} (aFix : Fin k → ℝ) (bFix : Fin (1 + (m - k)) → ℝ) (αLeft : Fin k → ℝ) (αRight : Fin (m - k) → ℝ) {μ : ℝ} (hpacked_eq : ∑ i : Fin (k + (1 + (m - k))), Fin.append aFix bFix i * Fin.append αLeft (Fin.append (fun (x : Fin 1) => 1) αRight) i = μ) (hvertical_nonneg : 0 ≤ bFix (Fin.castAdd (m - k) 0)) : ↑(∑ i : Fin k, aFix i * αLeft i + ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ ↑μ

Helper for Corollary 19.1.2: if the packed objective equals μ and the vertical singleton coefficient is nonnegative, then the decoded original objective is at most μ after coercion to EReal.