theorem
Lemma_13_19_Curvature.polytope_quadratic_boundary_optimizer_ne_vertex
{n l : ℕ}
{Q : ↑(positiveDefiniteMatrices n)}
{b : Fin n → ℝ}
{a : Fin l → Fin n → ℝ}
{x : ℕ → ↑(polytope_quadratic_feasible_set a)}
{v0 : ↑(stdSimplex ℝ (Fin l))}
{xStar : Fin n → ℝ}
(hboundary :
IsBoundaryNonExtremeOptimalSolution (polytope_quadratic_problem (↑Q) b a) ((convexHull ℝ) (Set.range a)) xStar)
(hinit : IsStrictVertexSublevelInitialPoint (polytope_quadratic_objective (↑Q) b) a (↑(x 0)) v0)
(j : Fin l)
:
a j ≠ xStar
Helper for Lemma 13.19: the boundary optimizer xStar cannot coincide with any vertex
a_j, because every vertex lies strictly above the initial objective value while xStar is
optimal on Ω.
theorem
Lemma_13_19_Curvature.exists_pos_vertex_distance_lower_bound_at_boundary_optimizer
{n l : ℕ}
{Q : ↑(positiveDefiniteMatrices n)}
{b : Fin n → ℝ}
{a : Fin l → Fin n → ℝ}
{x : ℕ → ↑(polytope_quadratic_feasible_set a)}
{v0 : ↑(stdSimplex ℝ (Fin l))}
{xStar : Fin n → ℝ}
(hboundary :
IsBoundaryNonExtremeOptimalSolution (polytope_quadratic_problem (↑Q) b a) ((convexHull ℝ) (Set.range a)) xStar)
(hinit : IsStrictVertexSublevelInitialPoint (polytope_quadratic_objective (↑Q) b) a (↑(x 0)) v0)
:
∃ ε > 0, ∀ (j : Fin l), ε ≤ ‖a j - xStar‖
Helper for Lemma 13.19: the boundary optimizer xStar stays a positive distance away from the
finite vertex set {a_j}.
theorem
Lemma_13_19_Curvature.exists_pos_quadratic_form_lower_bound_of_posDef
{n : ℕ}
{Q : ↑(positiveDefiniteMatrices n)}
:
∃ γ > 0, ∀ (d : Fin n → ℝ), γ * ‖d‖ ^ 2 ≤ d ⬝ᵥ (↑Q).mulVec d
Helper for Lemma 13.19: a positive-definite quadratic form dominates the Euclidean square norm by a uniform positive constant.
theorem
Lemma_13_19_Curvature.exists_pos_polytope_quadratic_directional_curvature_lower_bound
{n l : ℕ}
{Q : ↑(positiveDefiniteMatrices n)}
{b : Fin n → ℝ}
{a : Fin l → Fin n → ℝ}
{x : ℕ → ↑(polytope_quadratic_feasible_set a)}
{i : ℕ → Fin l}
{v0 : ↑(stdSimplex ℝ (Fin l))}
{xStar : Fin n → ℝ}
(hboundary :
IsBoundaryNonExtremeOptimalSolution (polytope_quadratic_problem (↑Q) b a) ((convexHull ℝ) (Set.range a)) xStar)
(hinit : IsStrictVertexSublevelInitialPoint (polytope_quadratic_objective (↑Q) b) a (↑(x 0)) v0)
(htraj : is_polytope_quadratic_conditional_gradient_exact_line_search_trajectory Q b a x i)
:
∃ β > 0,
∀ (k : ℕ),
β ≤ polytope_quadratic_conditional_gradient_direction a (↑(x k)) (i k) ⬝ᵥ (↑Q).mulVec (polytope_quadratic_conditional_gradient_direction a (↑(x k)) (i k))
Helper for Lemma 13.19: the directional curvatures ((dᵏ)^T Q dᵏ) are uniformly bounded
below by a positive constant.