TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-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.

A lower singular-value bound and Lipschitz Jacobian control local parameter error

Statement

Let $F : Θ \to R^{m}$ be $C^{1}$ on an open $Θ \subseteq R^{p}$ , let $θ_{0} \in Θ$ , and let $r_{0} > 0$ be such that the closed Euclidean ball $\overline{B} (θ_{0}, r_{0})$ lies in $Θ$ . Suppose $∥ D F (θ_{0}) v ∥_{2} \geq μ ∥ v ∥_{2}$ for every $v \in R^{p}$ , where $μ > 0$ , and suppose $D F$ is $L$ -Lipschitz in operator norm on this ball, where $L \geq 0$ . Define $r = r_{0}$ if $L = 0$ and $r = \min {r_{0}, μ / (2 L)}$ if $L > 0$ . If $y = F (θ_{0}) + e$ with $∥ e ∥_{2} \leq δ$ , and $\hat{θ} \in \overline{B} (θ_{0}, r)$ satisfies $∥ F (\hat{θ}) - y ∥_{2} \leq ε$ , then $∥ \hat{θ} - θ_{0} ∥_{2} \leq \frac{2 (ε + δ)}{μ} .$ The bound is conditional on the stated local ball and on the existence of such a fit; it does not assert that a fit exists.

Facts & Assumptions

Given: $F, Θ, θ_{0}, r_{0}, μ, L, y, e, \hat{θ}, ε, δ$ with the hypotheses in the Statement.

[F1]

Finite nonlinear observation designs, local identifiability, and weighted information: the Jacobian is the total derivative of the observation map; a lower singular-value bound $μ$ means $∥ D F (θ_{0}) v ∥_{2} \geq μ ∥ v ∥_{2}$ for every $v$ .

[F2]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : for a differentiable path $γ$ , $D (F \circ γ) (t) = D F (γ (t)) D γ (t)$ .

[F3]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||: $∥ A v ∥_{2} \leq ∥ A ∥_{2} ∥ v ∥_{2}$ for a linear map $A$ and vector $v$ .

[F4]

Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction: $L$ -Lipschitz means $∥ D F (u) - D F (v) ∥_{2} \leq L ∥ u - v ∥_{2}$ on the stated ball.

[F5]

If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz: for $m \geq 1$ , a path into $R^{m}$ continuous on $[0, 1]$ and differentiable on $(0, 1)$ with derivative norm at most $C \geq 0$ is $C$ -Lipschitz there.

[F6]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: the Euclidean norm satisfies the triangle and reverse-triangle inequalities.

Proof

technique · direct

1.1givenF1F2construct

Put $h = \hat{θ} - θ_{0}$ and define $R (t) = F (θ_{0} + t h) - F (θ_{0}) - t D F (θ_{0}) h$ for $0 \leq t \leq 1$ . The segment stays in the convex ball. By [F2], $R^{'} (t) = (D F (θ_{0} + t h) - D F (θ_{0})) h$ .

2.1step 1.1F3F4F5algebra

If $m = 0$ , the path $R$ is identically the zero vector, so $∥ R (1) - R (0) ∥_{2} = 0 \leq L ∥ h ∥_{2}^{2}$ . If $m \geq 1$ , [F4] and [F3] give $∥ R^{'} (t) ∥_{2} \leq L t ∥ h ∥_{2}^{2} \leq L ∥ h ∥_{2}^{2}$ for $0 < t < 1$ ; since $R$ is continuous on $[0, 1]$ and differentiable on $(0, 1)$ , [F5] gives $∥ R (1) - R (0) ∥_{2} \leq L ∥ h ∥_{2}^{2}$ . In either case, $R (0) = 0$ yields the first-order remainder bound $∥ F (θ_{0} + h) - F (θ_{0}) - D F (θ_{0}) h ∥_{2} \leq L ∥ h ∥_{2}^{2}$ .

3.1givenF1step 2.1F6algebra

If $L > 0$ , then $∥ h ∥_{2} \leq r \leq μ / (2 L)$ , so [F1], step 2.1, and the reverse-triangle inequality [F6] yield $∥ F (\hat{θ}) - F (θ_{0}) ∥_{2} \geq μ ∥ h ∥_{2} - L ∥ h ∥_{2}^{2} \geq (μ / 2) ∥ h ∥_{2}$ . If $L = 0$ , step 2.1 gives zero remainder, and the same lower bound follows from [F1].

4.1givenstep 3.1F6algebra∎

The fit condition and $y = F (θ_{0}) + e$ give $∥ F (\hat{θ}) - F (θ_{0}) ∥_{2} \leq ∥ F (\hat{θ}) - y ∥_{2} + ∥ e ∥_{2} \leq ε + δ$ . Combining with step 3.1 gives $(μ / 2) ∥ h ∥_{2} \leq ε + δ$ , and division by $μ / 2 > 0$ proves the asserted bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 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

Leah R. McLean et al., Estimability Analysis and Optimal Design in Dynamic Multi-scale Models of Cardiac Electrophysiology, §§2.1–2.2 (standard reference, not scraped)
Henrik Madsen, Optimal Experimental Design for Grey-box Models, §1.2.3 (standard reference, not scraped)