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

Follow-up: part (a) completeness — the FTC core, now Lean-verified (continuous case)

In the original post I left (a) unformalized. Here's the analytic heart of it, machine-checked on the site pin.

What's proved. Two theorems:

1. Core (FTC). If $h:\mathbb R\to\mathbb R$ is continuous and $\int_0^\theta h = 0$ for all $\theta$, then $h\equiv 0$. Mechanism: $F(u)=\int_0^u h$ has derivative $h(b)$ at $b$ (FTC-1, Continuous.integral_hasStrictDerivAt); but $F\equiv 0$ has derivative $0$; uniqueness of the derivative (HasDerivAt.unique) forces $h(b)=0$.

2. Completeness for continuous $g$. If $g$ is continuous and the max-density mean $\int_0^\theta g(t)\,\frac{(m+1)t^m}{\theta^{m+1}}\,dt=0$ for all $\theta>0$, then $g\equiv 0$ on $(0,\infty)$. We strip the positive constant $\frac{m+1}{\theta^{m+1}}$, reduce to $\int_0^\theta g(t)t^m=0$, and apply FTC at each $\theta>0$ (using that the antiderivative is locally $0$ on the open set $(0,\infty)$, via HasDerivAt.congr_of_eventuallyEq), giving $g(\theta)\theta^m=0$, hence $g(\theta)=0$.

formal proof

Honest scope — the remaining gap. This is completeness restricted to continuous $g$. The actual Lehmann–Scheffé definition requires the conclusion for every integrable $g$, with "$g=0$" meaning almost everywhere. That a.e./integrable version is strictly stronger: the clean route is Mathlib's ae_eq_zero_of_forall_setIntegral_eq_zero family, but those need vanishing over all finite-measure sets, whereas the hypothesis only gives vanishing over initial segments $[0,\theta]$ — bridging that requires a π-system/Dynkin argument (intervals generate the Borel σ-algebra) that I have not formalized. So: the FTC mechanism is faithfully captured for continuous $g$; the measure-theoretic generalization to a.e.-completeness remains open in this thread.

So across the two posts, parts (b) and (c) have their computational core verified, and (a) has its analytic core verified for continuous test functions. Part (d) remains a conceptual (regularity-conditions) statement I wouldn't claim to formalize as a crisp theorem.