theorem convex_halfspace_inner_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : E) (β : ℝ) : Convex ℝ {x : E | inner ℝ a x ≤ β}

Exmaple 2.18.1 (1): a half-space cut out by one affine linear inequality is convex on any real inner-product space. The textbook ℝ^n statement is the specialization E = EuclideanSpace ℝ (Fin n).

theorem convex_innerLePolyhedron {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {m : ℕ} (a : Fin m → E) (b : Fin m → ℝ) : Convex ℝ (innerLePolyhedron a b)

Helper for Exmaple 2.18.1: part (2) shows that the region cut out by finitely many affine inequalities is convex. The project's owner declaration for this region is innerLePolyhedron a b. The textbook ℝ^n statement is the specialization E = EuclideanSpace ℝ (Fin n).

theorem convex_euclidean_posSemidef_quadratic_sublevelSet {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosSemidef) (r : ℝ) : Convex ℝ {x : EuclideanSpace ℝ (Fin n) | inner ℝ ((Matrix.toEuclideanLin A) x) x ≤ r ^ 2}

Helper for Exmaple 2.18.1: part (3) states that the sublevel set of a positive-semidefinite quadratic form on ℝ^n is convex.