TheoremStatement: Literature-sourcedProof: 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.

3DVAR tracking error under a global contraction and bounded observation error

Statement

Let $d, p \geq 1$ be integers, let $Ψ : R^{d} \to R^{d}$ , $H \in R^{p \times d}$ , and fixed symmetric positive-definite $B \in R^{d \times d}$ , $Γ \in R^{p \times p}$ . Define $S = H B H^{T} + Γ$ , $K = B H^{T} S^{- 1}$ , and $F = (I - K H) \circ Ψ$ . Suppose $F$ is globally Lipschitz with constant $a$ in a norm $∥ \cdot ∥$ on $R^{d}$ , where $0 \leq a < 1$ . Let the true path satisfy $v_{j + 1}^{†} = Ψ (v_{j}^{†})$ , let $y_{j + 1} = H v_{j + 1}^{†} + ϵ_{j}$ , and assume $\sup_{j \geq 0} ∥ ϵ_{j} ∥_{2} \leq ϵ < \infty$ . Starting from any $m_{0} \in R^{d}$ , run the 3DVAR update $m_{j + 1} = (I - K H) Ψ (m_{j}) + K y_{j + 1} .$ Let $e_{1}, \dots, e_{p}$ be the standard basis of $R^{p}$ and set $κ : = \sum_{r = 1}^{p} ∥ K e_{r} ∥ < \infty$ . Then ${lim sup}_{j \to \infty} ∥ m_{j} - v_{j}^{†} ∥ \leq \frac{κ}{1 - a} ϵ .$

Facts & Assumptions

Given: The model, positive-definite covariances, data-error bound, and global contraction hypothesis in the Statement.

[F1]

The 3DVAR analysis update has $m_{j + 1} = (I - K H) Ψ (m_{j}) + K y_{j + 1}$ with the fixed gain $K$ . Finite-dimensional 3DVAR analysis

[F2]

For $z = (z_{1}, \dots, z_{p})$ , linearity and $∣ z_{r} ∣ \leq ∥ z ∥_{2}$ give $∥ K z ∥ = ∥ \sum_{r} z_{r} K e_{r} ∥ \leq \sum_{r} ∣ z_{r} ∣ ∥ K e_{r} ∥ \leq κ ∥ z ∥_{2}$ .

[A1]

The map $F = (I - K H) \circ Ψ$ is globally Lipschitz with constant $0 \leq a < 1$ .

[A2]

The observation errors satisfy $∥ ϵ_{j} ∥_{2} \leq ϵ$ for all $j \geq 0$ .

Proof

Given: The hypotheses in the Statement.

1.1A1A2F1F2givenalgebra

Set $e_{j} = m_{j} - v_{j}^{†}$ . By [F1], the observation equation, and $v_{j + 1}^{†} = Ψ (v_{j}^{†})$ , $e_{j + 1} = F (m_{j}) - F (v_{j}^{†}) + K ϵ_{j} .$ The contraction bound [A1], triangle inequality, and [F2] give $∥ e_{j + 1} ∥ \leq a ∥ e_{j} ∥ + κ ϵ .$

2.1step 1.1givenalgebra∎

Put $c = κ ϵ$ . Repeated substitution in step 1.1 gives, for each $n \geq 1$ , $∥ e_{n} ∥ \leq a^{n} ∥ e_{0} ∥ + c \sum_{r = 0}^{n - 1} a^{r} = a^{n} ∥ e_{0} ∥ + c \frac{1 - a^{n}}{1 - a} .$ For $a = 0$ the finite sum is $1$ and the same expression holds for every $n \geq 1$ . Since $0 \leq a < 1$ , $a^{n} \to 0$ , so taking the limit superior proves the bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

K. J. H. Law, A. M. Stuart, and K. C. Zygalakis, Data Assimilation: A Mathematical Introduction, Chapter 4 §4.4.2, Theorem 4.10 and proof (standard reference, not scraped)
Geir Evensen, Femke C. Vossepoel, and Peter Jan van Leeuwen, Data Assimilation Fundamentals, Chapter 6 §6.2 (standard reference, not scraped)