theorem whole_space_phi_star_lower_bound_intermediate {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x0 : E) (μ : ℝ) (L : NNRealˣ) (gamma0 : ℝ) (y : ℕ → E) (α : ℕ → ℝ) (k : ℕ) (xk : E) (halpha_k : α k ≤ 1) (htransportCoeff : 0 ≤ α k * (1 - α k) * estimatingSequenceCurvature μ gamma0 α k / estimatingSequenceCurvature μ gamma0 α (k + 1)) (hμ : 0 ≤ μ) (hphi_k : f xk ≤ simpleSetEstimatingValue Set.univ ⋯ ⋯ ⋯ f x0 μ L gamma0 y α k) : simpleSetEstimatingValue Set.univ ⋯ ⋯ ⋯ f x0 μ L gamma0 y α (k + 1) ≥ (1 - α k) * f xk + α k * f (gradientStep f (y k) L) + (α k / (2 * ↑↑L) - α k ^ 2 / (2 * estimatingSequenceCurvature μ gamma0 α (k + 1))) * ‖gradient f (y k)‖ ^ 2 + α k * (1 - α k) * estimatingSequenceCurvature μ gamma0 α k / estimatingSequenceCurvature μ gamma0 α (k + 1) * inner ℝ (gradient f (y k)) (simpleSetEstimatingCenter Set.univ ⋯ ⋯ ⋯ f x0 μ L gamma0 y α k - y k)

The intermediate whole-space lower bound obtained from the strong-convexity owner recursion by specializing to Q = Set.univ and dropping the nonnegative transport strong-convexity term.

theorem strong_objective_correction_nonneg {E : Type u} [NormedAddCommGroup E] (μ : ℝ) (y : ℕ → E) (k : ℕ) (xk : E) (hμ : 0 ≤ μ) : 0 ≤ μ / 2 * ‖xk - y k‖ ^ 2

Helper for Remark 2.20.1: the strong-convexity correction in (2.3.8) is nonnegative when μ ≥ 0.

theorem strong_objective_lower_implies_objective_lower {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (μ : ℝ) (L : NNRealˣ) (y : ℕ → E) (k : ℕ) (xk : E) (hμ : 0 ≤ μ) (hobjective_lower : f xk ≥ f (gradientStep f (y k) L) + inner ℝ (gradient f (y k)) (xk - y k) + 1 / (2 * ↑↑L) * ‖gradient f (y k)‖ ^ 2 + μ / 2 * ‖xk - y k‖ ^ 2) : f xk ≥ f (gradientStep f (y k) L) + inner ℝ (gradient f (y k)) (xk - y k) + 1 / (2 * ↑↑L) * ‖gradient f (y k)‖ ^ 2

Helper for Remark 2.20.1: the strong lower model (2.3.8) implies the μ-free lower model used by the owner estimate-sequence theorem.

theorem whole_space_phi_star_lower_bound_of_strong_objective_lower_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x0 : E) (μ : ℝ) (L : NNRealˣ) (gamma0 : ℝ) (y : ℕ → E) (α : ℕ → ℝ) (k : ℕ) (xk : E) (halpha_k : α k ≤ 1) (htransportCoeff : 0 ≤ α k * (1 - α k) * estimatingSequenceCurvature μ gamma0 α k / estimatingSequenceCurvature μ gamma0 α (k + 1)) (hμ : 0 ≤ μ) (hphi_k : f xk ≤ simpleSetEstimatingValue Set.univ ⋯ ⋯ ⋯ f x0 μ L gamma0 y α k) (hobjective_lower : f xk ≥ f (gradientStep f (y k) L) + inner ℝ (gradient f (y k)) (xk - y k) + 1 / (2 * ↑↑L) * ‖gradient f (y k)‖ ^ 2 + μ / 2 * ‖xk - y k‖ ^ 2) : simpleSetEstimatingValue Set.univ ⋯ ⋯ ⋯ f x0 μ L gamma0 y α (k + 1) ≥ f (gradientStep f (y k) L) + (1 / (2 * ↑↑L) - α k ^ 2 / (2 * estimatingSequenceCurvature μ gamma0 α (k + 1))) * ‖gradient f (y k)‖ ^ 2 + (1 - α k) * inner ℝ (gradient f (y k)) ((α k * estimatingSequenceCurvature μ gamma0 α k / estimatingSequenceCurvature μ gamma0 α (k + 1)) • (simpleSetEstimatingCenter Set.univ ⋯ ⋯ ⋯ f x0 μ L gamma0 y α k - y k) + (xk - y k))

Remark 2.20.1: if φ_k^* ≥ f(x_k) and the whole-space lower model (2.3.8) holds at y_k, then the next estimate-sequence value satisfies the textbook whole-space lower bound (2.3.10).