The single adjusted constant: the weighted mean and its variance
ProvedCODATA.weighted_meanFor a weighted least-squares problem with one adjusted constant, at least one input datum, zero offsets, observational equations of the form y i = x, and a strictly positive definite weight matrix, the solution x of the normal equations satisfies: x is the weighted mean of the data, the weight being the total sum of the entries of the weight matrix; the one-by-one normal matrix has a two-sided inverse whose single entry, the variance of the adjusted constant, is the reciprocal of the total weight; and every other solution of the normal equations has the same value. This is the situation of the separate adjustment of the sixteen values of the Newtonian constant of gravitation in the 2022 CODATA report: sixteen input data for a single adjusted constant, with the expansion factor 3.9 applied to all the uncertainties.
import Mathlib import Definitions.Def_CODATA_lsa import Definitions.Def_CODATA_uncert import Definitions.Def_CODATA_values
/-!
# The single adjusted constant: the weighted mean
The 2022 CODATA report treats the Newtonian constant of gravitation
separately: an adjustment of sixteen input data for a single adjusted
constant (sixteen minus one equals fifteen degrees of freedom), with
an expansion factor of 3.9 applied to the uncertainties of all the
data. This milestone identifies the general rank-one case of the
least-squares model of `Def_CODATA_lsa`: when every observational
equation reads y i = x + 0, the adjusted constant is the weighted mean
of the data, the weights being the entries of the weight matrix; its
variance is the single entry of the inverse of the normal matrix; and
the adjusted value is unique. This milestone is proved on the way to
the goal theorem `CODATA.codata_self_consistent`.
-/
namespace CODATA
/-- For a least-squares problem with one adjusted constant, at least
one input datum, zero offsets, observational equations y i = x and a
strictly positive definite weight matrix, the adjusted constant at a
solution x of the normal equations is the weighted mean
(sum_i sum_j G i j y j) / (sum_i sum_j G i j); there is a two-sided
inverse C of the normal matrix, the variance of the adjusted constant
is its (0, 0) entry, 1 / (sum_i sum_j G i j); and every other solution
of the normal equations has the same value. -/
theorem weighted_mean {N : ℕ} (L : LSQ N 1) (hN : 0 < N)
(hG : IsSPD L.G) (hA : ∀ i, L.A i 0 = 1) (hb : ∀ i, L.b i = 0)
(x : Fin 1 → ℝ) (hx : SolvesNormal L x) :
x 0 = (∑ i, ∑ j, L.G i j * L.y j) / (∑ i, ∑ j, L.G i j) ∧
∃ C, IsCov L C ∧ C 0 0 = 1 / (∑ i, ∑ j, L.G i j) ∧
∀ z, SolvesNormal L z → z 0 = x 0 := by
sorry
end CODATA
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The formal statement fixes a least-squares structure L with N input data and one adjusted constant, assumes N is positive, the weight matrix is symmetric and strictly positive definite, every design matrix entry in the single column is one, every offset is zero, and x solves the normal equations. The conclusion has three parts. First, the adjusted constant x 0 equals the double sum of the weight matrix entries times the data, divided by the double sum of the weight matrix entries: the weighted mean. Second, there exists a two-sided inverse C of the normal matrix, and its (0, 0) entry equals the reciprocal of the double sum of the weight matrix entries: the variance of the weighted mean. Third, any other solution z of the normal equations satisfies z 0 = x 0. The statement renders the intended milestone faithfully: the rank-one case of the adjustment, of which the separate adjustment of the Newtonian constant of gravitation is the instance in the 2022 report.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.