(4.6) — mixed-regularity decrease inequality

Proved

RelaxedPRS.Linear.eq_4_6

by mikedeng1 · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-optimizationlinear-convergencep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1relaxed-peaceman-rachford

Assume the relaxed PRS setting with $0<\lambda_k\le1$ and fixed point $z^*$ . Suppose $f$ is $\mu$ -strongly convex with $\mu>0$ , and $g$ is real valued with a $(1/\beta)$ -Lipschitz gradient for $\beta>0$ . Put $x^*=P_gz^*$ and use the proximal points $x_f^k,x_g^k$ . Then, for every $k\ge0$ ,

4\gamma\lambda_k\mu\|x_f^k-x^*\|^2+4\gamma\lambda_k\beta\|\nabla g(x_g^k)-\nabla g(x^*)\|^2+4\lambda_k(1-\lambda_k)\|x_f^k-x_g^k\|^2\le\|z^k-z^*\|^2-\|z^{k+1}-z^*\|^2.

This is display (4.6), the mixed-regularity decrease bound for the case in which $f$ supplies strong convexity and $g$ supplies smoothness.

Preamble

import Mathlib
import Definitions.Def_RelaxedPRS_Linear_Setting

Formal statement

namespace RelaxedPRS.Linear

/-- (4.6), proof of Theorem 4.3, p. 16: mixed-regularity decrease. -/
theorem eq_4_6 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (f g : H → EReal)
    (hf : ThreeOpSplitting.ConvexRates.IsProperClosedConvex f)
    (hg : ThreeOpSplitting.ConvexRates.IsProperClosedConvex g)
    (γ : ℝ) (hγ : 0 < γ) (Pf Pg : H → H)
    (hPf : ThreeOpSplitting.ConvexRates.IsProx γ f Pf)
    (hPg : ThreeOpSplitting.ConvexRates.IsProx γ g Pg)
    (lam : ℕ → ℝ) (hlam : ∀ k, 0 < lam k ∧ lam k ≤ 1)
    (z : ℕ → H) (hz : RelaxedPRS.StrongCvx.IsPRSRun Pf Pg lam z)
    (zs : H) (hzs : RelaxedPRS.StrongCvx.TPRS Pf Pg zs = zs)
    (μ β : ℝ) (hμ : 0 < μ) (hβ : 0 < β)
    (hsc : RelaxedPRS.StrongCvx.IsStrongCvxE μ f)
    (h : H → ℝ) (hgh : ∀ x, g x = (h x : EReal))
    (hh : ThreeOpSplitting.ConvexRates.IsSmoothConvex β h) :
    ∀ k, 4 * γ * lam k * μ * ‖RelaxedPRS.StrongCvx.xf Pf Pg (z k) - RelaxedPRS.StrongCvx.xg Pg zs‖ ^ 2 +
      4 * γ * lam k * β * ‖gradient h (RelaxedPRS.StrongCvx.xg Pg (z k)) - gradient h (RelaxedPRS.StrongCvx.xg Pg zs)‖ ^ 2 +
      4 * lam k * (1 - lam k) * ‖RelaxedPRS.StrongCvx.xf Pf Pg (z k) - RelaxedPRS.StrongCvx.xg Pg (z k)‖ ^ 2 ≤
      ‖z k - zs‖ ^ 2 - ‖z (k + 1) - zs‖ ^ 2 := by sorry
end RelaxedPRS.Linear

Source

Davis & Yin, Faster convergence rates of relaxed Peaceman-Rachford and ADMM under regularity assumptions, arXiv:1407.5210v3, p. 16, proof of Theorem 4.3, (4.6)

Human review

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

View graph