Moments of the sign pair U-statistic
Abstract
Independent signs with common mean have explicit first and second moments for their normalized pair statistic.
Definition 1.1 (Product weight of a sign vector).
Formalization. D5/S3/Estimation/DecisionRisk/SignPairUStatisticMoments.signPairWeight (✓ std3).
Source. Repository-derived.
Commentary.
Each coordinate assigns masses (1 + mu eta_i) / 2 to its two signs. The weight of a sign vector is the product of these coordinate masses.
Definition 1.2 (Normalized second-order sign statistic).
Formalization. D5/S3/Estimation/DecisionRisk/SignPairUStatisticMoments.signPairUStatistic (✓ std3).
Source. Repository-derived.
Commentary.
The statistic subtracts the diagonal contribution from the square of the sign sum and normalizes by the number of ordered distinct pairs.
Theorem 1.3 (Pair representation, mean, and variance).
Proof. Machine-checked in Lean as D5/S3/Estimation/DecisionRisk/SignPairUStatisticMoments.sign_pair_u_statistic_moments (✓ std3). ∎
Source. Repository-derived.
Commentary.
Expanding the square identifies the statistic with the average product over unordered coordinate pairs. Product factorization gives the expectation of every sign character as mu raised to the number of coordinates in that character.
For the second moment, equal pairs contribute the squared centered second moment. Pairs sharing one coordinate and disjoint pairs vanish after centering. Counting the surviving pairs and simplifying yields the stated variance.