Certified dominance at the origin for polynomial-rate shrinkage estimators of a normal mean
Abstract
Let X ∼ Nₚ(θ,Iₚ) be estimated under quadratic loss. Maruyama and Takemura build, from a positive non-decreasing function Φ, shrinkage estimators hat(θ)_φ that dominate the James–Stein estimator hat(θ)_JS provided they dominate it at the origin, i.e. provided Rdiff₀(hat(θ)_JS,hat(θ)_φ;p)=R(0,hat(θ)_JS)-R(0,hat(θ)_φ) ≥ 0. For their second example Φ₂(w;b,γ)=(w/b)^γ with b=1, γ=5 their Proposition 3.2 gives this for all p ≥ 8, and of the remaining dimensions they write only that "we numerically check that Rdiff₀(hat(θ)_JS,hat(θ)_φ;p_*) ≥ 0 for 3 ≤ p ≤ 7 individually"; no quadrature rule, error bound or range appears in the paper. We prove those five cells. We prove the same for b=1, C=1 at p=4,…,7, cell by cell, where the source instead propagates upward from p=3 by its Proposition 3.1. At p=3 we prove a two-sided rational bracket for the underlying integral, 1/300 ≤ I ≤ 1/50, so that the dominance there is strict and the risk gain at the origin lies between 1/(6√(2π))=0.0664… and 1/√(2π)=0.3989…, where the source prints only a table symbol. We also certify one entry the source marks as failing — at b=3, p=3 the risk difference is at most -1/20000 times an explicit positive constant — and the return to nonnegativity at p=4 in that same column. The method replaces floating-point quadrature by exact rational coverings: after the substitution w=u² the whole question is the sign of a one-variable integral of a rational function against the Gaussian weight, and fourteen finite rational computations bound it. The reduction, the soundness of the coverings, the alternating Taylor sandwich for exp and the Gaussian tail estimate are proved rather than computed. All statements are machine-checked in Lean 4; Section [sec:verif] records exactly what the kernel checks and what it does not.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
619a8e9481d1675c230f522b5e34f3daa2b0106fd35f6339b0b0af845d87bf9c
Claim ledger
Stated results
J1candidate2026-09-03
Rdiff₀(theta_JS, thetaₚhi; p) >= 0 at p = 3 for the source's Phi₂(w;b,gamma) = (w/b)ᵍamma with b = 1, gamma = 5, C = 1/(p-2) = 1 (Table 3 column b=1,gamma=5), certified by a 128-cell covering of mesh 1/64 on [0,2] of the reduced integral int₀ⁱnf (4uᵏ⁺¹⁰ - uᵏ)/(u¹⁰+c)² e^(-u²/2) du, (k,c) = (0,5)
J2candidate2026-09-03
Rdiff₀(theta_JS, thetaₚhi; p) >= 0 at p = 4 for the source's Phi₂(w;b,gamma) = (w/b)ᵍamma with b = 1, gamma = 5, C = 1/2 (Table 3 column b=1,gamma=5), certified by a 128-cell covering of mesh 1/64 on [0,2] of the reduced integral int₀ⁱnf (4uᵏ⁺¹⁰ - uᵏ)/(u¹⁰+c)² e^(-u²/2) du, (k,c) = (1,5/2)
J3candidate2026-09-03
Rdiff₀(theta_JS, thetaₚhi; p) >= 0 at p = 5 for the source's Phi₂(w;b,gamma) = (w/b)ᵍamma with b = 1, gamma = 5, C = 1/3 (Table 3 column b=1,gamma=5), certified by a 128-cell covering of mesh 1/64 on [0,2] of the reduced integral int₀ⁱnf (4uᵏ⁺¹⁰ - uᵏ)/(u¹⁰+c)² e^(-u²/2) du, (k,c) = (2,5/3)
J4candidate2026-09-03
Rdiff₀(theta_JS, thetaₚhi; p) >= 0 at p = 6 for the source's Phi₂(w;b,gamma) = (w/b)ᵍamma with b = 1, gamma = 5, C = 1/4 (Table 3 column b=1,gamma=5), certified by a 128-cell covering of mesh 1/64 on [0,2] of the reduced integral int₀ⁱnf (4uᵏ⁺¹⁰ - uᵏ)/(u¹⁰+c)² e^(-u²/2) du, (k,c) = (3,5/4)
J5candidate2026-09-03
Rdiff₀(theta_JS, thetaₚhi; p) >= 0 at p = 7 for the source's Phi₂(w;b,gamma) = (w/b)ᵍamma with b = 1, gamma = 5, C = 1/5 (Table 3 column b=1,gamma=5), certified by a 128-cell covering of mesh 1/64 on [0,2] of the reduced integral int₀ⁱnf (4uᵏ⁺¹⁰ - uᵏ)/(u¹⁰+c)² e^(-u²/2) du, (k,c) = (4,1) This p = 7 cell is the base case p_* = gamma + 2 = 7 from which the source's Proposition 2 gives every p >= 8.
J6candidate2026-09-03
Rdiff₀(theta_JS, thetaₚhi; p) >= 0 at p = 4 for Phi₂ with b = 1, gamma = 5 and C = 1 (the same column of the source's Table 2, where c = 5 for every p), same 128-cell covering
J7candidate2026-09-03
Rdiff₀(theta_JS, thetaₚhi; p) >= 0 at p = 5 for Phi₂ with b = 1, gamma = 5 and C = 1 (the same column of the source's Table 2, where c = 5 for every p), same 128-cell covering
J8candidate2026-09-03
Rdiff₀(theta_JS, thetaₚhi; p) >= 0 at p = 6 for Phi₂ with b = 1, gamma = 5 and C = 1 (the same column of the source's Table 2, where c = 5 for every p), same 128-cell covering
J9candidate2026-09-03
Rdiff₀(theta_JS, thetaₚhi; p) >= 0 at p = 7 for Phi₂ with b = 1, gamma = 5 and C = 1 (the same column of the source's Table 2, where c = 5 for every p), same 128-cell covering
J10candidate2026-09-03
Two-sided rational bracket at p = 3, b = 1, gamma = 5, C = 1: 1/300 <= int₀ⁱnf (4u¹0 - 1)/(u¹0+5)² e^(-u²/2) du <= 1/50, so the dominance is STRICT and the risk gain at the origin is pinned between two rationals (true value 0.00959648, i.e. Rdiff₀ = 0.19142)
J11candidate2026-09-03
Rdiff₀(theta_JS, thetaₚhi; 3) < 0 for Phi₂ with b = 3, gamma = 5, C = 1: perturbing the shrinkage constant destroys dominance in dimension 3. Certified by a 256-cell upper covering on [0,4] plus the explicit tail bound 4/T¹⁰ (sqrt(2 pi)/2 - gInt m T); the reduced integral is <= -1/20000 (true value -1.049e-4)
J12candidate2026-09-03
Rdiff₀(theta_JS, thetaₚhi; 4) >= 0 for Phi₂ with b = 3, gamma = 5, C = 1: the certified sign flip in the b = 3 column, one dimension above the negative cell J11 (192-cell covering on [0,3]; true value +3.086e-5)
J13routine2026-09-03
Non-vacuity control: the reduced integrand is strictly negative at u = 1/2, so the sign theorems are not pointwise trivialities – the answer is a cancellation (negative mass 0.02847 against positive mass 0.03807 at p = 3, a 25% margin)
J14routine2026-09-03
Hypothesis-non-vacuity control: the covering test itself FAILS at the b = 3, p = 3 cell (not 0 <= coverSum 0 243 1215 256), so '0 <= coverSum' is a real hypothesis and not an artefact of the construction
J15candidate2026-09-03
The same p = 3 cell stated in the source's OWN variable: 0 <= RdKernel 3 1 (1), where RdKernel p b C = int_((0,infty)) (4(w/b)⁵ - 1) w^(p/2-2) e^(-w/2) / (w⁵/(5b⁵)+C)² dw is Rdiff₀(...;p) times the positive constant 2^(p/2) Gamma(p/2)
J16candidate2026-09-03
The same p = 4 cell stated in the source's OWN variable: 0 <= RdKernel 4 1 (1/2), where RdKernel p b C = int_((0,infty)) (4(w/b)⁵ - 1) w^(p/2-2) e^(-w/2) / (w⁵/(5b⁵)+C)² dw is Rdiff₀(...;p) times the positive constant 2^(p/2) Gamma(p/2)
J17candidate2026-09-03
The same p = 5 cell stated in the source's OWN variable: 0 <= RdKernel 5 1 (1/3), where RdKernel p b C = int_((0,infty)) (4(w/b)⁵ - 1) w^(p/2-2) e^(-w/2) / (w⁵/(5b⁵)+C)² dw is Rdiff₀(...;p) times the positive constant 2^(p/2) Gamma(p/2)
J18candidate2026-09-03
The same p = 6 cell stated in the source's OWN variable: 0 <= RdKernel 6 1 (1/4), where RdKernel p b C = int_((0,infty)) (4(w/b)⁵ - 1) w^(p/2-2) e^(-w/2) / (w⁵/(5b⁵)+C)² dw is Rdiff₀(...;p) times the positive constant 2^(p/2) Gamma(p/2)
J19candidate2026-09-03
The same p = 7 cell stated in the source's OWN variable: 0 <= RdKernel 7 1 (1/5), where RdKernel p b C = int_((0,infty)) (4(w/b)⁵ - 1) w^(p/2-2) e^(-w/2) / (w⁵/(5b⁵)+C)² dw is Rdiff₀(...;p) times the positive constant 2^(p/2) Gamma(p/2)
J20candidate2026-09-03
RdKernel 3 3 1 < 0: the negative cell J11 stated in the source's own variable w
J21known2026-09-03
The reduction: RdKernel p b C = 50 b⁵ int_((0,infty)) (4uᵏ⁺¹⁰ - b⁵ uᵏ)/(u¹⁰+5Cb⁵)² e^(-u²/2) du for 3 <= p, k = p-3, b, C > 0 – the substitution w = u² that turns the source's fractional exponents into natural ones, proved from Mathlib's integral_compᵣpow_Ioiₒfₚos
Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- X Nₚ(θ, Iₚ), quadratic loss ‖θ̂ − θ‖², risk R(θ, θ̂) = E_θ‖θ̂(X) − θ‖². The James–Stein estimator is θ̂_JS(X) = (1 − (p−2)/‖X‖²) X and the general shrinkage class is θ̂_φ(X) = (1 − φ(‖X‖²)/‖X‖²) X.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7