theorem OptimalMethodRecurrence.estimatingWeight_eq_weight {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : ℝ} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : OptimalMethodRecurrence f L 0 x0 gamma0) (k : ℕ) : estimatingWeight method.alpha k = method.weight k

Helper for Theorem 2.22: the scalar recurrence estimatingWeight method.alpha is exactly the owner weight sequence method.weight.

theorem OptimalMethodRecurrence.weight_le_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : ℝ} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : OptimalMethodRecurrence f L 0 x0 gamma0) (k : ℕ) : method.weight k ≤ 1

Helper for Theorem 2.22: every owner weight stays at most 1.

theorem OptimalMethodRecurrence.weight_lt_one_of_one_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : ℝ} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : OptimalMethodRecurrence f L 0 x0 gamma0) {k : ℕ} (hk : 1 ≤ k) : method.weight k < 1

Helper for Theorem 2.22: every positive-stage owner weight is strictly below 1.

noncomputable def OptimalMethodRecurrence.gradientAverage {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : ℝ} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : OptimalMethodRecurrence f L 0 x0 gamma0) : ℕ → E

The weighted gradient average gₖ from Theorem 2.22. For k ≥ 1 this is the textbook weighted finite sum, while g₀ is fixed to 0 explicitly so the owner remains total without using division-by-zero conventions. The exported source-facing notation is g_[method; k].

def OptimalMethodRecurrence.OptimalMethodGradientAverage.«termG_[_;_]» : Lean.ParserDescr

@[simp]

theorem OptimalMethodRecurrence.gradientAverage_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : ℝ} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : OptimalMethodRecurrence f L 0 x0 gamma0) : method.gradientAverage 0 = 0

@[simp]

theorem OptimalMethodRecurrence.gradientAverage_succ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : ℝ} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : OptimalMethodRecurrence f L 0 x0 gamma0) (k : ℕ) : method.gradientAverage (k + 1) = method.weightedAverage (fun (i : ℕ) => gradient f (method.y i)) (k + 1)

theorem OptimalMethodRecurrence.v_succ_eq_sub_weighted_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : ℝ} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : OptimalMethodRecurrence f L 0 x0 gamma0) (k : ℕ) : method.v (k + 1) = method.v k - (method.alpha k / method.gamma (k + 1)) • gradient f (method.y k)

Helper for Theorem 2.22: in the smooth-convex specialization μ = 0, the owner center update has the source form v_{k+1} = v_k - (α_k / γ_{k+1}) ∇ f(y_k).

theorem OptimalMethodRecurrence.weighted_gradient_sum_eq_initial_curvature_sub_center {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : ℝ} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : OptimalMethodRecurrence f L 0 x0 gamma0) (k : ℕ) : ∑ i ∈ Finset.range k, (method.alpha i / method.weight (i + 1)) • gradient f (method.y i) = gamma0 • (method.x 0 - method.v k)

Helper for Theorem 2.22: the weighted gradient sum is the initial-curvature multiple of the center displacement x₀ - vₖ.

theorem OptimalMethodRecurrence.gradientAverage_normalization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : ℝ} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : OptimalMethodRecurrence f L 0 x0 gamma0) (k : ℕ) : ∑ i ∈ Finset.range k, method.alpha i / method.weight (i + 1) = (1 - method.weight k) / method.weight k

The coefficients in the source formula for gₖ normalize to the textbook scalar (1 - λₖ) / λₖ.

theorem OptimalMethodRecurrence.gradientAverage_eq_weight_mul_initial_curvature {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : ℝ} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : OptimalMethodRecurrence f L 0 x0 gamma0) (k : ℕ) (hk : 1 ≤ k) : method.gradientAverage k = (method.weight k * gamma0 / (1 - method.weight k)) • (method.x 0 - method.v k)

In the smooth-convex specialization μ = 0, the source-defined gradient average can equally be written using the owner center vₖ and weight λₖ for every positive stage k.

theorem GeneralOptimalMethodScheme.estimating_curvature_eq_method_gamma {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : GeneralOptimalMethodScheme f (↑L) 0 x0 gamma0) (k : ℕ) : estimatingSequenceCurvature 0 gamma0 method.alpha k = method.gamma k

Helper for Theorem 2.22: the source curvature sequence γ_k coincides with the owner curvature sequence of the optimal-method scheme.

theorem GeneralOptimalMethodScheme.estimating_center_eq_method_v {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : GeneralOptimalMethodScheme f (↑L) 0 x0 gamma0) (k : ℕ) : estimatingSequenceCenter f method.alpha method.y 0 gamma0 (method.x 0) k = method.v k

Helper for Theorem 2.22: the source center recursion v_k coincides with the owner center sequence of the optimal-method scheme.

theorem GeneralOptimalMethodScheme.y_eq_alpha_smul_v_add_one_sub_smul_x {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : GeneralOptimalMethodScheme f (↑L) 0 x0 gamma0) (k : ℕ) : method.y k = method.alpha k • method.v k + (1 - method.alpha k) • method.x k

Helper for Theorem 2.22: the owner interpolation point satisfies the source identity y_k = α_k v_k + (1 - α_k) x_k in the smooth-convex case μ = 0.

theorem GeneralOptimalMethodScheme.estimating_value_succ_eq_descent_form {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {f : E → ℝ} {x0 : E} {gamma0 : ℝ} (method : GeneralOptimalMethodScheme f (↑L) 0 x0 gamma0) (k : ℕ) : estimatingSequenceValue f method.alpha method.y 0 (f (method.x 0)) gamma0 (method.x 0) (k + 1) = (1 - method.alpha k) * estimatingSequenceValue f method.alpha method.y 0 (f (method.x 0)) gamma0 (method.x 0) k + method.alpha k * f (method.y k) - 1 / (2 * ↑L) * ‖gradient f (method.y k)‖ ^ 2 + method.alpha k * inner ℝ (gradient f (method.y k)) (method.v k - method.y k)

Helper for Theorem 2.22: the successor formula for φ_k^* simplifies to the exact smooth-convex descent form used in the source induction.

theorem GeneralOptimalMethodScheme.estimating_value_ge_objective {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {f : E → ℝ} (hconv : ConvexOn ℝ Set.univ f) (hgrad : ∀ (x : E), HasGradientAt f (gradient f x) x) {x0 : E} {gamma0 : ℝ} (method : GeneralOptimalMethodScheme f (↑L) 0 x0 gamma0) (k : ℕ) : f (method.x k) ≤ estimatingSequenceValue f method.alpha method.y 0 (f (method.x 0)) gamma0 (method.x 0) k

Helper for Theorem 2.22: the source minimum values dominate the actual objective values along the optimal-method trajectory.

theorem GeneralOptimalMethodScheme.contDiff_one_of_hasGradientAt_lipschitz {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {f : E → ℝ} (hgrad : ∀ (x : E), HasGradientAt f (gradient f x) x) (hgrad_lipschitz : LipschitzWith L (gradient f)) : ContDiff ℝ 1 f

Helper for Theorem 2.22: the smoothness assumptions imply C¹ regularity.

theorem GeneralOptimalMethodScheme.smooth_gap_le_initial_distance_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {f : E → ℝ} (hgrad : ∀ (x : E), HasGradientAt f (gradient f x) x) (hgrad_lipschitz : LipschitzWith L (gradient f)) (xStar : E) (hxStar : IsMinOn f Set.univ xStar) {x0 : E} {gamma0 : ℝ} (method : GeneralOptimalMethodScheme f (↑L) 0 x0 gamma0) : f (method.x 0) - f xStar ≤ ↑L / 2 * ‖xStar - method.x 0‖ ^ 2

Helper for Theorem 2.22: the initial objective gap is bounded by the smooth quadratic upper model at a minimizer.

theorem GeneralOptimalMethodScheme.center_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {f : E → ℝ} (hconv : ConvexOn ℝ Set.univ f) (hgrad : ∀ (x : E), HasGradientAt f (gradient f x) x) (hgrad_lipschitz : LipschitzWith L (gradient f)) (xStar : E) (hxStar : IsMinOn f Set.univ xStar) {x0 : E} {gamma0 : ℝ} (method : GeneralOptimalMethodScheme f (↑L) 0 x0 gamma0) (k : ℕ) : ‖method.v k - xStar‖ ≤ √(1 + ↑L / gamma0) * ‖xStar - method.x 0‖

Theorem 2.22 (1): for the smooth convex optimal-method scheme, every estimating-sequence center vₖ stays within sqrt (1 + L / γ₀) ‖x* - x₀‖ of a minimizer x*, written on the owner surface as ‖xStar - method 0‖.

theorem GeneralOptimalMethodScheme.gradientAverage_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {f : E → ℝ} (hconv : ConvexOn ℝ Set.univ f) (hgrad : ∀ (x : E), HasGradientAt f (gradient f x) x) (hgrad_lipschitz : LipschitzWith L (gradient f)) (xStar : E) (hxStar : IsMinOn f Set.univ xStar) {x0 : E} {gamma0 : ℝ} (method : GeneralOptimalMethodScheme f (↑L) 0 x0 gamma0) (k : ℕ) (hk : 1 ≤ k) : ‖method.gradientAverage k‖ ≤ method.weight k * gamma0 / (1 - method.weight k) * (1 + √(1 + ↑L / gamma0)) * ‖xStar - method.x 0‖

Theorem 2.22 (2): for every positive stage k, the weighted gradient average gₖ satisfies the displayed norm bound in terms of λₖ, γ₀, and the initial distance to a minimizer.

theorem GeneralOptimalMethodScheme.sqrt_factor_eq_three_plus_two_sqrt_three {L : NNReal} : 3 * ↑L * (1 + √(1 + ↑L / (3 * ↑L))) = (3 + 2 * √3) * ↑L

Helper for Theorem 2.22: the smooth-convex square-root factor simplifies to (3 + 2 √3) / 3 when γ₀ = 3L.

theorem GeneralOptimalMethodScheme.gradientAverage_norm_le_of_gamma0_eq_three_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {f : E → ℝ} (hconv : ConvexOn ℝ Set.univ f) (hgrad : ∀ (x : E), HasGradientAt f (gradient f x) x) (hgrad_lipschitz : LipschitzWith L (gradient f)) (xStar : E) (hxStar : IsMinOn f Set.univ xStar) {x0 : E} (method : GeneralOptimalMethodScheme f (↑L) 0 x0 (3 * ↑L)) (k : ℕ) (hk : 1 ≤ k) : ‖method.gradientAverage k‖ ≤ 4 * (3 + 2 * √3) * ↑L * ‖xStar - method.x 0‖ / (3 * (↑k + 1) ^ 2 - 4)

Theorem 2.22 (3): when γ₀ = 3L, the weighted gradient average gₖ satisfies the explicit O((k + 1)⁻²) norm bound from the textbook.