theorem proximal_gradient_convex_objective_gap_le_of_ceiling_iteration_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [ProperSpace E] {f g : E → EReal} {XStar : Set E} {FOpt : ℝ} {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {α : ℝ} {x : ℕ → E} {L : ℕ → ↑PosReal} {xStar : E} (htraj : is_proximal_gradient_trajectory f g x L) (hrule : hproblem.SourceSublinearRateStepsizeRule x L htraj α) (hxStar : xStar ∈ XStar) (ε : ↑PosReal) (R : ℝ) (hR : ‖x 0 - xStar‖ ≤ R) (k : ℕ) (hiter : ⌈α * ↑Lf * R ^ 2 / (2 * ↑ε)⌉₊ ≤ k) : composite_model_objective f g (x k) - ↑FOpt ≤ ↑↑ε

Theorem 10.25: under Assumption 10.1, if f is convex and the proximal-gradient iterates use either the constant rule L_k = L_f or backtracking procedure B2, then any iterate index k ≥ ⌈α L_f R^2 / (2 ε)⌉ satisfies F(x^k) - F_opt ≤ ε, where R bounds the distance from the initial point x^0 to some optimizer xStar ∈ X^*.