TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck pass

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.

Finite fixed-point iteration sensitivity error bounds and the limits of residual control

Statement

Let $p, m \geq 0$ , let $Θ \subseteq R^{p}$ be open with $θ_{0} \in Θ$ , and let $G : U \to R^{m}$ be $C^{2}$ on an open neighborhood $U \subseteq R^{m} \times Θ$ of $D \times {θ_{0}}$ . Suppose $D \subseteq R^{m}$ is an open convex neighborhood of $z_{*}$ and $z_{*} = G (z_{*}, θ_{0})$ . Assume $G (D, θ_{0}) \subseteq D$ , $∥ G_{z} (z, θ_{0}) ∥ \leq q < 1$ on $D$ , and $G_{z}, G_{θ}$ are Lipschitz in $z$ with constants $L_{z}, L_{θ}$ . Let $z_{0} : Θ \to R^{m}$ be $C^{1}$ , with the iterates at $θ_{0}$ lying in $D$ . Write $s_{*} = D ϕ (θ_{0})$ for the local exact fixed-point branch (supplied by the implicit function theorem when $p, m \geq 1$ ), $e_{k} = D_{θ} z_{k} (θ_{0})$ , $δ_{0} = ∥ z_{0} (θ_{0}) - z_{*} ∥$ , $d_{0} = ∥ e_{0} - s_{*} ∥$ , and $C = L_{z} ∥ s_{*} ∥ + L_{θ}$ . For every integer $K \geq 1$ , $∥ z_{K} (θ_{0}) - z_{*} ∥ \leq q^{K} δ_{0}, ∥ e_{K} - s_{*} ∥ \leq q^{K} d_{0} + C K q^{K - 1} δ_{0},$ with $q^{0} = 1$ when $q = 0, K = 1$ . If $R (z, θ) = z - G (z, θ)$ and $r_{K} = R (z_{K} (θ_{0}), θ_{0})$ , then $(1 - q) ∥ z_{K} - z_{*} ∥ \leq ∥ r_{K} ∥$ . The derivative error is not bounded by the residual alone: for $G (z, θ) = q z + (1 - q) θ$ , $θ_{0} = 0$ , and $z_{0} (θ) = 0$ , every finite $K$ has residual zero at $θ_{0}$ but $e_{K} = 1 - q^{K} \neq 1 = s_{*}$ when $0 < q < 1$ .

Facts & Assumptions

Given: The $C^{2}$ iteration map, invariant convex state neighborhood, contraction and derivative-Lipschitz bounds, fixed point, differentiable initial map, and finite iteration count.

[F1]

Differentiate a finite fixed-point iteration as a finite composed map: $z_{k + 1} = G (z_{k}, θ)$ , and the procedure applies forward mode to the finite composition.

[F2]

The Euclidean implicit function theorem with derivative formula: for $R (z, θ) = z - G (z, θ)$ , an invertible $R_{z}$ at a fixed point gives a local $C^{1}$ solution branch and its derivative formula.

[F3]

Forward mode computes the exact directional derivative of the real-arithmetic graph: exact forward mode returns the derivative of the finite graph in every input direction.

[F4]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : derivatives of finite compositions satisfy the chain rule.

[A1]

The stated invariant-neighborhood, uniform derivative, Lipschitz, and initial-map hypotheses hold on the neighborhoods used below.

[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 derivative bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ .

[F6]

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition: a finite-dimensional linear map has orthonormal singular-vector bases; a square map with no zero singular value is invertible.

Proof

technique · differentiate the finite recurrence and compare it with the fixed-point equation

1.1F6givenalgebra

Put $A_{*} = G_{z} (z_{*}, θ_{0})$ . For $m = 0$ , the unique endomorphism of $R^{0}$ is invertible. For $m \geq 1$ , the derivative bound gives $∥ (I - A_{*}) v ∥ \geq (1 - q) ∥ v ∥$ for every $v$ . By [F6], if $I - A_{*}$ had a zero singular value then it would annihilate a nonzero basis vector; hence all its $m$ singular values are positive, and the SVD bases show $I - A_{*}$ is invertible. Thus $R_{z} = I - A_{*}$ is invertible in every state dimension.

2.1F2F5A1step 1.1algebra

Since $∥ G_{z} (z_{*}, θ_{0}) ∥ \leq q$ , we have $q \geq 0$ . Applying [F5] to $z \mapsto G (z, θ_{0})$ on the convex open set $D$ gives $∥ G (z_{k}, θ_{0}) - G (z_{*}, θ_{0}) ∥ \leq q ∥ z_{k} - z_{*} ∥$ ; induction on the primal recurrence yields $∥ z_{k} - z_{*} ∥ \leq q^{k} δ_{0}$ . If $p, m \geq 1$ , apply [F2] to $R (z, θ) = z - G (z, θ)$ ; the exact branch derivative satisfies $s_{*} = A_{*} s_{*} + B_{*}$ , where $B_{*} = G_{θ} (z_{*}, θ_{0})$ . If $p = 0$ and $m \geq 1$ , then $Θ = {θ_{0}}$ ; contraction on $D$ makes $z_{*}$ the unique fixed point there, so the constant branch has $s_{*} = 0 = B_{*}$ and the same identity. If $m = 0$ , the state space and all state-valued derivatives are zero-dimensional, and that identity is again immediate. Thus the fixed-point branch and identity used below hold in all allowed dimensions.

3.1F1F2F3F4step 2.1algebra

Because $U$ is open, $z_{0}$ is continuous, and the finite trajectory at $θ_{0}$ lies in $D$ , induction gives a neighborhood of $θ_{0}$ on which each of the first $K$ evaluations stays in $U$ ; hence every $e_{k}$ below exists. By [F4], the derivative of $z_{k + 1} = G (z_{k}, θ)$ is $e_{k + 1} = A_{k} e_{k} + B_{k}$ , where $A_{k} = G_{z} (z_{k}, θ_{0})$ and $B_{k} = G_{θ} (z_{k}, θ_{0})$ ; [F3] computes that exact finite-graph derivative. Subtract $s_{*} = A_{*} s_{*} + B_{*}$ to obtain $e_{k + 1} - s_{*} = A_{k} (e_{k} - s_{*}) + (A_{k} - A_{*}) s_{*} + (B_{k} - B_{*})$ .

4.1A1step 2.1step 3.1algebra

Set $D_{k} = ∥ e_{k} - s_{*} ∥$ . Taking norms and applying the hypotheses gives $D_{k + 1} \leq q D_{k} + C ∥ z_{k} - z_{*} ∥ \leq q D_{k} + C δ_{0} q^{k}$ by step 2.1. For $K = 1$ this gives $D_{1} \leq q d_{0} + C δ_{0}$ . If $D_{K} \leq q^{K} d_{0} + C δ_{0} \sum_{j = 0}^{K - 1} q^{K - 1 - j} q^{j}$ , then $D_{K + 1} \leq q^{K + 1} d_{0} + C δ_{0} \sum_{j = 0}^{K - 1} q^{K - j} q^{j} + C δ_{0} q^{K} = q^{K + 1} d_{0} + C δ_{0} \sum_{j = 0}^{K} q^{K - j} q^{j} .$ Induction proves the sum bound for every $K \geq 1$ . Each summand equals $q^{K - 1}$ , including the stated convention at $q = 0, K = 1$ , so the sum is $K q^{K - 1}$ .

5.1A1step 2.1step 3.1step 4.1algebra∎

The residual identity $r_{K} = (z_{K} - z_{*}) - (G (z_{K}, θ_{0}) - G (z_{*}, θ_{0}))$ and the triangle inequality imply $(1 - q) ∥ z_{K} - z_{*} ∥ \leq ∥ r_{K} ∥$ . For the stated scalar example, $z_{*} = θ$ , $z_{k} (0) = 0$ and $r_{K} = 0$ ; differentiating the recurrence gives $e_{k + 1} = q e_{k} + (1 - q)$ , $e_{0} = 0$ , hence $e_{K} = 1 - q^{K}$ , whereas $s_{*} = 1$ . Thus a finite-iteration derivative is a different target even at zero primal residual, with its discrepancy still bounded by step 4.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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

Atilım Güneş Baydin and Barak A. Pearlmutter, Automatic Differentiation of Algorithms for Machine Learning, complete arXiv text, §§2–3 (standard reference, not scraped)
J. Lebl, Basic Analysis II, Theorem 8.5.6 and proof, §8.5.1 (standard reference, not scraped)