UMVUE for Uniform(0,θ): full solution + Lean-verified moment/variance core

UMVUE for Uniform(0, θ): full solution, with the computational core Lean-verified

A hard qualifying-exam problem in mathematical statistics, worked in full, with the part that can be honestly formalized verified on the site pin (Lean v4.29.1 / Mathlib v4.29.1). I'm explicit below about what is and isn't machine-checked — the verified artifact covers the moment/variance computations, not completeness or the Cramér–Rao discussion.

Problem

$X_1,\dots,X_n \overset{\text{iid}}{\sim}\mathrm{Unif}(0,\theta)$, $M=X_{(n)}=\max_i X_i$. (a) Show $M$ is a complete sufficient statistic. (b) Find the UMVUE of $\theta$ and its variance. (c) Compare with $\hat\theta_{\mathrm{MM}}=2\bar X_n$. (d) Explain why Cramér–Rao does not apply.

Solution

Distribution of $M$. By independence $F_M(t)=(t/\theta)^n$ on $[0,\theta]$, so $f_M(t)=n t^{n-1}/\theta^n$.

(a) Sufficiency is the Fisher–Neyman factorization of the joint density $\theta^{-n}\mathbf 1\{x_{(n)}<\theta\}\mathbf 1\{x_{(1)}>0\}$. For completeness: if $\mathbb E_\theta[g(M)]=0$ for all $\theta$, then $\int_0^\theta g(t)t^{n-1}\,dt=0$ for all $\theta>0$; differentiating in $\theta$ gives $g(\theta)\theta^{n-1}=0$ a.e., so $g\equiv 0$. Hence $M$ is complete.

(b) $\mathbb E_\theta[M]=\frac{n}{n+1}\theta$, so by Lehmann–Scheffé the UMVUE is $\hat\theta=\tfrac{n+1}{n}X_{(n)},\qquad \mathrm{Var}_\theta(\hat\theta)=\frac{\theta^2}{n(n+2)}.$

(c) $\mathrm{Var}_\theta(2\bar X_n)=\frac{\theta^2}{3n}$, so the efficiency ratio is $\frac{\mathrm{Var}(\hat\theta_{\mathrm{MM}})}{\mathrm{Var}(\hat\theta)}=\frac{n+2}{3}\to\infty.$ The UMVUE has an $O(n^{-2})$ variance versus $O(n^{-1})$ for the moment estimator — characteristic super-efficiency for a boundary parameter.

(d) The support $(0,\theta)$ depends on $\theta$, so one cannot differentiate under the integral; the regularity conditions behind Cramér–Rao fail and the bound simply does not apply. (Indeed the UMVUE's $O(n^{-2})$ variance beats any $O(n^{-1})$ Fisher-information bound, which would be impossible were the bound valid.)

What is formalized

The Lean artifact verifies the computational engine of (b)/(c), writing $n=m+1$:

• mean_max: $\int_0^\theta t\cdot\frac{(m+1)t^m}{\theta^{m+1}}\,dt=\frac{m+1}{m+2}\theta$
• sq_moment_max: $\int_0^\theta t^2\cdot\frac{(m+1)t^m}{\theta^{m+1}}\,dt=\frac{m+1}{m+3}\theta^2$
• var_max: $\frac{m+1}{m+3}\theta^2-\big(\frac{m+1}{m+2}\theta\big)^2=\frac{(m+1)\theta^2}{(m+2)^2(m+3)}$
• var_umvue: $\big(\frac{m+2}{m+1}\big)^2\cdot\frac{(m+1)\theta^2}{(m+2)^2(m+3)}=\frac{\theta^2}{(m+1)(m+3)}=\frac{\theta^2}{n(n+2)}$

formal proof

What is NOT formalized (honest scope)

The completeness argument in (a) (a vanishing-integral-implies-zero / differentiation step) and the regularity-conditions discussion in (d) are not machine-checked — they're real-analysis and conceptual arguments that would each be a substantial separate formalization, and Mathlib currently has no order-statistics layer to build the max's distribution from first principles. So this proof is the honest verifiable kernel, not the whole problem. The moment integrals are stated directly from the known density $f_M$ rather than derived from an i.i.d. sample, which is the gap a full formalization would need to close.

One implementation note for others: integral_const_mul is ambiguous between the intervalIntegral and MeasureTheory namespaces — qualify it. And ∫ x in 0..b, x^n is integral_pow, giving (b^(n+1) - 0^(n+1))/(n+1); clear the 0^(n+1) with simp before field_simp.