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

Multivariate Cramér–Rao bound

Statement

Assume AC for the selected density representatives. Let $Θ \subseteq R^{d}$ be open and fix $θ \in Θ$ . Let $T : X \to R^{k}$ be a measurable estimator (Statistics and estimators) with finite second moments and $E_{θ} T = ψ (θ)$ coordinatewise (this is the meaning of unbiasedness here), where $ψ : Θ \to R^{k}$ is differentiable at $θ$ . Let the score vector $S_{θ}$ be square-integrable, have mean zero, and have nonsingular information matrix $I (θ) = E_{θ} [S_{θ} S_{θ}^{T}]$ . Assume the vector score-derivative identity $E_{θ} [(T - ψ (θ)) S_{θ}^{T}] = D ψ (θ),$ where $D ψ (θ)$ is the $k \times d$ Jacobian matrix with entries $\partial ψ_{a} / \partial θ_{j}$ . Then ${Cov}_{θ} (T) ⪰ D ψ (θ) I (θ)^{- 1} D ψ (θ)^{T} .$ Here $A ⪰ B$ means $a^{T} (A - B) a \geq 0$ for every $a \in R^{k}$ , and ${Cov}_{θ} (T)$ is the matrix whose $a, b$ entry is ${Cov}_{θ} (T_{a}, T_{b})$ . The mean-zero and score-derivative identities are explicit hypotheses; common support with suitable derivative-interchange conditions is one sufficient regular route, not the only possible route. If each coordinate $T_{a}$ is a finite-variance unbiased estimator of the real estimand $ψ_{a}$ in the sense of Unbiased estimators and UMVU estimators, then $T$ satisfies the pointwise mean and moment premises; the score-derivative identity remains a separate condition.

Facts & Assumptions

Given: AC; an open $d$ -dimensional parameter set; a measurable $R^{k}$ -valued estimator $T$ with finite second moments and mean $ψ (θ)$ ; a square-integrable score vector $S_{θ}$ with mean zero and nonsingular $I (θ) = E_{θ} [S_{θ} S_{θ}^{T}]$ ; the vector derivative identity; and the stated quadratic-form definition of $⪰$ .

[A1]

The Axiom of Choice: AC supplies the arbitrary-index family of selected density representatives used by the score.

[F1]

Score and Fisher information: the score is the gradient of the log density and $I (θ)$ has entries $E_{θ} [S_{θ, i} S_{θ, j}]$ .

[F2]

Mean-zero score and the information identity: under its regularity hypotheses, the score mean is zero and the information matrix is its second-moment matrix.

[F3]

Statistics and estimators: an estimator is a measurable statistic with its target measurable space specified.

[F4]

Moments, variance, and covariance on a probability space: covariance is the expectation of centered coordinate products; for a vector, this defines the covariance matrix entrywise.

[F5]

Expectation of a nonnegative or integrable random variable: expectation is integration against the sampling probability measure.

[F6]

Unbiased estimators and UMVU estimators, applied to each real coordinate: if $T_{a}$ is finite-variance unbiased for $ψ_{a}$ , then $E_{η} T_{a} = ψ_{a} (η)$ and $E_{η} T_{a}^{2} < \infty$ at every parameter.

[F7]

The Lebesgue integral is linear on $L^{1} (μ)$ : expectation is linear on integrable real random variables. Finite second moments imply first moments on a probability space (use $∣ z ∣ \leq (1 + z^{2}) / 2$ ), and all products of coordinates in the covariance expansion are integrable by $2 ∣ Y Z ∣ \leq Y^{2} + Z^{2}$ .

Proof

technique · direct

1.1A1F1F2F3F4F5F6F7givenconstruct

Applying [F6] to each coordinate of a globally finite-variance unbiased vector estimator shows that it satisfies the theorem's pointwise mean and moment premises; the score-derivative identity is separately assumed. Define $R : = T - ψ (θ) - D ψ (θ) I (θ)^{- 1} S_{θ}$ . The stated mean assumptions and expectation linearity [F7] give $E_{θ} R = 0$ , so ${Cov}_{θ} (R) = E_{θ} [R R^{T}]$ .

2.1F1F4F7step 1.1givenalgebra

Expand the residual covariance using expectation linearity [F7], $E_{θ} [(T - ψ) S_{θ}^{T}] = D ψ$ , $E_{θ} [S_{θ} (T - ψ)^{T}] = D ψ^{T}$ , and $E_{θ} [S_{θ} S_{θ}^{T}] = I$ . The products are integrable by the coordinate bound in [F7]. Since $I$ is symmetric and nonsingular, $I^{- 1}$ is symmetric, and matrix multiplication yields ${Cov}_{θ} (R) = {Cov}_{θ} (T) - D ψ (θ) I (θ)^{- 1} D ψ (θ)^{T} .$

3.1step 2.1givenalgebra∎

For every $a \in R^{k}$ , $a^{T} {Cov}_{θ} (R) a = E_{θ} [(a^{T} R)^{2}] \geq 0$ . By the definition of $⪰$ in the Statement and step 2.1, this is exactly ${Cov}_{θ} (T) ⪰ D ψ (θ) I (θ)^{- 1} D ψ (θ)^{T}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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

George Deligiannidis, SB2.1 Foundations of Statistical Inference, Theorem 5.9 and proof sketch, PDF pp. 32–33 (standard reference, not scraped)
Peter Kempthorne, MIT 18.655 Lecture 13: Unbiased Estimation and Risk Inequalities, Theorems 3.4.3–3.4.4, PDF pp. 18–19 (standard reference, not scraped)