Statistics

Motivation

Bayesian filtering estimates an unobserved state from measurements arriving over time. A filter combines what the state dynamics predict with what the newest observation says. In neural decoding, for example, the state may describe an intended movement while the observation contains activity from many recorded neurons. The observation can have many more coordinates than the state and need not follow a linear Gaussian observation model.

The Discriminative Kalman Filter (DKF) uses a Gaussian approximation to the state conditional on the newest observation. It combines that approximation with a Gaussian state transition and a correction for the stationary state distribution. The resulting recursion retains a mean vector and covariance matrix. Burkhart et al. developed this construction and proved an asymptotic justification in Theorem 2 of Appendix B.

The historical starting point is the linear Gaussian filter of Kalman (1960). The 2020 DKF paper changes how observation information enters the update and establishes a corresponding approximation theorem. The present mission concerns formal verification of that published theorem.

Setting

The state space is $\mathbb R^d$ for a positive finite dimension $d$. Write $\eta_d(z;m,C)$ for the ordinary multivariate Gaussian density with mean $m$ and symmetric positive-definite covariance $C$. Densities and their $L^1$ distances are with respect to Lebesgue measure.

The state model has a matrix $A$ and positive-definite covariance matrices $\Gamma,S$ satisfying

$$S=ASA^\top+\Gamma.$$

Its stationary density and transition density are

$$p(z)=\eta_d(z;0,S),\qquad \tau(y,z)=\eta_d(z;Ay,\Gamma).$$

For an integrable density $s$, prediction gives

$$(\tau s)(z)=\int\tau(y,z)s(y)\,dy.$$

The discriminative update combines a previous filtering density $s$ with a density $u$ for the state given the current observation:

$$\frac{u\,\tau s/p}{\|u\,\tau s/p\|_1}.$$

This expression is a probability density when its nonnegative weight has a finite, strictly positive integral. Dividing by $p$ is part of the standard DKF under consideration.

For Gaussian inputs with parameters $(a,V)$ and $(b,U)$, define

$$G=AVA^\top+\Gamma,\qquad T=(U^{-1}+G^{-1}-S^{-1})^{-1},$$ $$c=T(U^{-1}b+G^{-1}Aa).$$

The DKF step returns mean $c$ and covariance $T$ when the precision is invertible and the covariance is positive definite. The recursive filter starts from mean zero and covariance $S$, using the current observation's functions $f$ and $Q$ as the Gaussian input mean and covariance. These are the updates in equation (2.7) of the paper.

Formalization targets

Fix sequences of probability densities $s_n,u_n$, indexed by positive integers, whose exact normalized updates

$$p_n=\frac{u_n\tau s_n/p}{\|u_n\tau s_n/p\|_1}$$

are well defined for every index. Fix Gaussian density sequences $s'_n,u'_n$, a point $b$, and a probability measure $P$. The five assumptions are

$$\begin{aligned} \mathrm{A1}:&\quad s_n\Rightarrow P,\\ \mathrm{A2}:&\quad \|s_n-s'_n\|_1\longrightarrow0,\\ \mathrm{A3}:&\quad u_n\Rightarrow\delta_b,\\ \mathrm{A4}:&\quad \|u_n-u'_n\|_1\longrightarrow0,\\ \mathrm{A5}:&\quad p_n\Rightarrow\delta_b. \end{aligned}$$

Here $\Rightarrow$ denotes weak convergence, characterized by convergence of expectations of every bounded continuous real function; $\delta_b$ is the unit point mass at $b$. The measure $P$ need not have a density and may be degenerate.

The main goal is the complete conjunction of Theorem 2's conclusions, with separate milestones for each:

• C1: $s'_n\Rightarrow P$.
• C2: $u'_n\Rightarrow\delta_b$.
• C3: the specific update

$$p'_n=\frac{u'_n\tau s'_n/p}{\|u'_n\tau s'_n/p\|_1}$$

is a well-defined Gaussian density for all sufficiently large $n$.

• C4: $p'_n\Rightarrow\delta_b$.
• C5: $\|p_n-p'_n\|_1\longrightarrow0$.

A sixth milestone is Lemma 1 (DKF equation): the normalized Gaussian-input update has the explicit mean and covariance above whenever valid, and the two input weak limits imply its eventual validity and convergence to $\delta_b$. It includes both the exact equation and the asymptotic assertion from the source.

Significance

In addition to neurodecoding with intracortical brain-computer interfaces, the DKF has also found applications in optimization and sequential data augmentation (see references). The original study was successfully reproduced by Casco-Rodriguez, et al. in ReScience C.

Difficulty

The inverse stationary density can grow in the tails, so small $L^1$ errors in the input densities do not immediately control the error after division and renormalization. Normalizing constants must remain finite and nonzero. The candidate Gaussian covariance must also become positive definite as a conclusion of the assumptions, rather than through an extra validity assumption imposed at every index.

There is a second distinction between convergence to a point mass and approximation in $L^1$. Two sequences may concentrate at the same point while retaining different shapes at shrinking scales. The C5 target therefore requires the full approximation argument, beyond the weak-convergence conclusions.

Formalization scope

Lean represents states as Fin d → ℝ and covariance matrices as real square matrices. The Gaussian density is the standard determinant-and-quadratic-form formula. The definition of Gaussian PDF includes positive-definite covariance and equality of densities almost everywhere. Thus null-set changes do not constrain the theorem artificially.

Probability density validity explicitly includes nonnegativity almost everywhere, integrability and total integral one. The $L^1$ quantity is an extended nonnegative integral. The update's validity explicitly requires measurable weight and a finite, strictly positive normalizer. Total expressions outside that domain supply no assumed probability interpretation; C3 establishes validity on a tail.

All density sequences use positive integer indices. The limit measure is a Mathlib probability measure. Weak convergence is tested against Mathlib bounded continuous functions using the actual measures generated by the densities. The stationary model, standard recursive DKF, exact update and approximate update are defined independently of the theorem conclusions.

The mission addresses deterministic Theorem 2 of Appendix B. The random-sequence extension in Remark 4, conditions implying a Bernstein–von Mises theorem, and induction over filtering time are separate developments. The proof plan follows the appendix through C1–C2, Lemma 1, C3–C4, and the five-term comparison for C5.

Selected references

• M. C. Burkhart, D. M. Brandman, B. Franco, L. R. Hochberg and M. T. Harrison, The Discriminative Kalman Filter for Bayesian Filtering with Nonlinear and Nongaussian Observation Models, Neural Computation 32(5), 969–1017, 2020. DOI: 10.1162/neco_a_01275.
• R. E. Kalman, A New Approach to Linear Filtering and Prediction Problems, Journal of Basic Engineering 82(1), 35–45, 1960. DOI: 10.1115/1.3662552.
• M. C. Burkhart, A Discriminative Approach to Bayesian Filtering with Applications to Human Neural Decoding, Ph.D. dissertation, Brown University, 2019. DOI: 10.26300/nhfp-xv22.
• D. M. Brandman, M. C. Burkhart, J. Kelemen, B. Franco, M. T. Harrison and L. R. Hochberg, Robust Closed-Loop Control of a Cursor in a Person with Tetraplegia using Gaussian Process Regression, Neural Computation 30(11), 2986–3008, 2018. DOI: 10.1162/neco_a_01129.
• D. M. Brandman, T. Hosman, J. Saab, M. C. Burkhart, B. E. Shanahan, J. G. Ciancibello et al., Rapid calibration of an intracortical brain–computer interface for people with tetraplegia, Journal of Neural Engineering 15(2), 026007, 2018. DOI: 10.1088/1741-2552/aa9ee7.
• J. Casco-Rodriguez, C. Kemere and R. G. Baraniuk, [Re] The Discriminative Kalman Filter for Bayesian Filtering with Nonlinear and Non-Gaussian Observation Models, ReScience C 10(1), article 3, 2025. DOI: 10.5281/zenodo.15172014, published PDF.
• M. C. Burkhart, Discriminative Bayesian filtering lends momentum to the stochastic Newton method for minimizing log-convex functions, Optimization Letters 17, 657–673, 2023. DOI: 10.1007/s11590-022-01895-5.

Motivation

A foundation model trained on tokenized electronic health record (EHR) timelines can be used to predict clinical outcomes without ever being finetuned for a specific prediction task: condition the model on a patient's observed timeline, autoregressively sample many possible futures, and report the fraction of sampled futures in which the outcome of interest occurs. This generative approach to inference powers a growing family of EHR foundation models— including Event Stream GPT (McDermott et al., 2023), Foresight (Kraljevic et al., 2024), ETHOS (Renc et al., 2024), and Curiosity (Waxler et al., 2025)—and it is attractive for its zero-shot approach to predicting a variety of outcomes.

It is also expensive. Reproducing one published pipeline required more than $1500$ A100 GPU-hours of inference. Worse, the estimator built from $n$ sampled futures takes values in $\{0, 1/n, \dots, 1\}$, so its resolution is tied to the sampling budget: for an outcome of prevalence $1/10{,}000$, $100$ sampled futures fail more than $90\%$ of the time to rank a patient at ten times average risk above an average one. The most consequential clinical decisions turn on exactly such low-prevalence, high-impact outcomes.

Solo et al. (arXiv:2602.03730) observe that Monte Carlo discards almost everything the model produces: at every step the model emits a full next-token distribution and the sampler keeps only the token it drew. The paper introduces two estimators that consume the discarded probabilities instead, and proves that doing so costs no bias and—for one of them—never costs variance.

Setting and estimators

Let $P$ generate token sequences from a countable vocabulary $V$, with designated outcome token $O$. The next-token probabilities may depend on the complete preceding history. The time threshold is initially unexceeded. Its crossing may depend on several kinds of time-spacing tokens and on their accumulated duration.

For a sampled timeline $X$, $T_O(X)$ is the first position occupied by $O$, or $\infty$ if it never appears. The time $T_E(X)$ is the first position at which the threshold has been exceeded. Assume $T_O\ne T_E$ almost surely. Timelines are retained through the actual threshold crossing, even if the outcome appears earlier. Thus $T_E$ is not reassigned after an outcome.

The threshold is reached almost surely, but the number of tokens required may be arbitrarily large. No deterministic bound or finite expected token count is assumed. For REACH, assume also that removing the outcome token and renormalizing defines a sampler that reaches the same threshold almost surely.

For $n\ge1$ independent original timelines, the Monte Carlo estimator is

$$M_0=\frac1n\sum_{i=1}^n 1_{\{T_O(X^{(i)})<T_E(X^{(i)})\}}.$$

The SCOPE estimator is

$$\mathcal S=\frac1n\sum_{i=1}^n\sum_{t=1}^{\min\{T_E(X^{(i)}),T_O(X^{(i)})\}}P(X_t=O\mid X_{1:t-1}^{(i)}).$$

For REACH, sample independent outcome-free timelines by setting the next-token probability of $O$ to zero and renormalizing the probabilities of the other tokens. Using the original model probabilities along those timelines, define

$$\mathcal R=\frac1n\sum_{i=1}^n\left[1-\prod_{t=1}^{T_E(\hat X^{(i)})}\left(1-P(X_t=O\mid\hat X_{1:t-1}^{(i)})\right)\right].$$

Formalization targets

The targets are:

1. SCOPE unbiasedness: $\mathbb E[\mathcal S]=P(T_O<T_E)$.
2. Equal probabilities milestone: $P(A)=P(B)$ from Appendix C, where $A$ is the original outcome-before-threshold event and $B$ is at least one successful Bernoulli trial along an outcome-free timeline.
3. REACH unbiasedness: $\mathbb E[\mathcal R]=P(T_O<T_E)$.
4. Rao–Blackwell identity: for every positive sample count, conditioning the average of the two-stage event indicators on the entire pool of outcome-free timelines equals $\mathcal R$ almost surely.
5. Main goal: $\operatorname{Var}(\mathcal R)\le\operatorname{Var}(M_0)$ at the same positive sample count, with finite second moments for both estimators.

Expectations and variances use each estimator's specified sampling law.

What the formalization establishes

The claims concern the probability assigned by the generative model. They provide unbiasedness and a comparison of sampling variance. SCOPE is kept unclipped, as in the paper's unbiasedness result. All five target statements have accompanying local Lean proofs.

Main mathematical difficulty

A pathwise finite stopping time need not have a common finite bound or a finite mean. An expectation involving the stopped SCOPE sum therefore needs justification beyond finite-sum linearity. REACH uses a different sampling law, so its unbiasedness and variance comparison also require a proved connection between the original event and the two-stage experiment. The equal-probabilities milestone records that connection explicitly.

Formalization scope

Lean represents each sampled timeline by a finite list ending at its first threshold crossing. Arbitrary finite lengths are included in the same sample space. Path probabilities are products of next-token probabilities, and the laws are countable sums of these path masses. Requiring each law to have total mass one expresses almost-sure termination of that sampler; it is not a uniform length bound. The vocabulary can be finite or countably infinite.

The stopping predicate examines a complete prefix and is not restricted to a single terminal token. The original law continues through outcomes until the threshold. A separate almost-everywhere hypothesis excludes equal outcome and threshold times. The code proves that the actual threshold time is finite almost surely and that the strict event $T_O<T_E$ is the event used by the internal calculations.

The two-stage experiment explicitly samples conditionally independent Bernoulli trials using the original hazards. Its conditioning information retains the complete indexed pool of outcome-free timelines. The Rao–Blackwell target uses Mathlib's conditional expectation. The variance target uses Mathlib's variance, and proves square integrability rather than assuming it.

Selected references

• Luke Solo, Matthew B. A. McDermott, William F. Parker, Bashar Ramadan, Michael C. Burkhart, Brett K. Beaulieu-Jones, Efficient Generative Prediction for EHR Foundation Models: The SCOPE and REACH Estimators, 2026. arXiv:2602.03730
• M. B. A. McDermott, B. Nestor, P. Argaw, I. S. Kohane, Event Stream GPT: A Data Pre-processing and Modeling Library for Generative, Pre-trained Transformers over Continuous-time Sequences of Complex Events, Advances in Neural Information Processing Systems 36, pp. 24322–24334, 2023. arXiv:2306.11547
• Z. Kraljevic, D. Bean, A. Shek, R. Bendayan, H. Hemingway, J. A. Yeung, A. Deng, A. Baston, J. Ross, E. Idowu, J. T. Teo, R. J. B. Dobson, Foresight—a generative pretrained transformer for modelling of patient timelines using electronic health records: a retrospective modelling study, Lancet Digital Health 6(4), pp. e281–e290, 2024. doi:10.1016/S2589-7500(24)00025-6
• P. Renc, Y. Jia, A. E. Samir, J. Was, Q. Li, D. W. Bates, A. Sitek, Zero shot health trajectory prediction using transformer, npj Digital Medicine 7(1), p. 256, 2024. doi:10.1038/s41746-024-01235-0
• S. Waxler, P. Blazek, D. White, D. Sneider, K. Chung, M. Nagarathnam, P. Williams, H. Voeller, K. Wong, M. Swanhorst, S. Zhang, N. Usuyama, C. Wong, T. Naumann, H. Poon, A. Loza, D. Meeker, S. Hain, R. Shah, Generative medical event models improve with scale, 2025. Introduces the Curiosity model family. arXiv:2508.12104

The problem

(a) In a tennis match, you are the favorite, and win each point independently with probability $q\in(1/2,1)$. Let $n,m$ be odd positive integers greater than $1$. You have the choice between playing a best-of-$nm$ (i.e., you play $nm$ points and whoever wins the majority of points wins the match), or a best-of-$n$ of best-of-$m$'s (i.e., the match is won by winning the majority of $n$ "sets", and each "set" is won by winning the majority of $m$ points). Prove that your probability of winning the match is strictly greater by playing the best-of-$nm$.

(b) We now consider two generalizations: $m_1,\ldots,m_k$ are odd positive integers, while $n$ is any positive integer, with all integers being greater than $1$. You have the choice between playing a best-of-$nm_1\cdots m_k$, or a best-of-$n$ of "sets", which are best-of-$m_1$'s of "games", …, which are best-of-$m_k$'s of "points". In both cases, now that $n$ may be even, it is possible for the players to tie, in which case the match winner is determined by an independent fair coin. Prove again that your probability of winning the match is strictly greater by playing the best-of-$nm_1\cdots m_k$.

(c) We consider a further generalization where each completed "set" counts toward the match score in an independently random way:

• with probability $a$, the winner gains $1$ in the match score, as usual;
• with probability $b$, the set is ignored and does not count toward the match score;
• with probability $c$, the loser gains $1$ in the match score;

with $a+b+c=1$ and $a>c$, so players are still incentivized to win sets (previously we had $a=1$, $b=c=0$). This random scoring rule is applied once per completed set, at the outermost layer only: the games and points inside a set are decided by plain majorities, with no randomness, and only the set's final result is scored. If you choose to play the best-of-$nm_1\cdots m_k$, then each individual point counts as a set and is subject to the same randomness with probabilities $a,b,c$. Prove that your probability of winning the match is still strictly greater by playing the best-of-$nm_1\cdots m_k$ (the fair-coin-on-ties convention continues).

(d) Continue from part (c), but change the fair-coin-on-ties convention so that you only win the match if you have a strictly greater match score than your opponent. Assuming $b\ge1/2$, prove that your probability of winning the match is strictly greater by playing the best-of-$nm_1\cdots m_k$.

Source and connection to Dorner–Hardt

Florian E. Dorner and Moritz Hardt, Don't Label Twice: Quantity Beats Quality when Comparing Binary Classifiers on a Budget, ICML 2024. arXiv:2402.02249 (v3, 8 April 2026).

The paper asks how to spend a fixed budget of noisy crowdworker labels when comparing two binary classifiers: one label each for many data points, or several labels per data point aggregated by majority vote. It proves, via Cramér's theorem, that one label each is asymptotically optimal, and states the finite-sample version as an open conjecture (Section 5, Conjecture 1), still open in the April 2026 revision. Its Section 3 displays the finite-sample inequality for the independent, homogeneous-label case and verifies it numerically over about five billion parameter settings.

Part (d) of this mission with one level of sets is that Section 3 inequality in tennis language. A point is a single crowdworker label being correct ($q$ is the label accuracy); a set is a data point, whose test label is the majority of its $m$ labels; and the scoring rule is what the two classifiers do with that label. Writing $p$ for the worse classifier's accuracy and $p+\epsilon$ for the better one's, a set is scored to its winner when the better classifier alone matches the test label, ignored when the two classifiers agree, and scored to its loser when the worse classifier alone matches:

$$a=(p+\epsilon)(1-p),\qquad c=p(1-p-\epsilon),\qquad b=1-a-c,$$

so that $a-c=\epsilon>0$, and $b\ge1/2$ always holds because two classifiers of accuracy at least $1/2$ agree on at least half the data. Substituting into the paper's Proposition 1 recovers its gap-indicator probabilities exactly: $\Pr(+1)=q\epsilon+p(1-p-\epsilon)$, $\Pr(-1)=(1-q)\epsilon+p(1-p-\epsilon)$. The paper's inequality also allows $n=1$ and $q=1$, which parts (c)–(d) exclude only because the inequality can fail to be strict at $b=0$ there; for $b\ge1/2$ the same argument covers those edge cases. The paper's Conjecture 1 as literally stated concerns a correlated-error setting (its Section 3.2) and is not claimed here.

Parts (a)–(c) go beyond the paper's setting: arbitrary nesting depth, a fair-coin tie rule, and no constraint on the ignore rate $b$. The hypothesis $b\ge1/2$ in part (d) cannot be dropped: with one level, $(a,b,c)=(0.9,0.1,0)$, $q=0.6$, $m=3$, $n=1$, the single best-of-3 finishes strictly ahead with probability $0.5832$ while three single points do so with probability $0.5761$.

Timeline

• Feb 2024 — arXiv v1; ICML 2024. Asymptotic theorem via Cramér; finite-sample statement conjectured; ~5·10⁹-configuration numerical sweep.
• Oct 2024 — arXiv v2.
• Apr 2026 — arXiv v3; conjecture still stated as open.
• Aug 2026 — private proof of the Section 3 inequality (strict win, $b\ge1/2$, one level) via exponential tilting of the tie probability.
• Sep 2026 — private proof of the fair-coin version with no constraint on $b$ (Bernstein degree elevation and a hypergeometric parity argument), then of the full four-part statement via a pairing lemma for player-symmetric rules. This mission formalizes that proof.

Conventions in the formal statement

"Greater than $1$" is read as $n\ge2$ and each $m_i\ge3$ odd; the list of set sizes in (b)–(d) is nonempty. Laws are functions $\mathbb Z\to\mathbb R$ and every probability is a finite sum — no measure theory. The goal theorem is the conjunction of the four parts.

Motivation

Chapter 4 of Luenberger's Optimization by Vector Space Methods (Wiley, 1969) develops linear least-squares estimation as an application of the Hilbert space projection theorem formalized in Mission I of this series. The chapter's centerpiece is the classical Gauss–Markov theorem: among all linear unbiased estimators of an unknown parameter vector from noisy linear measurements, the estimator $(W^\top Q^{-1} W)^{-1} W^\top Q^{-1} y$ has minimum variance — componentwise, not merely in trace. This result is foundational for statistics and econometrics, and its Hilbert-space derivation is the cleanest known.

Setting

Measurements are modeled as $y = W\beta + \varepsilon$, where $y$ is an $m$-dimensional data vector, $W$ a known $m \times n$ matrix ($n < m$) with linearly independent columns, $\beta$ an unknown $n$-dimensional parameter vector, and $\varepsilon$ a random $m$-vector of measurement errors with $E\varepsilon = 0$ and covariance $E[\varepsilon\varepsilon^\top] = Q$, positive definite. A linear estimate is $\hat\beta = Ky$ for a constant $n \times m$ matrix $K$; it is unbiased when $E\hat\beta = \beta$ for every $\beta$, which holds iff $KW = I$. The optimality criterion is the error second moment $E\|\hat\beta - \beta\|^2$, and the book's key observation (p. 85) is that the problem splits into $n$ independent minimum norm problems, one per component, each solvable by the dual approximation theorem of Mission I.

Formally, randomness is carried by an abstract probability space: a measure space $(\Omega, \mu)$ with $\mu$ a probability measure, random vectors as functions $\Omega \to \mathbb{R}^m$ with explicit integrability hypotheses for all first and second moments, and $E[\cdot] = \int \cdot \, d\mu$.

Formalization targets

The goal is §4.4 Theorem 1 (Gauss–Markov): with $K_0 = (W^\top Q^{-1} W)^{-1} W^\top Q^{-1}$,

$$K_0 W = I, \qquad E\big[(K_0 y - \beta)_i^2\big] \le E\big[(K y - \beta)_i^2\big] \quad \text{for every } i \text{ and every } K \text{ with } KW = I,$$

with error covariance

$$E\big[(K_0 y - \beta)(K_0 y - \beta)^\top\big] = (W^\top Q^{-1} W)^{-1}.$$

Milestones: the deterministic least-squares estimate $\hat\beta = (W^\top W)^{-1} W^\top y$ (§4.3 Theorem 1); the book's deterministic reduction — minimize the diagonal entries of $KQK^\top$ subject to $KW = I$ (p. 85); the minimum-variance estimate $\hat\beta = E[\beta y^\top] (E[y y^\top])^{-1} y$ for random $\beta$ (§4.5 Theorem 1); and the information-form identities $RW^\top(WRW^\top + Q)^{-1} = (W^\top Q^{-1}W + R^{-1})^{-1}W^\top Q^{-1}$ and $R - RW^\top(WRW^\top+Q)^{-1}WR = (W^\top Q^{-1}W + R^{-1})^{-1}$ (§4.5 Corollary 2).

Significance

The Gauss–Markov theorem justifies weighted least squares as the optimal linear unbiased procedure and is the standard benchmark against which biased and nonlinear estimators are measured. The minimum-variance estimate of §4.5 is the Bayesian counterpart with prior covariance $R$; the information-form identities connect the two and exhibit Gauss–Markov as the limit $R^{-1} \to 0$. Mission III builds the recursive (Kalman) estimator directly on these results.

All results are classical and proved in the source. Mathlib has mature measure-theoretic integration but, to date, no Gauss–Markov theorem and no linear estimation theory; the matrix milestones (trace reduction, information form) are also absent as stated. The probabilistic statements here are deliberately phrased with elementary integrals of products of real-valued components — no Bochner integration of vector-valued maps — so they are approachable with MeasureTheory.integral alone.

Difficulty

The subtlety is bookkeeping, not depth. Unbiasedness must be encoded as the algebraic constraint $KW = I$ (the book proves the equivalence with $E\hat\beta = \beta$ for all $\beta$); the componentwise variance claim is strictly stronger than the trace claim and requires the per-component minimum norm argument, not a single matrix inequality. Positive definiteness of $Q$ enters through invertibility of $W^\top Q^{-1} W$, which itself needs the linear independence of the columns of $W$ — dropping either hypothesis makes the goal false. In the probabilistic statements every integral needs an integrability hypothesis; the drafts supply integrability of all pairwise products of components, from which integrability of every derived expression follows.

Formalization scope

Random vectors are plain functions Ω → Fin m → ℝ on a MeasurableSpace Ω with a probability measure μ; second moments are hypotheses of the form ∫ ω, ε ω i * ε ω j ∂μ = Q i j with explicit Integrable assumptions; no independence, Gaussianity, or distributional assumptions are used anywhere. Matrices are Matrix (Fin m) (Fin n) ℝ with Mathlib's Matrix.PosDef, nonconstructive inverse ⁻¹, and mulVec. Norms on parameter space are written as explicit finite sums of squares, avoiding any ambiguity between Euclidean and supremum norms on pi types. The estimators under comparison are strictly linear ($\hat\beta = Ky$, no affine offset), exactly as in the source; §4.5's affine extension (its Problem 6) is out of scope.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969. Chapter 4, pp. 78–102. ISBN 0-471-55359-X.
• A. C. Aitken, On least squares and linear combination of observations, Proc. Roy. Soc. Edinburgh 55 (1935), 42–48 (the weighted-least-squares form of Gauss–Markov).