Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A frozen Newton step yields a controlled error inequality

Statement

Let 1≤p<∞. Let X,Y,Z be real Banach spaces, let X0 be a closed linear subspace of X, and let D,U⊆X. Let x0,x†∈D∩U∩X0, let F:D→Y, K∈L(Z,Y), and r:D→Z satisfy F(x)−F(x0)=Kr(x) for all x∈D. Assume r∣U:U→U~ is a bijection, r is Lipschitz on D with constant Lr, and r has bounded linear Gâteaux derivatives on U. Let P:X→X be a bounded linear projection with P2=P, P∣X0=0, and (I−P)(X)⊆X0. Assume P(x†)=0 and (I−P)r−1(r^)∈D∩X0 for each admitted r^∈U~.

Let Rˇ:X0→[0,+∞] be proper and convex, choose ξ†∈∂Rˇ(x†), and write

DRˇξ†(z,x†):=Rˇ(z)−Rˇ(x†)−⟨ξ†,z−x†⟩X0∗,X0.

Suppose that, on the stated sublevel Rˇ(z)≤R0, the variational source inequality

−⟨ξ†,z−x†⟩X0∗,X0≤bDRˇξ†(z,x†)+ψ ⁣(∥F(z)−F(x†)∥Yp)

holds for some R0≥Rˇ(x†) and 0≤b<1. Assume that ψ:[0,∞)→[0,∞) is continuous, nondecreasing and concave, with ψ(0)=0, and that for a constant Cψ>0,

ψ(a+b)≤Cψ(ψ(a)+ψ(b))(a,b≥0).

Let H(q):=sup⁡s≥0(ψ(s)−qs), and assume the values of H used below are finite. Let γ>Cψ, CP≥2p−1∥K∥pLrp, and C~Q>0. Let RP:P(X)→[0,+∞] satisfy RP(0)=0 and

RP(z)≥γψ(CP∥z∥Xp)(z∈P(X)).

For each admitted r^∈U~, put u(r^):=r−1(r^) and xˇ(r^):=(I−P)u(r^). Assume the compatibility bound

∥r^−r(x†)∥Zp≤C~Q(DRˇξ†(xˇ(r^),x†)+ψ(CP∥Pu(r^)∥Xp)).

Choose cβα>0 with cβα≤min⁡{1−b,γ−Cψ}/(4C~Q), and set

m:=min⁡{1−b,γ−Cψ},a:=21−p,λ:=21−p,t:=22−2p−2p−1ctcrp,v:=(1+2p−1)ctcrp,C‾:=Cψ22p−2.

Assume 0<ctcr<1 and t>0, and for all x1,x2∈U assume

∥r(x1)−r(x2)−r′(x2)(x1−x2)∥Z≤ctcr∥r(x1)−r(x2)∥Z.

Assume the candidate projected point satisfies Rˇ(xˇ(r^n+1))≤R0.

Let Q(a,b):=∥a−b∥Z. Fix δ>0, yδ∈Y with ∥yδ−F(x†)∥Y≤δ, and αn>0, with βn:=cβααn. Suppose (r^n+1,xn+1)∈U~×U satisfies, for some ηn≥0,

Jnδ(r^n+1,xn+1)≤Jnδ(r^,x)+ηn((r^,x)∈U~×U),

where Jnδ is the frozen objective in the Joint and frozen-Newton objectives definition, with regularizer R(r^)=Rˇ(xˇ(r^))+RP(Pu(r^)) and distance Q.

Define

En+1:=cβαCψ(λ∥r^n+1−r(x†)∥Zp+t∥r(xn+1)−r(x†)∥Zp),

Sn+1:=1Cψ(21−p∥K(r^n+1−r(x†))∥Yp+∥Pxn+1∥Xp),

and

dn:=cβαCψαnv∥r(xn)−r(x†)∥Zp+2δp+ηnCψ.

Then

Sn+1+αnEn+1≤dn+αnψ(C‾Sn+1).

Consequently,

En+1≤dnαn+H ⁣(1C‾αn),Sn+1≤2(dn+αnH ⁣(12C‾αn)).

Facts & Assumptions

Given: All spaces, maps, penalties, parameters, source inequalities, compatibility inequalities, and the approximate frozen step satisfy the hypotheses in the Statement.

[A1]

The projected point xˇ(r^n+1) belongs to the regularizer sublevel where the VSC holds.

[F1]

Differential range invariance for Banach-space maps: F(x)−F(x0)=Kr(x) on the specified domain, and r∣U is invertible onto U~.

[F2]

Joint and frozen-Newton objectives for range-invariant relaxations: the frozen objective has data term ∥Kr^+F(x0)−yδ∥p, regularizer αnR(r^), coupling βn∥ℓn(x)−r^∥p, and penalty ∥Px∥p, where ℓn(x)=r(xn)+r′(xn)(x−xn).

[F3]

Banach-space convex subgradients and dual pairings: ξ†∈∂Rˇ(x†) means Rˇ(z)≥Rˇ(x†)+⟨ξ†,z−x†⟩ for every z∈X0.

[F4]

Bregman distances for convex regularizers: DRˇξ†(z,x†)=Rˇ(z)−Rˇ(x†)−⟨ξ†,z−x†⟩.

[F5]

Variational source conditions on a regularizer sublevel: −⟨ξ†,z−x†⟩≤bDRˇξ†(z,x†)+ψ(∥F(z)−F(x†)∥p) on the stated sublevel.

[F6]

A conjugate bound for residual and Bregman errors: if r+αe≤d+αψ(Cr), then e≤d/α+H(1/(Cα)) and r≤2(d+αH(1/(2Cα))).

Proof

1.1A1F1F2givenalgebra

Write r†:=r(x†), u:=r−1(r^n+1), xˇ:=(I−P)u, and ℓn(x):=r(xn)+r′(xn)(x−xn). Compare the approximate-minimum inequality with (r^,x)=(r†,x†). The competitor has data residual at most δp, penalty RP(0)=0, and Px†=0. If g:=Kr^n+1+F(x0)−yδ, then K(r^n+1−r†)=g+(yδ−y); convexity of s↦sp gives ∥K(r^n+1−r†)∥p≤2p−1(∥g∥p+δp). Thus the comparison gives 21−p∥K(r^n+1−r†)∥p+αn(R(r^n+1)−Rˇ(x†))+βn∥ℓn(xn+1)−r^n+1∥p+∥Pxn+1∥p≤2δp+ηn+βn∥ℓn(x†)−r†∥p. The remainder hypothesis at (x†,xn) and ctcr<1 imply ∥ℓn(x†)−r†∥p≤ctcrp∥r(xn)−r†∥p.

1.2givenalgebra

Let A:=∥r(xn+1)−r^n+1∥, B:=∥ℓn(xn+1)−r^n+1∥, and Dn:=∥r(xn+1)−ℓn(xn+1)∥. The triangle inequality gives A≤B+Dn, hence Bp≥21−pAp−Dnp. Applying the same power inequality to ∥r(xn+1)−r†∥≤A+∥r^n+1−r†∥ gives Ap≥21−p∥r(xn+1)−r†∥p−∥r^n+1−r†∥p. The Taylor hypothesis and another triangle-power estimate give Dnp≤2p−1ctcrp(∥r(xn+1)−r†∥p+∥r(xn)−r†∥p). Therefore ∥ℓn(xn+1)−r^n+1∥p≥t∥r(xn+1)−r†∥p−λ∥r^n+1−r†∥p−2p−1ctcrp∥r(xn)−r†∥p, with t=22−2p−2p−1ctcrp and λ=21−p.

1.3A1F1F4F5givenalgebra

Set z:=Pu. Since ∥r(xˇ)−r(u)∥≤Lr∥z∥, the factorization and power inequality give ∥F(xˇ)−F(x†)∥p≤2p−1∥K(r^n+1−r†)∥p+2p−1∥K∥pLrp∥z∥p. By the VSC [F5], the Bregman identity [F4], the penalty lower bound, and ψ(a+b)≤Cψ(ψ(a)+ψ(b)), we obtain R(r^n+1)−Rˇ(x†)≥m(DRˇξ†(xˇ,x†)+ψ(CP∥z∥p))−Cψψ(2p−1∥K(r^n+1−r†)∥p). Indeed, the VSC yields coefficient 1−b on the Bregman term, and the penalty leaves coefficient γ−Cψ on the penalty-index term; their minimum is m.

2.1step 1.1step 1.2step 1.3A1F1F3F4F5givenalgebra

Substituting steps 1.1–1.3 into the objective comparison and applying the compatibility inequality gives CψSn+1+αnmT+βnt∥r(xn+1)−r†∥p≤βnv∥r(xn)−r†∥p+βnλ∥r^n+1−r†∥p+αnCψψ(2p−1∥K(r^n+1−r†)∥p)+2δp+ηn, where T:=DRˇξ†(xˇ,x†)+ψ(CP∥Pu∥p). By [F3], DRˇξ†(xˇ,x†)≥0, so T≥0. Since ∥r^n+1−r†∥p≤C~QT and βnλC~Q≤αnm/4, the left regularizer term absorbs the displayed compatibility term and a second copy of it, leaving αnmT/2; in particular it bounds another βnλ∥r^n+1−r†∥p. The resulting inequality is CψSn+1+βnλ∥r^n+1−r†∥p+βnt∥r(xn+1)−r†∥p≤βnv∥r(xn)−r†∥p+αnCψψ(2p−1∥K(r^n+1−r†)∥p)+2δp+ηn.

3.1step 2.1F6givenalgebra∎

Divide step 2.1 by Cψ and use βn=cβααn. Since CψSn+1≥21−p∥K(r^n+1−r†)∥p, we have 2p−1∥K(r^n+1−r†)∥p≤Cψ22p−2Sn+1=C‾Sn+1. Monotonicity of ψ gives Sn+1+αnEn+1≤dn+αnψ(C‾Sn+1). Applying [F6] with c1=c2=1, C3=C‾, r=Sn+1, and e=En+1 proves both conjugate bounds.

Depends on

Used by

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources