Prove2Me

Proposition 4: Gk(q)G_k(q) is bounded above for q∈dom Φq \in \mathrm{dom}\,\Phi (under Hypothesis H)

Proved
InertialFB.IFB.proposition4_G_bdd_above

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

convex-optimizationforward-backwardinertial-methodsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let HH be a real Hilbert space, let Hypothesis H hold, and let (uk,yk)(u_k, y_k) be generated by (IFB). For each q∈dom⁡Φq \in \operatorname{dom}\Phi (that is, Φ(q)<+∞\Phi(q) < +\infty), the sequence

Gk(q)=⟨zk,uk−q⟩−∑i=2k⟨zi,ξi⟩,k≥2,G_k(q) = \langle z_k, u_k - q\rangle - \sum_{i=2}^{k}\langle z_i, \xi_i\rangle, \qquad k \ge 2,

is bounded from above: there is M∈RM \in \mathbb R with Gk(q)≤MG_k(q) \le M for all k≥2k \ge 2.

Together with Proposition 2, this bound gives the lower estimate (28) on Fk(q)F_k(q) used for the minimization and boundedness results.

Formalization Note The paper states Proposition 4 under HΦH_\Phi and HΨH_\Psi only. Its proof ends by invoking Proposition 2, which needs all of Hypothesis H, and without HλH_\lambda the printed statement fails (e.g. H=RH = \mathbb R, Φ=x2/2\Phi = x^2/2, Ψ=3x2/2\Psi = 3x^2/2, a=2a = 2, b=0.02b = 0.02, λ=10>Λ\lambda = 10 > \Lambda, u0=1u_0 = 1, y0=0y_0 = 0, q=0q = 0, where Gk(0)G_k(0) grows geometrically). This item is therefore stated under the full Hypothesis H, which is a deviation from the printed hypotheses.

Preamble
import Mathlib
import Definitions.Def_InertialFB_IFB_ConvexAnalysis
import Definitions.Def_InertialFB_IFB_Algorithm
import Definitions.Def_InertialFB_IFB_Lyapunov

open Filter Topology
Formal statement
namespace InertialFB.IFB

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]

/-- **Proposition 4** (Attouch–Peypouquet–Redont, p. 8), stated under the full Hypothesis H
(the printed hypotheses are `H_Φ` and `H_Ψ` only, but the proof uses Proposition 2, which
needs all of H, and the printed version admits counterexamples): for each `q ∈ dom Φ`, the
sequence `(G_k(q))_{k ≥ 2}` is bounded from above. -/
theorem proposition4_G_bdd_above (Φ : H → EReal) (Ψ : H → ℝ) (L a b lam : ℝ)
    (hH : HypothesisH Φ Ψ L a b lam) (u y : ℕ → H) (hIFB : IsIFBSeq Φ Ψ a b lam u y) :
    ∀ q : H, Φ q ≠ ⊤ → ∃ M : ℝ, ∀ k : ℕ, 2 ≤ k → auxG a b lam u y k q ≤ M := by sorry

end InertialFB.IFB
Source
Attouch, Peypouquet & Redont, A Dynamical Approach to an Inertial Forward-Backward Algorithm for Convex Minimization, authors' manuscript (Aug 2013) of SIAM J. Optim. (2014), DOI 10.1137/130910294, p. 8, Proposition 4 (stated under the full Hypothesis H; see Formalization Note)
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