TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Residual bounds for exact and approximate-state adjoint hypergradients

Statement

Let $p, d \geq 1$ , let $Θ \subseteq R^{p}$ and $W \subseteq R^{d}$ be open, and let $f : Θ \times W \to R$ be $C^{2}$ and $g : W \times Θ \to R$ be $C^{1}$ , where $C^{1}$ means total differentiability with continuous derivative and $C^{2}$ means the derivative map is $C^{1}$ . Let $w^{*} : P \to W$ be a $C^{1}$ map on an open neighborhood $P$ of $θ_{0}$ , with $w^{*} (θ_{0}) = w_{0}$ and $F (θ, w^{*} (θ)) = 0$ for $F (θ, w) : = \nabla_{w} f (θ, w)$ , and define $J (θ) : = g (w^{*} (θ), θ)$ , $H (θ, w) : = D_{w} F (θ, w)$ , and $B (θ, w) : = D_{θ} F (θ, w)$ . Assume $H (θ_{0}, w_{0})$ is invertible. Write $c (w) : = \partial_{θ} g (w, θ_{0})$ and $d (w) : = \nabla_{w} g (w, θ_{0})$ , and use the induced Euclidean operator norm for matrices. If the adjoint algorithm at $w_{0}$ returns a vector $\tilde{v}$ , define $ρ : = d (w_{0}) - H (θ_{0}, w_{0})^{T} \tilde{v}$ and $\hat{h} : = c (w_{0}) - B (θ_{0}, w_{0})^{T} \tilde{v}$ . Suppose the evaluated Hessian is symmetric and has a valid lower-bound certificate $x^{T} H (θ_{0}, w_{0}) x \geq μ ∥ x ∥_{2}^{2}$ for every $x$ , for some $μ > 0$ . Then

$∥ \hat{h} - \nabla_{θ} J (θ_{0}) ∥_{2} \leq \frac{∥ B (θ_{0}, w^{*} (θ_{0})) ∥ ∥ ρ ∥_{2}}{μ} .$

There is also a separate approximate-state bound under stronger hypotheses. Put $R (w, θ) : = \nabla_{w} f (θ, w)$ and $A (w) : = D_{w} R (w, θ_{0}) = H (θ_{0}, w)$ . Suppose $R$ is $C^{2}$ on an open neighborhood of $(w_{0}, θ_{0})$ . Let $\tilde{w}$ lie in a $C^{1}$ local inverse chart: for $r : = R (\tilde{w}, θ_{0})$ , there is a local inverse $Ψ$ of $w \mapsto R (w, θ_{0})$ with $Ψ (0) = w_{0}$ , defined on a convex open residual neighborhood containing $0$ and $r$ , with $\tilde{w} = Ψ (r)$ and $∥ D Ψ (y) ∥ \leq κ$ along the segment from $0$ to $r$ . Suppose the segment from $w_{0}$ to $\tilde{w}$ lies in a convex state neighborhood where $∥ A (w)^{- 1} ∥ \leq M$ , $∥ B (θ_{0}, w) ∥ \leq B_{0}$ , and $A (w), B (θ_{0}, w)$ are Lipschitz with constants $L_{A}, L_{B}$ . Suppose also that $c, d$ are Lipschitz there with constants $L_{c}, L_{d}$ and $∥ d (w_{0}) ∥_{2} \leq D_{*}$ . If the adjoint algorithm at $\tilde{w}$ returns $\tilde{v}$ , set $ρ : = d (\tilde{w}) - A (\tilde{w})^{T} \tilde{v}$ and $\hat{h} : = c (\tilde{w}) - B (θ_{0}, \tilde{w})^{T} \tilde{v}$ . Assume the certificate $A (\tilde{w}) = A (\tilde{w})^{T}$ and $x^{T} A (\tilde{w}) x \geq μ ∥ x ∥_{2}^{2}$ for all $x$ , with the same $μ > 0$ . Then

$∥ \hat{h} - \nabla_{θ} J (θ_{0}) ∥_{2} \leq κ (L_{c} + D_{*} (M^{2} L_{A} B_{0} + M L_{B}) + M B_{0} L_{d}) ∥ r ∥_{2} + \frac{B_{0}}{μ} ∥ ρ ∥_{2} .$

The first term bounds the implicit formula evaluated at an approximate state; it does not identify that formula with the derivative of a stopped iteration. The second term bounds the separate linear-solve error.

Statement references

Definitions of F, H, B, J, and the hypergradient

The adjoint algorithm and its measured residual

Full-chart state and sensitivity perturbation bound

Derivative of the residual-chart path

Uniform derivative bound along a path controls its endpoint change

Exact local-branch hypergradient

Euclidean Cauchy–Schwarz inequality

Facts & Assumptions

Given: The exact stationary branch, its exact and approximate states, the local inverse chart and Lipschitz bounds, and a solver output vector with the stated actual residual.

[F1]

Smooth bilevel stationary problems and their hypergradients: $R = \nabla_{w} f$ , $A = H = D_{w} R$ , $B = D_{θ} R$ , and $J (θ) = g (w^{*} (θ), θ)$ .

[F2]

Hypergradient of a smooth local stationary branch: at an exact branch state, $\nabla_{θ} J = c - B^{T} H^{- T} d$ .

[F3]

An implicit sensitivity evaluated at an approximate state has a local residual bound: under a common invertible residual chart and the stated inverse and Lipschitz bounds, $∥ S (\tilde{w}) - S (w^{*}) ∥ \leq κ (M^{2} L_{A} B_{0} + M L_{B}) ∥ r ∥_{2}$ , where $S (w) = - A (w)^{- 1} B (w)$ .

[F4]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : the derivative of a composition of finite-dimensional totally differentiable maps is the composition of their derivatives.

[F5]

On a convex open set, a uniform bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ : on a convex open set, a uniform bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ .

[F6]

Adjoint hypergradient with a measured linear-solve residual: for any returned vector $\tilde{v}$ , the algorithm computes the actual residual $ρ = d - H^{T} \tilde{v}$ and estimate $\hat{h} = c - B^{T} \tilde{v}$ .

[F7]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∣ x^{T} y ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ for Euclidean vectors of equal dimension.

Proof

1.1F1F3given

Put $S (w) : = - A (w)^{- 1} B (w)$ on the stated state neighborhood. The chart and Lipschitz hypotheses with [F3] give $∥ S (\tilde{w}) - S (w^{*}) ∥ \leq κ (M^{2} L_{A} B_{0} + M L_{B}) ∥ r ∥_{2}$ .

1.2F4F5given

For the state bound, set $γ (t) : = Ψ (t r)$ for $0 < t < 1$ . By [F4], $γ^{'} (t) = D Ψ (t r) r$ , so $∥ γ^{'} (t) ∥_{2} \leq κ ∥ r ∥_{2}$ . For $0 < ε < 1 / 2$ , apply [F5] to $γ$ on the convex open interval $(ε / 2, 1 - ε / 2)$ at $ε$ and $1 - ε$ ; it gives $∥ Ψ ((1 - ε) r) - Ψ (ε r) ∥_{2} \leq κ (1 - 2 ε) ∥ r ∥_{2}$ . Letting $ε ↓ 0$ and using continuity of $Ψ$ , $Ψ (0) = w^{*}$ and $Ψ (r) = \tilde{w}$ give $∥ \tilde{w} - w^{*} ∥_{2} \leq κ ∥ r ∥_{2}$ .

1.3givenalgebra

The inverse and operator-norm hypotheses give $∥ S (\tilde{w}) ∥ \leq ∥ A (\tilde{w})^{- 1} ∥ ∥ B (\tilde{w}) ∥ \leq M B_{0}$ .

1.4F1F2givenalgebra

Define the implicit formula evaluated at a state by $\overset{ˉ}{h} (w) : = c (w) + S (w)^{T} d (w)$ . By [F1] and [F2], $\overset{ˉ}{h} (w^{*}) = \nabla_{θ} J (θ_{0})$ . Expansion gives $\overset{ˉ}{h} (\tilde{w}) - \overset{ˉ}{h} (w^{*}) = (c (\tilde{w}) - c (w^{*})) + (S (\tilde{w}) - S (w^{*}))^{T} d (w^{*}) + S (\tilde{w})^{T} (d (\tilde{w}) - d (w^{*}))$ .

1.5F6F7givenalgebra

At the evaluated state, write $H = A (\tilde{w})$ and $B = B (θ_{0}, \tilde{w})$ . Let $v_{*} = H^{- T} d (\tilde{w})$ . The residual identity gives $v_{*} - \tilde{v} = H^{- T} ρ$ . For any vector $x$ , the certificate and [F7] imply $μ ∥ x ∥_{2}^{2} \leq x^{T} H x \leq ∥ x ∥_{2} ∥ H x ∥_{2}$ , hence $∥ H^{- 1} ∥ \leq 1 / μ$ ; symmetry gives the same bound for $H^{- T}$ . The Euclidean dual formula and [F7] give $∥ B^{T} y ∥_{2} \leq ∥ B ∥ ∥ y ∥_{2}$ , so $∥ \hat{h} - \overset{ˉ}{h} (\tilde{w}) ∥_{2} = ∥ B^{T} H^{- T} ρ ∥_{2} \leq (B_{0} / μ) ∥ ρ ∥_{2}$ .

1.6F2F6F7givenalgebra

For the exact-state claim, put $H : = H (θ_{0}, w_{0})$ , $B : = B (θ_{0}, w_{0})$ , $c : = c (w_{0})$ , and $d : = d (w_{0})$ , and let $v_{*} : = H^{- T} d$ . Since $w_{0} = w^{*} (θ_{0})$ , [F2] gives $\nabla_{θ} J (θ_{0}) = c - B^{T} v_{*}$ . The residual identity gives $v_{*} - \tilde{v} = H^{- T} ρ$ . For every $x$ , the stated symmetry and lower-bound certificate together with [F7] imply $μ ∥ x ∥_{2}^{2} \leq x^{T} H x \leq ∥ x ∥_{2} ∥ H x ∥_{2}$ , so $∥ H^{- 1} ∥ \leq 1 / μ$ ; symmetry gives $∥ H^{- T} ∥ \leq 1 / μ$ . The Euclidean dual formula and [F7] give $∥ B^{T} y ∥_{2} \leq ∥ B ∥ ∥ y ∥_{2}$ . Therefore $∥ \hat{h} - \nabla_{θ} J (θ_{0}) ∥_{2} = ∥ B^{T} H^{- T} ρ ∥_{2} \leq \frac{∥ B ∥ ∥ ρ ∥_{2}}{μ} = \frac{∥ B (θ_{0}, w^{*} (θ_{0})) ∥ ∥ ρ ∥_{2}}{μ} .$ This proves the exact-state claim using only its stated hypotheses.

2.1F1F2F7step 1.1step 1.3step 1.4givenalgebra

For any matrix $M$ and vector $x$ , the Euclidean dual formula $∥ M^{T} x ∥_{2} = \sup_{∥ y ∥_{2} = 1} ∣ y^{T} M^{T} x ∣$ and [F7] give $∥ M^{T} x ∥_{2} \leq ∥ M ∥ ∥ x ∥_{2}$ . Put $δ : = ∥ \tilde{w} - w^{*} ∥_{2}$ . Apply this norm bound to the three terms in step 1.4. The first and third terms have norms at most $L_{c} δ$ and $M B_{0} L_{d} δ$ , respectively, by the stated Lipschitz bounds and step 1.3. The middle term is at most $κ D_{*} (M^{2} L_{A} B_{0} + M L_{B}) ∥ r ∥_{2}$ by step 1.1 and $∥ d (w^{*}) ∥_{2} \leq D_{*}$ . Therefore $∥ \overset{ˉ}{h} (\tilde{w}) - \nabla_{θ} J (θ_{0}) ∥_{2} \leq (L_{c} + M B_{0} L_{d}) δ + κ D_{*} (M^{2} L_{A} B_{0} + M L_{B}) ∥ r ∥_{2}$ .

3.1step 1.2step 2.1algebra

Substitute the state-residual estimate from step 1.2 into step 2.1. This gives the first term in the asserted approximate-state bound for the implicit formula evaluation.

4.1step 3.1step 1.5givenalgebra∎

Combine the approximate-state formula bound from step 3.1 and the solve-error bound from step 1.5 by the triangle inequality. This gives the approximate-state bound under its separate chart and Lipschitz hypotheses.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

37 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

J. Lebl, Basic Analysis II, §8.5.1, Theorem 8.5.6 and proof (standard reference, not scraped)
MIT OpenCourseWare 18.S096, Matrix Calculus for Machine Learning and Beyond, Lecture 4 Part 2, §6.3.1 (standard reference, not scraped)