The stepsizes (3.6) are positive and strictly decreasing

Proved

ThreeOpSplitting.Accel.stepsizes_decreasing_part1

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

accelerationp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1stepsize

Let $\mu_B \ge 0$ , $\mu_C > 0$ , $\eta \in (0,1)$ and $\gamma_0 > 0$ , and let $(\gamma_k)_{k \ge 0}$ be generated by the stepsize rule (3.6). Then for every $k \ge 0$ , $\gamma_{k+1} > 0$ and

\gamma_k^2 - \gamma_{k+1}^2 = \gamma_k\gamma_{k+1}\big(2\gamma_{k+1}\mu_B + 2\gamma_k\mu_C\eta\big) > 0.

In particular $(\gamma_k)$ is decreasing and $(1/\gamma_k)$ is increasing, which is the monotonicity hypothesis needed to apply the Stolz–Cesàro theorem in the proof of Theorem 3.3.

Formalization Note The paper prints the bracket as $2\gamma_k\mu_B + 2\gamma_{k+1}\mu_C\eta$ , with $\gamma_k$ and $\gamma_{k+1}$ swapped. That version is false in general (for $\mu_B = 0.7$ , $\mu_C = 1.3$ , $\eta = 0.4$ , $\gamma_k = 0.5$ the two sides are $0.1511$ and $0.1616$ ). Multiplying the identity $(1+2\gamma_k\mu_B)/\gamma_k^2 = (1-2\gamma_{k+1}\mu_C\eta)/\gamma_{k+1}^2$ by $\gamma_k^2\gamma_{k+1}^2$ gives the corrected form stated here. The positivity claim and the rest of the proof are unaffected, since $\gamma_k/\gamma_{k+1} \to 1$ .

Preamble

import Mathlib
import Definitions.Def_ThreeOpSplitting_Accel_Stepsizes

open Filter Topology

Formal statement

namespace ThreeOpSplitting.Accel

/-- Proof of Theorem 3.3, Part 1 (p. 845): the stepsizes (3.6) are positive and strictly
decreasing, with `γ_k² - γ_{k+1}² = γ_kγ_{k+1}(2γ_{k+1}μ_B + 2γ_kμ_Cη) > 0` for all `k ≥ 0`.
The page prints the bracket as `2γ_kμ_B + 2γ_{k+1}μ_Cη` (indices swapped), which is false in
general; the identity above is the one that follows from (3.6). -/
theorem stepsizes_decreasing_part1 (μB μC η γ0 : ℝ)
    (hμB : 0 ≤ μB) (hμC : 0 < μC) (hη0 : 0 < η) (hη1 : η < 1) (hγ0 : 0 < γ0) (k : ℕ) :
    0 < stepsPart1 μB μC η γ0 (k + 1) ∧
    stepsPart1 μB μC η γ0 k ^ 2 - stepsPart1 μB μC η γ0 (k + 1) ^ 2
      = stepsPart1 μB μC η γ0 k * stepsPart1 μB μC η γ0 (k + 1)
        * (2 * stepsPart1 μB μC η γ0 (k + 1) * μB + 2 * stepsPart1 μB μC η γ0 k * μC * η) ∧
    0 < stepsPart1 μB μC η γ0 k ^ 2 - stepsPart1 μB μC η γ0 (k + 1) ^ 2 := by sorry

end ThreeOpSplitting.Accel

Source

Davis and Yin, A Three-Operator Splitting Scheme and its Optimization Applications, Set-Valued Var. Anal. 25 (2017), https://doi.org/10.1007/s11228-017-0421-z, p. 845, Section 3.3, proof of Theorem 3.3, Part 1 (unnumbered display)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

The hypotheses and the sequence are the same as in the previous read-back. $\mu_B, \mu_C, \eta, \gamma_0$ are reals with $\mu_B \ge 0$ , $\mu_C > 0$ , $0 < \eta < 1$ and $\gamma_0 > 0$ . The sequence $(\gamma_j)$ starts at $\gamma_0$ and follows

\gamma_{j+1} = \frac{-2\gamma_j^2\mu_C\eta + \sqrt{(2\gamma_j^2\mu_C\eta)^2 + 4(1+2\gamma_j\mu_B)\gamma_j^2}}{2(1+2\gamma_j\mu_B)},

with the square root of a negative number read as $0$ and division by $0$ giving $0$ .

The theorem states that for every $k \in \mathbb{N}$ , including $k = 0$ , all three of the following hold:

$\gamma_{k+1} > 0$ ;
$\gamma_k^2 - \gamma_{k+1}^2 = \gamma_k\gamma_{k+1}\big(2\gamma_{k+1}\mu_B + 2\gamma_k\mu_C\eta\big)$ ;
$\gamma_k^2 - \gamma_{k+1}^2 > 0$ .

Combined with $\gamma_0 > 0$ , these give a strictly positive sequence whose squares, and hence whose terms, strictly decrease. The case $\mu_B = 0$ is allowed; the bracket in item 2 then reduces to $2\gamma_k\mu_C\eta$ . No degenerate zero or empty cases arise beyond this, since all parameters are constrained as stated.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph