noncomputable def secondOrderTaylorIncrementAt {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x : E) : E → ℝ

The source-facing quadratic increment of the canonical second-order Taylor model centered at x, obtained by removing the constant term f x.

theorem secondOrderTaylorIncrementAt_apply {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x y : E) : secondOrderTaylorIncrementAt f x y = inner ℝ (gradient f x) (y - x) + 1 / 2 * inner ℝ ((hessian f x) (y - x)) (y - x)

Evaluating secondOrderTaylorIncrementAt f x at y gives the linear term ⟪∇ f(x), y - x⟫ plus the quadratic Hessian term.

noncomputable def contractedCompositeSecondOrderModel {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (problem : CompositeConvexMinimizationProblem E) (x : E) : E → WithTop ℝ

The contracted composite second-order local model at x, written using the source-facing quadratic increment together with the chapter owner _root_.compositeObjective.

theorem contractedCompositeSecondOrderModel_apply {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (problem : CompositeConvexMinimizationProblem E) (x y : E) : contractedCompositeSecondOrderModel problem x y = ↑(inner ℝ (gradient problem.smoothPart x) (y - x) + 1 / 2 * inner ℝ ((hessian problem.smoothPart x) (y - x)) (y - x)) + problem.nonsmoothPart y

Evaluating the contracted composite second-order model recovers the quadratic increment plus the regularizer value.

structure CompositeTrustRegionContractionMethod {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (problem : CompositeConvexMinimizationProblem E) (x0 : ↑problem.feasibleSet) : Type u

Algorithm 6.6: for a composite convex minimization problem problem, a composite trust- region method with contraction consists of a twice continuously differentiable inherited smooth part on the feasible set, an initial feasible point x₀, a contraction sequence τ_t ∈ (0, 1], and a chosen one-step solver sending each feasible current iterate x_t to a successor x_{t+1} that minimizes the contracted quadratic composite subproblem arg min_{y = (1 - τ_t) x_t + τ_t x, x ∈ Q} ⟪∇ f(x_t), y - x_t⟫ + (1 / 2) ⟪∇² f(x_t) (y - x_t), y - x_t⟫ + Ψ(y).

• objective_contDiffOn : ContDiffOn ℝ 2 problem.smoothPart problem.feasibleSet

  The inherited smooth part is twice continuously differentiable on the feasible set.

• stepSize : ℕ → ℝ

  The contraction sequence τ₀, τ₁, τ₂, ....

• stepSize_mem_Ioc (t : ℕ) : self.stepSize t ∈ Set.Ioc 0 1

  Each contraction factor lies in (0, 1].

• nextIterate (t : ℕ) (x : ↑problem.feasibleSet) : E

  The chosen contracted quadratic subproblem solver at time t and feasible current point x_t.

• nextIterate_mem_argmin (t : ℕ) (x : ↑problem.feasibleSet) : self.nextIterate t x ∈ constrainedArgmin (contractedFeasibleSet problem.feasibleSet (↑x) (self.stepSize t)) (contractedCompositeSecondOrderModel problem ↑x)

  The one-step solver returns a minimizer of the contracted quadratic composite model centered at the current feasible iterate.

theorem CompositeTrustRegionContractionMethod.nextIterate_mem_feasibleSet {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {problem : CompositeConvexMinimizationProblem E} {x0 : ↑problem.feasibleSet} (method : CompositeTrustRegionContractionMethod problem x0) (t : ℕ) (x : ↑problem.feasibleSet) : method.nextIterate t x ∈ problem.feasibleSet

Every one-step update chosen by Algorithm 6.6 remains in the inherited feasible set Q.

def CompositeTrustRegionContractionMethod.iterates {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {problem : CompositeConvexMinimizationProblem E} {x0 : ↑problem.feasibleSet} (method : CompositeTrustRegionContractionMethod problem x0) : ℕ → ↑problem.feasibleSet

The iterate sequence starts from x₀ and recursively applies the contracted quadratic subproblem solver at each feasible iterate.

@[implicit_reducible]

instance CompositeTrustRegionContractionMethod.instCoeFunForallNat {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {problem : CompositeConvexMinimizationProblem E} {x0 : ↑problem.feasibleSet} : CoeFun (CompositeTrustRegionContractionMethod problem x0) fun (x : CompositeTrustRegionContractionMethod problem x0) => ℕ → E

A composite trust-region method with contraction can be used as its iterate sequence.

@[simp]

theorem CompositeTrustRegionContractionMethod.x_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {problem : CompositeConvexMinimizationProblem E} {x0 : ↑problem.feasibleSet} (method : CompositeTrustRegionContractionMethod problem x0) : (fun (t : ℕ) => ↑(method.iterates t)) 0 = ↑x0

The zeroth iterate is the prescribed initial point x₀.

@[simp]

theorem CompositeTrustRegionContractionMethod.iterates_succ {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {problem : CompositeConvexMinimizationProblem E} {x0 : ↑problem.feasibleSet} (method : CompositeTrustRegionContractionMethod problem x0) (t : ℕ) : (fun (t : ℕ) => ↑(method.iterates t)) (t + 1) = method.nextIterate t (method.iterates t)

Each successor iterate is obtained by applying the contracted quadratic subproblem solver to the previous feasible iterate.

theorem CompositeTrustRegionContractionMethod.x0_mem {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {problem : CompositeConvexMinimizationProblem E} {x0 : ↑problem.feasibleSet} : ↑x0 ∈ problem.feasibleSet

The prescribed initial point x₀ belongs to the feasible set Q.

theorem CompositeTrustRegionContractionMethod.iterates_succ_mem_argmin {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {problem : CompositeConvexMinimizationProblem E} {x0 : ↑problem.feasibleSet} (method : CompositeTrustRegionContractionMethod problem x0) (t : ℕ) : (fun (t : ℕ) => ↑(method.iterates t)) (t + 1) ∈ constrainedArgmin (contractedFeasibleSet problem.feasibleSet ((fun (t : ℕ) => ↑(method.iterates t)) t) (method.stepSize t)) (contractedCompositeSecondOrderModel problem ((fun (t : ℕ) => ↑(method.iterates t)) t))

Each successor iterate belongs to the argmin set of the contracted quadratic composite subproblem at the previous iterate.

theorem CompositeTrustRegionContractionMethod.iterates_succ_mem_and_isMinOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {problem : CompositeConvexMinimizationProblem E} {x0 : ↑problem.feasibleSet} (method : CompositeTrustRegionContractionMethod problem x0) (t : ℕ) : (fun (t : ℕ) => ↑(method.iterates t)) (t + 1) ∈ contractedFeasibleSet problem.feasibleSet ((fun (t : ℕ) => ↑(method.iterates t)) t) (method.stepSize t) ∧ IsMinOn (contractedCompositeSecondOrderModel problem ((fun (t : ℕ) => ↑(method.iterates t)) t)) (contractedFeasibleSet problem.feasibleSet ((fun (t : ℕ) => ↑(method.iterates t)) t) (method.stepSize t)) ((fun (t : ℕ) => ↑(method.iterates t)) (t + 1))

Each successor iterate belongs to the contracted feasible set and minimizes the quadratic composite local model there.

theorem CompositeTrustRegionContractionMethod.iterates_mem_feasibleSet {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {problem : CompositeConvexMinimizationProblem E} {x0 : ↑problem.feasibleSet} (method : CompositeTrustRegionContractionMethod problem x0) (t : ℕ) : (fun (t : ℕ) => ↑(method.iterates t)) t ∈ problem.feasibleSet

Every iterate produced by Algorithm 6.6 belongs to the inherited feasible set Q.