structure KelleyMethod {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (problem : SetConstrainedMinimizationProblem E) : Type u

Algorithm 3.9: for a constrained problem min_{x ∈ Q} f(x), Kelley's method is given by an initial feasible point x₀, a sampled subgradient sequence g_k ∈ ∂f(x_k), and an iterate sequence whose successor x_{k+1} minimizes the canonical Kelley model \hat f_k(X; ·) = nonsmoothModel f x g k over the feasible set Q.

• iterates : ℕ → E

  The iterate sequence x₀, x₁, x₂, ....

• subgradient : ℕ → E

  The chosen sampled vector g_k.

• x0_mem : self.iterates 0 ∈ problem.feasibleSet

  The initialization chooses a feasible point x₀ ∈ Q.

• subgradient_spec (k : ℕ) : IsSubgradientAt (fun (x : E) => ↑(problem.objective x)) (self.iterates k) (self.subgradient k)

  Each sampled vector is a genuine subgradient of the owner objective at the current iterate.

• nextIterate_mem_argmin (k : ℕ) : self.iterates (k + 1) ∈ constrainedArgmin problem.feasibleSet (nonsmoothModel problem.objective self.iterates self.subgradient k)

  Each new iterate x_{k+1} belongs to the argmin set of the current Kelley model on Q.

@[implicit_reducible]

instance KelleyMethod.instCoeFunForallNat {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {problem : SetConstrainedMinimizationProblem E} : CoeFun (KelleyMethod problem) fun (x : KelleyMethod problem) => ℕ → E

A Kelley method can be used as its underlying iterate sequence.

theorem KelleyMethod.subgradient_isSubgradientAt {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {problem : SetConstrainedMinimizationProblem E} (method : KelleyMethod problem) (k : ℕ) : IsSubgradientAt (fun (x : E) => ↑(problem.objective x)) (method.iterates k) (method.subgradient k)

The sampled vector at stage k is a genuine subgradient of the owner objective at x_k.

theorem KelleyMethod.subgradient_mem_subdifferential {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {problem : SetConstrainedMinimizationProblem E} (method : KelleyMethod problem) (k : ℕ) : method.subgradient k ∈ subdifferential (fun (x : E) => ↑(problem.objective x)) (method.iterates k)

The sampled vector at stage k belongs to the owner subdifferential at x_k.

theorem KelleyMethod.iterates_succ_mem_argmin {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {problem : SetConstrainedMinimizationProblem E} (method : KelleyMethod problem) (k : ℕ) : method.iterates (k + 1) ∈ constrainedArgmin problem.feasibleSet (nonsmoothModel problem.objective method.iterates method.subgradient k)

Each successor iterate belongs to the argmin set of the current Kelley model on Q.

theorem KelleyMethod.iterates_succ_mem_and_isMinOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {problem : SetConstrainedMinimizationProblem E} (method : KelleyMethod problem) (k : ℕ) : method.iterates (k + 1) ∈ problem.feasibleSet ∧ IsMinOn (nonsmoothModel problem.objective method.iterates method.subgradient k) problem.feasibleSet (method.iterates (k + 1))

Each successor iterate is feasible and minimizes the current Kelley model over the feasible set.

theorem KelleyMethod.iterates_mem {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {problem : SetConstrainedMinimizationProblem E} (method : KelleyMethod problem) (k : ℕ) : method.iterates k ∈ problem.feasibleSet

Every iterate produced by a Kelley method lies in the feasible set.