def sumCoordinateSeminorm {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type w} [Fintype ι] (p : Seminorm ℝ F) : Seminorm ℝ (ι → F)

Helper for Proposition 7.35: the coordinate-sum seminorm on a finite product is the sum of the pulled-back coordinate seminorms.

theorem sum_coordinate_seminorm_apply {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {ι : Type w} [Fintype ι] (p : Seminorm ℝ F) (z : ι → F) : (sumCoordinateSeminorm p) z = ∑ i : ι, p (z i)

Helper for Proposition 7.35: evaluating the coordinate-sum seminorm gives the sum of the coordinate seminorm values.

theorem sum_coordinate_seminorm_isNorm {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {ι : Type w} [Fintype ι] (p : Seminorm ℝ F) [p.IsNorm] : (sumCoordinateSeminorm p).IsNorm

Helper for Proposition 7.35: if p is a norm, then the coordinate-sum seminorm is again a norm.

theorem seminorm_isNorm_comp_of_injective {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {G : Type u_1} [AddCommGroup G] [Module ℝ G] (q : Seminorm ℝ G) [q.IsNorm] (L : E →ₗ[ℝ] G) (hL : Function.Injective ⇑L) : (q.comp L).IsNorm

Helper for Proposition 7.35: pulling back a norm seminorm along an injective linear map preserves separation.

theorem affineResidualSeminorm_strictlyPositiveOn_univ {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p : Seminorm ℝ F) [p.IsNorm] (A : E →ₗ[ℝ] F) (b : F) : StrictlyPositiveOn Set.univ fun (x : E) => p (A x - b)

If p is a norm, then the affine residual objective x ↦ p (A x - b) is strictly positive on the whole space.

theorem affineResidualSeminormSum_strictlyPositiveOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {ι : Type w} [Fintype ι] (p : Seminorm ℝ F) [p.IsNorm] (A : ι → E →ₗ[ℝ] F) (b : ι → F) : StrictlyPositiveOn Set.univ fun (x : E) => ∑ i : ι, p ((A i) x - b i)

Proposition 7.35 (1): the aggregate objective f₁(x) = ∑ᵢ p (Aᵢ x - bᵢ) is strictly positive on the whole space in the sense of Definition 7.81.

def maxCoordinateSeminorm {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type w} [Fintype ι] (p : Seminorm ℝ F) : Seminorm ℝ (ι → F)

Helper for Proposition 7.35: the coordinate-max seminorm on a finite product is the finite supremum of the pulled-back coordinate seminorms.

theorem max_coordinate_seminorm_apply {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {ι : Type w} [Fintype ι] [Nonempty ι] (p : Seminorm ℝ F) (z : ι → F) : (maxCoordinateSeminorm p) z = maxTypeObjective (fun (i : ι) (w : ι → F) => p (w i)) z

Helper for Proposition 7.35: evaluating the coordinate-max seminorm gives the finite maximum of the coordinate seminorm values.

theorem max_coordinate_seminorm_isNorm {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {ι : Type w} [Fintype ι] [Nonempty ι] (p : Seminorm ℝ F) [p.IsNorm] : (maxCoordinateSeminorm p).IsNorm

Helper for Proposition 7.35: if p is a norm, then the coordinate-max seminorm is again a norm.

theorem affineResidualSeminormMax_strictlyPositiveOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {ι : Type w} [Fintype ι] [Nonempty ι] (p : Seminorm ℝ F) [p.IsNorm] (A : ι → E →ₗ[ℝ] F) (b : ι → F) : StrictlyPositiveOn Set.univ (maxTypeObjective fun (i : ι) (x : E) => p ((A i) x - b i))

Proposition 7.35 (2): the aggregate objective f₂(x) = maxᵢ p (Aᵢ x - bᵢ) is strictly positive on the whole space in the sense of Definition 7.81.