3.1. The classical definition🔗

The most common definition of QMD uses a Euclidean parameter set. We start here to fix intuition, then relax the parameter space below.

Let \Theta \subseteq \mathbb{R}^k and let \mu dominate the family. The family \mathcal{P}(\Theta) is QMD at an interior point \theta^\star if there exists a score h \in L^2(\mathbb{P}_{\theta^\star}) such that

\left\| \frac{p_{\theta^\star + t}^{1/2} - p_{\theta^\star}^{1/2}}{\|t\|} - \tfrac{1}{2}\, h\, p_{\theta^\star}^{1/2} \right\|_{L^2(\mu)} \longrightarrow 0,

as \|t\| \to 0. The function h is the score at \theta^\star.

A cornerstone result is that the score has mean zero under \mathbb{P}_{\theta^\star}. Inspecting its proof shows that one can weaken both the parameter space and the notion of differentiability and still reach the conclusion.

3.2. QMD over a normed space🔗

The first generalization replaces \mathbb{R}^k by a normed vector space E. Let \Theta \subseteq E, let \mu be \sigma-finite, and assume \mathbb{P}_\theta \ll \mu for all \theta \in \Theta. The family is QMD at an interior point \theta^\star with a bounded linear score A_{\theta^\star} : E \to L^2(\mathbb{P}_{\theta^\star}) if

\left\| \sqrt{p_{\theta^\star + h}} - \sqrt{p_{\theta^\star}} - \tfrac{1}{2}\, A_{\theta^\star}(h)\, \sqrt{p_{\theta^\star}} \right\|_{L^2(\mu)} = o(\|h\|_E).

The main result of interest at this level of generality is the mean-zero score property: if \mathcal{P}(\Theta) is QMD at an interior point \theta^\star with score A_{\theta^\star}, then \mathbb{E}_{\mathbb{P}_{\theta^\star}}\!\big(A_{\theta^\star}(h)\big) = 0 for every h \in E.

However, the notion of differentiability can be weakened further to achieve this.

3.3. Hadamard QMD over a topological vector space🔗

The mean-zero-score conclusion survives an even weaker hypothesis: E may be a topological vector space, and differentiability may be tested only along local paths. This Hadamard formulation is what the Lean development uses, because it is both weaker than the classical condition and easier to work with.

The family is Hadamard QMD (H.Q.M.D.) at an interior point \theta^\star with linear score A_{\theta^\star} if, whenever t \to 0, a_t \to h in E, and \theta^\star + t\,a_t \in \Theta eventually,

\frac{1}{t}\left\| \sqrt{p_{\theta^\star + t a_t}} - \sqrt{p_{\theta^\star}} - \tfrac{1}{2}\, A_{\theta^\star}(t h)\, \sqrt{p_{\theta^\star}} \right\|_{L^2(\mu)} \longrightarrow 0.

In Lean the local path is encoded by a filter l on \mathbb{R} \times E whose first coordinate tends to 0 and whose second coordinate tends to h, with the path eventually staying in \Theta.

The Hadamard notion is genuinely weaker: a quadratic mean derivative within a set is always a Hadamard QMD derivative.

3.4. The mean-zero score theorem🔗

The central result, formalized as integral_score_eq_zero, is the following.

Theorem (Mean-zero score). Let \mathcal{P}(\Theta) = \{\mathbb{P}_\theta\}_{\theta \in \Theta}

be a class of probability measures on a measurable space (\Omega,\mathcal{A}), where

\Theta \subseteq E for a topological vector space E and \mu is a \sigma-finite

measure satisfying \mathbb{P}_\theta \ll \mu for all \theta \in \Theta. Suppose that

\mathcal{P}(\Theta) is Hadamard quadratic mean differentiable at an interior point

\theta^\star \in \Theta with score A_{\theta^\star} : E \to L^2(\mathbb{P}_{\theta^\star}).

Then

\mathbb{E}_{\mathbb{P}_{\theta^\star}}\!\big(A_{\theta^\star}(h)\big) = 0 \qquad \text{for all } h \in E.