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

Computed Jacobian error controls the weighted information-matrix error

Statement

Use the finite observation designs of Finite nonlinear observation designs, local identifiability, and weighted information. Suppose uniformly over $x \in X$ that $∥ J_{x} ∥_{2} \leq K$ , $∥ J_{h, x} - J_{x} ∥_{2} \leq η$ , and $∥ W_{x} ∥_{2} \leq w$ , where $K, η, w \geq 0$ . For every approximate design $ξ$ , $∥ M_{h} (ξ) - M (ξ) ∥_{2} \leq δ : = w (2 K η + η^{2}),$ where $M_{h} (ξ) = \sum_{x} ξ_{x} J_{h, x}^{T} W_{x} J_{h, x}$ . If $M (ξ)$ satisfies $v^{T} M (ξ) v \geq α ∥ v ∥_{2}^{2}$ for every $v$ with some $α > δ$ , then $v^{T} M_{h} (ξ) v \geq (α - δ) ∥ v ∥_{2}^{2}$ for every $v$ , so the computed information matrix remains positive definite.

Facts & Assumptions

Given: A finite approximate design $ξ$ , the Jacobians and weights in the Statement, and the uniform matrix-norm bounds $K, η, w, α$ .

[F1]

Finite nonlinear observation designs, local identifiability, and weighted information: $M (ξ) = \sum_{x} ξ_{x} J_{x}^{T} W_{x} J_{x}$ , with $ξ_{x} \geq 0$ and $\sum_{x} ξ_{x} = 1$ ; the matrices $W_{x}$ are symmetric.

[F2]

The matrix norm induced by a published vector p-norm and Induced matrix norms are compatible with matrix-vector multiplication, submultiplicative, and satisfy ||I|| = 1: at $p = 2$ , the Euclidean induced matrix norm satisfies both $∥ A B ∥_{2} \leq ∥ A ∥_{2} ∥ B ∥_{2}$ and $∥ A v ∥_{2} \leq ∥ A ∥_{2} ∥ v ∥_{2}$ .

[F3]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||, Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition, and The operator norm is 0 on the zero domain and otherwise equals the largest singular value, attained at a right-singular vector: the induced Euclidean matrix norm is the operator norm; a real matrix and its transpose have the same largest singular value, since transposing an SVD preserves its positive singular values.

[F4]

Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes: matrix products associate and distribute over sums.

[F5]

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

Proof

technique · direct

1.1givenF1F2F3F4algebra

Put $E_{x} = J_{h, x} - J_{x}$ . By [F4], $J_{h, x}^{T} W_{x} J_{h, x} - J_{x}^{T} W_{x} J_{x} = J_{x}^{T} W_{x} E_{x} + E_{x}^{T} W_{x} J_{x} + E_{x}^{T} W_{x} E_{x}$ . By [F2] and [F3], the Euclidean operator norm of the right side is at most $∥ J_{x} ∥_{2} ∥ W_{x} ∥_{2} ∥ E_{x} ∥_{2} + ∥ E_{x} ∥_{2} ∥ W_{x} ∥_{2} ∥ J_{x} ∥_{2} + ∥ E_{x} ∥_{2} ∥ W_{x} ∥_{2} ∥ E_{x} ∥_{2} \leq w (2 K η + η^{2}) = δ$ .

2.1step 1.1F1algebra

Taking the design-weighted sum and using the triangle inequality gives $∥ M_{h} (ξ) - M (ξ) ∥_{2} \leq \sum_{x} ξ_{x} δ = δ$ , since the weights are nonnegative and sum to one.

3.1givenstep 2.1F1F2F5algebra∎

Let $v \in R^{p}$ . By step 2.1, the operator norm bound and Cauchy–Schwarz [F5], $∣ v^{T} (M_{h} - M) v ∣ \leq ∥ v ∥_{2} ∥ (M_{h} - M) v ∥_{2} \leq δ ∥ v ∥_{2}^{2}$ . Therefore $v^{T} M_{h} v \geq v^{T} M v - ∣ v^{T} (M_{h} - M) v ∣ \geq (α - δ) ∥ v ∥_{2}^{2}$ . Since $α > δ$ , this is positive for every nonzero $v$ , proving positive definiteness.

Depends on

Used by

Dependency tree · two levels

35 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.3 (standard reference, not scraped)
Jorge Nocedal and Stephen J. Wright, Numerical Optimization, second edition, Ch. 10 (standard reference, not scraped)