ExampleConstruction: AI-generatedVerification: 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.

Exact variance against propagated variance for a nonlinear observation map

Example

Let $Ω = {ω_{0}, ω_{1}, ω_{2}}$ carry the weights $w (ω_{0}) = 1 / 2$ , $w (ω_{1}) = w (ω_{2}) = 1 / 4$ , let $Y : Ω ⟶ R, Y (ω_{0}) = 0, Y (ω_{1}) = 1, Y (ω_{2}) = 3,$ and let $h (y) : = y^{2}$ on the open convex set $U = (- 1, 4)$ , which contains the three values of $Y$ . Then $h$ is $C^{2}$ with constant Hessian $H_{h} (x) = (2)$ and operator norm $B = 2$ , the mean is $μ = E [Y] = 1 \in U$ , and $E [Y^{2}] = \frac{5}{2}, Var (Y) = \frac{3}{2}, E [Y^{4}] = \frac{41}{2}, Var (h (Y)) = \frac{41}{2} - (\frac{5}{2})^{2} = \frac{57}{4} .$ The linearization $T (y) = h (1) + h^{'} (1) (y - 1) = 1 + 2 (y - 1)$ has variance $h^{'} (1)^{2} Var (Y) = 4 \cdot \frac{3}{2} = 6 = \frac{24}{4} \neq \frac{57}{4} = Var (h (Y)),$ so the propagated variance is not the exact variance of $h (Y)$ . The linearization error $R = h (Y) - T (Y) = (Y - 1)^{2}$ satisfies $E [R] = \frac{3}{2} = \frac{B}{2} E [(Y - 1)^{2}], E [R^{2}] = \frac{9}{2} = \frac{B^{2}}{4} E [(Y - 1)^{4}],$ so both displayed bounds of Mean, mean-square and covariance bounds for second-order linearization error are attained in this example. The example contains no measured quantity and asserts no physical model.

Facts & Assumptions

Given: The finite weighted set $(Ω, w)$ and the random variable $Y$ displayed in the Example; the function $h (y) = y^{2}$ on $U = (- 1, 4)$ .

[L1]

The finite probability space $(Ω, w)$ determines a probability measure $P$ on $(Ω, P (Ω))$ with $P (A) = \sum_{ω \in A} w (ω)$ , and expectations of finite-valued random variables computed by the finite weighted sum agree with their expectations as random variables on that probability space. (Finite probability spaces are exactly finite full-power-set probability spaces, Expectation of a real random variable on a finite probability space, Finite probability spaces, outcome weights, events, and event probabilities)

[L2]

If $h : U \to R$ is $C^{2}$ on the open convex set $U$ , $∥ H_{h} (x) ∥ \leq B$ on $U$ , $X$ takes values in $U$ with $E [X] = μ \in U$ and $E ∣ X - μ ∣^{2} < + \infty$ , then the linearization error $R = h (X) - h (μ) - h^{'} (μ) (X - μ)$ satisfies $∣ E [R] ∣ \leq E ∣ R ∣ \leq \frac{B}{2} E ∣ X - μ ∣^{2}$ , and $E [R^{2}] \leq \frac{B^{2}}{4} E ∣ X - μ ∣^{4}$ when the fourth moment is finite. (Mean, mean-square and covariance bounds for second-order linearization error)

[L3]

For a square-integrable random variable $X$ with mean $μ$ , the covariance matrix of the one-dimensional random vector $(X)$ is the $1 \times 1$ matrix $(Var (X))$ , and the linearization $x \mapsto h (μ) + h^{'} (μ) (x - μ)$ has covariance matrix $h^{'} (μ)^{2} Var (X)$ . (Mean vector and covariance matrix of a square-integrable random vector, The covariance of the linearization is $A Σ A^{T}$ )

[L4]

The derivative of $h (y) = y^{2}$ is $h^{'} (y) = 2 y$ , and variance is $Var (X) = E [X^{2}] - E [X]^{2}$ for square-integrable $X$ . (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, Moments, variance, and covariance on a probability space)

Verification

technique · direct computation on a finite probability space

1.1givenL1algebra

By [L1] the weights make $(Ω, w)$ a probability space and the expectations below are the finite weighted sums of Expectation of a real random variable on a finite probability space: $E [Y] = \frac{1}{2} \cdot 0 + \frac{1}{4} \cdot 1 + \frac{1}{4} \cdot 3 = 1, E [Y^{2}] = \frac{1}{4} \cdot 1 + \frac{1}{4} \cdot 9 = \frac{5}{2},$ $E [Y^{4}] = \frac{1}{4} \cdot 1 + \frac{1}{4} \cdot 81 = \frac{82}{4} = \frac{41}{2}, E [(Y - 1)^{2}] = \frac{1}{2} \cdot 1 + \frac{1}{4} \cdot 0 + \frac{1}{4} \cdot 4 = \frac{3}{2},$ and $E [(Y - 1)^{4}] = \frac{1}{2} \cdot 1 + \frac{1}{4} \cdot 0 + \frac{1}{4} \cdot 16 = \frac{1}{2} + 4 = \frac{9}{2}$ .

1.2givenL3L4algebra

The function $h (y) = y^{2}$ is $C^{2}$ on the open convex set $U = (- 1, 4)$ , with $h^{'} (y) = 2 y$ , so $h (1) = 1$ and $h^{'} (1) = 2$ ; its Hessian is the constant matrix $(2)$ , of operator norm $B = 2$ by [L3] and [L4], and the values $0, 1, 3$ of $Y$ and the mean $μ = 1$ all lie in $U$ .

2.1step 1.1L4algebra

By [L4], $Var (Y) = E [Y^{2}] - E [Y]^{2} = \frac{5}{2} - 1 = \frac{3}{2}$ and $Var (h (Y)) = E [Y^{4}] - E [Y^{2}]^{2} = \frac{41}{2} - \frac{25}{4} = \frac{82 - 25}{4} = \frac{57}{4}$ .

2.2step 1.2algebra

The linearization error is $R = h (Y) - 1 - 2 (Y - 1) = Y^{2} - 2 Y + 1 = (Y - 1)^{2}$ .

3.1step 1.2step 2.1L3algebra

By [L3] the propagated covariance is $h^{'} (1)^{2} Var (Y) = 4 \cdot \frac{3}{2} = 6 = \frac{24}{4}$ , while step 2.1 gives $Var (h (Y)) = \frac{57}{4}$ ; these differ, so the propagated covariance is not the exact variance of $h (Y)$ in this model.

4.1step 1.1step 2.2L2algebra∎

With $B = 2$ and the moments of step 1.1, the bounds of [L2] read $\frac{B}{2} E [(Y - 1)^{2}] = 1 \cdot \frac{3}{2} = \frac{3}{2}$ and $\frac{B^{2}}{4} E [(Y - 1)^{4}] = 1 \cdot \frac{9}{2} = \frac{9}{2}$ ; since $R^{2} = (Y - 1)^{4}$ by step 2.2, one has $E [R] = \frac{3}{2}$ and $E [R^{2}] = \frac{9}{2}$ , so both bounds are attained.

Depends on

Dependency tree · 2 levels

Sources

JCGM 100:2008, Evaluation of measurement data — Guide to the expression of uncertainty in measurement (BIPM), clause 5.1.2, note to equation (10), on higher-order terms when the nonlinearity of the model function is significant