Symmetric Binomial Chi-Square Defect

Abstract

The symmetric binomial mixture has an exact even-power chi-square defect, a hyperbolic-cosine envelope, and a root-fidelity bound.

Definition 1.1 (Symmetric binomial mixture).

$$\forall B:\mathbb{N},z:\mathbb{R},k:\mathbb{N},p_z(B,z,k)=\frac{1}{2}\cdot \mathrm{choose}(B,k)\cdot {\frac{1+z}{2}}^k\cdot {\frac{1-z}{2}}^{B-k}+{\frac{1-z}{2}}^k\cdot {\frac{1+z}{2}}^{B-k}.$$

Formalization. D5/S3/Estimation/ErrorExponents/SymmetricBinomialChiSquare.p_z (✓ std3).

Source. Repository-derived.

Commentary.

The law averages the binomial mass with success parameters (1+z)/2 and (1-z)/2. Exchanging the two parameters leaves the mixture unchanged.

Definition 1.2 (Central binomial reference law).

$$\forall B:\mathbb{N},k:\mathbb{N},p_0(B,k)=\frac{\mathrm{choose}(B,k)}{2^B}.$$

Formalization. D5/S3/Estimation/ErrorExponents/SymmetricBinomialChiSquare.p_0 (✓ std3).

Source. Repository-derived.

Commentary.

The reference law is the binomial distribution with success probability one half.

Definition 1.3 (Finite chi-square defect).

$$\forall B:\mathbb{N},z:\mathbb{R},\mathrm{chiSquare}(B,z)=\sum _{k\in \mathrm{range}(B+1)}\frac{{p_z(B,z,k)}^2}{p_0(B,k)}-1.$$

Formalization. D5/S3/Estimation/ErrorExponents/SymmetricBinomialChiSquare.chiSquare (✓ std3).

Source. Repository-derived.

Commentary.

The chi-square defect is the second likelihood-ratio moment under the central law, minus one.

Theorem 1.4 (Exact symmetric-binomial chi-square defect).

$$\begin{array}{r}\forall B:\mathbb{N},z:\mathbb{R},\\ |z|\le 1\Rightarrow [\\ (\forall k\in \mathrm{range}(B+1),0\le p_z(B,z,k))\wedge \\ \sum _{k\in \mathrm{range}(B+1)}{p}_z(B,z,k)=1\wedge \\ (\forall k:\mathbb{N},k\le B\Rightarrow \frac{p_z(B,z,k)}{p_0(B,k)}=\frac{{1+z}^k\cdot {1-z}^{B-k}+{1-z}^k\cdot {1+z}^{B-k}}{2})\wedge \\ \mathrm{chiSquare}(B,z)=\frac{{1+z^2}^B+{1-z^2}^B}{2}-1\wedge \\ \mathrm{chiSquare}(B,z)=\sum _{j\in \mathrm{Icc}(1,\frac{B}{2})}\mathrm{choose}(B,2\cdot j)\cdot z^{4\cdot j}\wedge \\ \mathrm{chiSquare}(B,z)\le \cosh (B\cdot z^2)-1\wedge \\ (\forall \delta :\mathbb{R},(0<\delta \wedge \delta \le \frac{1}{4}\wedge B\cdot \delta \le 1\wedge z^2=2\cdot \delta -{\delta }^2)\Rightarrow \mathrm{chiSquare}(B,z)\le 3\cdot {B\cdot \delta }^2)\wedge \\ (|z|<1\Rightarrow ((\forall k\in \mathrm{range}(B+1),0<p_z(B,z,k))\wedge 0<\mathrm{bhattacharyya}((k:\mathrm{Fin}(B+1))\mapsto p_0(B,k),(k:\mathrm{Fin}(B+1))\mapsto p_z(B,z,k))))\wedge \\ 1-{\mathrm{bhattacharyya}((k:\mathrm{Fin}(B+1))\mapsto p_0(B,k),(k:\mathrm{Fin}(B+1))\mapsto p_z(B,z,k))}^2\le \mathrm{chiSquare}(B,z)].\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/ErrorExponents/SymmetricBinomialChiSquare.symmetric_binomial_chi_square (✓ std3). ∎

Source. Repository-derived.

Commentary.

For absolute bias at most one, the symmetric mixture is nonnegative and normalized. Its likelihood ratio has the closed symmetric sign-product form. Its chi-square defect is both the average of two binomial powers minus one and the finite sum of its positive even terms.

The even terms are bounded by the corresponding hyperbolic-cosine series. For the quadratic parameterization z squared equals 2 delta minus delta squared, the small-argument series comparison gives a quadratic defect bound.

In the strict interior, every mixture mass and the Bhattacharyya affinity are positive. The squared affinity loss is no larger than the chi-square defect, by comparing the squared root likelihood-ratio gap with the squared likelihood-ratio gap.

References

• Truth anchor: D5/S3/Estimation/ErrorExponents/SymmetricBinomialChiSquare.chiSquare
• Truth anchor: D5/S3/Estimation/ErrorExponents/SymmetricBinomialChiSquare.p_0
• Truth anchor: D5/S3/Estimation/ErrorExponents/SymmetricBinomialChiSquare.p_z
• Truth anchor: D5/S3/Estimation/ErrorExponents/SymmetricBinomialChiSquare.symmetric_binomial_chi_square
• Dependency: D5/S3/TotalVariation/Hellinger