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

Efficient score gives the canonical gradient

Statement

Assume the Axiom of Choice and Countable Choice.

Let $H = L_{0}^{2} (P)$ , let $S_{θ} \in H^{p}$ be a finite-dimensional interest-score vector, and let $T_{η} \subseteq T \subseteq H$ be closed linear nuisance and full tangent spaces, with $T_{η}$ a subspace of $T$ . Assume the designated allowed score set is exactly

$S = {a^{T} S_{θ} + t : a \in R^{p}, t \in T_{η}}, T = {\overline{S}}^{L^{2} (P)},$

and every allowed one-sided path with score $a^{T} S_{θ} + t \in S$ has right target derivative $a$ for the parameter $θ$ . If $I_{e f f} = E_{P} [S_{e f f} S_{e f f}^{T}]$ is nonsingular, then $θ$ is pathwise differentiable and its canonical gradient is

$ϕ_{c a n} = I_{e f f}^{- 1} S_{e f f} .$

Its covariance matrix is $E_{P} [ϕ_{c a n} ϕ_{c a n}^{T}] = I_{e f f}^{- 1}$ . This theorem does not assert that an estimator attaining the covariance bound exists.

Facts & Assumptions

Given: The score-space decomposition and right-derivative convention in the statement, $S_{θ} \in L_{0}^{2} (P)^{p}$ , a closed nuisance tangent space $T_{η}$ , a closed full tangent space $T$ , the Axiom of Choice for selected score-density representatives, Countable Choice for Hilbert projection/Riesz representation, and nonsingular $I_{e f f}$ .

[F1]

Efficient score and efficient information: $S_{e f f} = S_{θ} - Π_{T_{η}} S_{θ}$ and $I_{e f f} = E_{P} [S_{e f f} S_{e f f}^{T}]$ .

[F2]

Pathwise differentiability and parameter influence curves: a derivative represented by $ϕ \in L_{0}^{2} (P)^{p}$ through $E_{P} [ϕ s]$ is a pathwise derivative; its canonical gradient is the unique representer in the full tangent space.

[F3]

Influence-curve representers form an affine orthogonal-complement class: the canonical gradient is the unique representer in the full tangent space.

[F4]

Mean-zero square-integrable functions: $L_{0}^{2} (P)$ is the space of mean-zero real $L^{2} (P)$ classes.

[F5]

The mean-zero L² space is a Hilbert space: under Countable Choice, $L_{0}^{2} (P)$ is a real Hilbert space.

[F6]

A tangent space is a closed linear subspace: the full tangent space is a closed linear subspace of $L_{0}^{2} (P)$ .

[F7]

Orthogonal decomposition by a closed subspace: under Countable Choice, projection onto a closed linear subspace exists and has an orthogonal residual.

[F8]

Orthogonality and the orthogonal complement: a residual orthogonal to every nuisance direction belongs to the nuisance orthogonal complement.

[F9]

Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs: inner products are bounded by products of norms, so represented linear functionals are continuous.

[A1]

The Axiom of Choice: the selected density representatives in the score definition use the Axiom of Choice.

[A2]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): Countable Choice is assumed by the Hilbert projection and representer results in [F3], [F5], and [F7].

Proof

Given: The hypotheses above. Write $R = Π_{T_{η}} S_{θ}$ , so $S_{e f f} = S_{θ} - R$ .

1.1givenF1F5F6F7F8A1A2

By the orthogonal-projection definition in [F1] and [F7], $R \in T_{η}^{p}$ and each coordinate of $S_{e f f}$ is orthogonal to every element of $T_{η}$ by [F8]. Since $T_{η} \subseteq T$ , both $S_{θ}$ and $R$ belong to $T^{p}$ , hence $S_{e f f} \in T^{p}$ . The projection exists by the Hilbert and closed-subspace hypotheses [F5] and [F6] under [A2]; [A1] is carried through the selected score definition.

2.1givenF1F8step 1.1algebra

Because $S_{θ} = S_{e f f} + R$ and $R$ is nuisance-tangent-valued, orthogonality [F8] gives $E_{P} [S_{e f f} S_{θ}^{T}] = E_{P} [S_{e f f} S_{e f f}^{T}] = I_{e f f}$ . Therefore for every $a \in R^{p}$ and $t \in T_{η}$ , $E_{P} [S_{e f f} (a^{T} S_{θ} + t)] = I_{e f f} a$ .

3.1givenstep 2.1algebra

If $a^{T} S_{θ} + t = a^{' T} S_{θ} + t^{'}$ for $t, t^{'} \in T_{η}$ , step 2.1 applied to the difference gives $I_{e f f} (a - a^{'}) = 0$ . Nonsingularity forces $a = a^{'}$ , so the target derivative assigned to a score in the allowed score set is well-defined.

4.1givenstep 1.1step 2.1step 3.1F2F4F5F9

Set $ϕ = I_{e f f}^{- 1} S_{e f f}$ . For a score $s = a^{T} S_{θ} + t$ , step 2.1 gives $E_{P} [ϕ s] = a$ . Moreover $ϕ \in T^{p}$ by step 1.1 and [F4]. The map $s \mapsto E_{P} [ϕ s]$ is continuous in $L^{2} (P)$ by [F9], so it extends uniquely from the dense allowed score set to $T$ and agrees there with the path derivative. Thus $ϕ$ is a representer in the full tangent space.

5.1step 4.1F1F3algebra∎

By [F3], a representer in $T^{p}$ is the unique canonical gradient, so $ϕ_{c a n} = I_{e f f}^{- 1} S_{e f f}$ . The second-moment matrix $I_{e f f}$ is symmetric, hence so is its inverse. Direct multiplication gives $E_{P} [ϕ ϕ^{T}] = I_{e f f}^{- 1} I_{e f f} I_{e f f}^{- 1} = I_{e f f}^{- 1}$ . No existence of an estimator is used.

Depends on

Used by

A finite nuisance-score projection Example

Dependency tree · two levels

41 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

A. W. van der Vaart, Semiparametric Statistics, Lecture Notes in Mathematics 1781, Lectures 2–3 (Springer, 2002) (standard reference, not scraped)
Edward H. Kennedy, Semiparametric theory, arXiv:1709.06418v1 (2017) (standard reference, not scraped)