Helper for Theorem 10.40: the theorem uses the source residual
u_n = t_n z^n - (x* + (t_n - 1) x^n).
Instances For
Helper for Theorem 10.40: the canonical momentum sequence stays above 1.
Helper for Theorem 10.40: the FISTA momentum recursion satisfies
t_(n+1)^2 - t_(n+1) = t_n^2.
Helper for Theorem 10.40: the textbook backtracking constant
α = max {η, s / L_f} is equivalent to the stepsize cap α L_f = max {η L_f, s}.
Helper for Theorem 10.40: on effective_domain g, the composite objective is the finite real
sum f + g.
Helper for Theorem 10.40: every finite objective gap is the cast of its real gap.
Helper for Theorem 10.40: once both composite values are finite, their difference is the
canonical EReal coercion of the real difference of their toReal values.
Helper for Theorem 10.40: every finite objective value is at least the optimal value FOpt.
Helper for Theorem 10.40: every optimizer has finite g-value, hence lies in
effective_domain g.
Helper for Theorem 10.40: every positive MFISTA iterate has finite g-value because its
objective is bounded above by the finite prox-point objective.
Helper for Theorem 10.40: every positive MFISTA objective gap is nonnegative on the real layer.
Helper for Theorem 10.40: the reciprocal of the MFISTA momentum coefficient belongs to
Set.Icc 0 1.
Helper for Theorem 10.40: the source comparison point
(1 / t_(n+1)) • xStar + (1 - 1 / t_(n+1)) • x^(n+1) stays in effective_domain g.
Helper for Theorem 10.40: convexity bounds the objective of the source comparison point by
(1 - 1 / t_(n+1)) v_(n+1) + FOpt on the real layer.
Helper for Theorem 10.40: convexity of the real-valued smooth term makes the local
linearization defect of f.toEReal nonnegative at every base point.
Helper for Theorem 10.40: after dropping the nonnegative convex linearization defect, the fundamental prox-gradient inequality becomes a real inequality on finite endpoints.
Helper for Theorem 10.40: the MFISTA extrapolation formula gives the exact predecessor transport from the pre-step vector to the previous residual.
Helper for Theorem 10.40: the accepted stepsize rule supplies both monotonicity of
L_n and the uniform cap L_n ≤ α L_f.
Helper for Theorem 10.40: the first source energy is bounded by the initial distance to an
optimizer on the exact source surface 2 / L_0.
Helper for Theorem 10.40: the source comparison point at step n + 1 satisfies the exact
current-step objective-gap estimate on the real layer.
Helper for Theorem 10.40: combining the accepted prox-gap with the current-step objective bound yields the exact shared-denominator Lyapunov balance.
Helper for Theorem 10.40: the exact MFISTA Lyapunov energy contracts in one step.
Theorem 10.40: under Assumption 10.31, any MFISTA trajectory whose curvature estimates are
chosen either by the constant rule L_k = L_f with α = 1 or by backtracking procedure B3 with
α = max {η, s / L_f} satisfies the accelerated objective-gap bound
F(x^k) - F_opt ≤ 2 α L_f ‖x^0 - x*‖^2 / (k + 1)^2 for every optimizer x* ∈ X^* and every
k ≥ 1.