The laws of propagation of relative uncertainty
ProvedCODATA.propagation_lawsLet V be a covariance matrix with positive diagonal entries. Four algebraic laws of the propagation of relative uncertainty hold. Every diagonal correlation coefficient is one. The relative variance of the linear combination concentrated at a single component, with sensitivity minus one there, is the square of the relative uncertainty of that component. The relative variance scales by the square of a scalar multiple of the sensitivity vector. And when all off-diagonal covariances vanish, the relative variance of any linear combination is the sum over components of the squared sensitivity times the squared relative uncertainty. These are the algebraic facts underlying the derivation of the recommended values and their uncertainties from the adjusted constants and their covariances in the 2022 CODATA report.
import Mathlib import Definitions.Def_CODATA_lsa import Definitions.Def_CODATA_uncert import Definitions.Def_CODATA_values
/-!
# The laws of propagation of relative uncertainty
The recommended values of the 2022 CODATA report are obtained from
the adjusted constants by propagating their uncertainties and
covariances. This milestone verifies the algebraic skeleton of that
propagation law for relative uncertainties, in the form recorded in
`Def_CODATA_uncert`: the correlation coefficient of an entry with
itself is one; the relative variance of a single component of the
value vector is the square of its relative uncertainty; the relative
variance scales quadratically in the sensitivity vector; and for
uncorrelated inputs the relative variances add. This milestone is
proved on the way to the goal theorem
`CODATA.codata_self_consistent`.
-/
namespace CODATA
/-- Let V be a covariance matrix with positive diagonal entries. Every
diagonal correlation coefficient is one; the relative variance of the
linear combination concentrated at a single component k with
sensitivity minus one is the square of the relative uncertainty of
that component; the relative variance scales by the square of a scalar
multiple of the sensitivity vector; and when all off-diagonal
covariances vanish, the relative variance of any linear combination is
the sum of the squared relative uncertainties weighted by the squared
sensitivities. -/
theorem propagation_laws {N : ℕ} (V : Matrix (Fin N) (Fin N) ℝ)
(hV : ∀ k, 0 < V k k) :
(∀ k, corr V k k = 1) ∧
(∀ k (u x : Fin N → ℝ),
relVar V u x (fun j => if j = k then -1 else 0)
= (u k / abs (x k))^2) ∧
(∀ c (p u x : Fin N → ℝ),
relVar V u x (fun i => c * p i) = c * c * relVar V u x p) ∧
((∀ k l, k ≠ l → V k l = 0) →
∀ (p u x : Fin N → ℝ),
relVar V u x p
= ∑ k, p k * p k * (u k / abs (x k)) * (u k / abs (x k))) := by
sorry
end CODATA
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The formal statement fixes a covariance matrix V with positive diagonal entries and asserts four conjunctions. First, for every index k, the correlation coefficient of V at (k, k) equals one, the coefficient being the diagonal entry divided by the square root of its product with itself. Second, for every index k and vectors u and x of uncertainties and values, the relative variance of the sensitivity vector that is minus one at k and zero elsewhere equals the square of u k divided by the absolute value of x k. Third, for every scalar c and sensitivity vector p, the relative variance of the vector c times p equals c times c times the relative variance of p. Fourth, if all off-diagonal entries of V vanish, then the relative variance of any sensitivity vector equals the sum over k of p k squared times the squared relative uncertainty of component k. The statement renders the intended milestone faithfully: the algebraic skeleton of the propagation law for relative uncertainties. No particular constant is claimed here.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.