class is_generalized_conditional_gradient_trajectory {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (g : E → EReal) (x p : ℕ → E) (t : ℕ → ↑(Set.Icc 0 1)) : Prop

Algorithm 13.2: a triple of sequences (xᵏ, pᵏ, tₖ) follows the generalized conditional gradient method for the composite objective f + g when x⁰ ∈ dom(g), each pᵏ ∈ argmin_p {⟪p, ∇ f(xᵏ)⟫ + g(p)}, each tₖ ∈ [0, 1], and xᵏ⁺¹ = xᵏ + tₖ (pᵏ - xᵏ). The primitive trajectory data are the initial-domain condition, the chosen argmin point at each step, and the affine update equality; the paired step statement is derived API.

• zero_mem_effective_domain : x 0 ∈ effective_domain g

  The initial iterate lies in dom(g).

• argmin_mem (k : ℕ) : p k ∈ generalized_conditional_gradient_argmin f g (x k)

  At each iteration, the chosen search point solves the canonical Chapter 13 linearized subproblem.

• step_eq (k : ℕ) : x (k + 1) = x k + ↑(t k) • (p k - x k)

  At each iteration, the next iterate is obtained by the convex-combination update along the chosen search point.

theorem is_generalized_conditional_gradient_trajectory_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → EReal} {x p : ℕ → E} {t : ℕ → ↑(Set.Icc 0 1)} (h : is_generalized_conditional_gradient_trajectory f g x p t) : x 0 ∈ effective_domain g

A generalized conditional-gradient trajectory starts from a point of dom(g).

theorem is_generalized_conditional_gradient_trajectory_argmin {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → EReal} {x p : ℕ → E} {t : ℕ → ↑(Set.Icc 0 1)} (h : is_generalized_conditional_gradient_trajectory f g x p t) (k : ℕ) : p k ∈ generalized_conditional_gradient_argmin f g (x k)

At each iteration k, a generalized conditional-gradient trajectory chooses a minimizer pᵏ of the canonical linearized subproblem at xᵏ.

theorem is_generalized_conditional_gradient_trajectory_step {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → EReal} {x p : ℕ → E} {t : ℕ → ↑(Set.Icc 0 1)} (h : is_generalized_conditional_gradient_trajectory f g x p t) (k : ℕ) : p k ∈ generalized_conditional_gradient_argmin f g (x k) ∧ x (k + 1) = x k + ↑(t k) • (p k - x k)

At each iteration k, a generalized conditional-gradient trajectory chooses a minimizer pᵏ of the linearized subproblem at xᵏ and updates by xᵏ⁺¹ = xᵏ + tₖ (pᵏ - xᵏ), with tₖ ∈ [0, 1] encoded by the type of t k.