Bhattacharyya Affinity and the Bretagnolle–Huber Bound

Abstract

Finite Bhattacharyya affinity links total variation and relative entropy through the complementary Bretagnolle–Huber bound.

Definition 1.1 (Finite Bhattacharyya affinity is the square-root product sum).

$$\begin{array}{c}\forall \iota [\mathrm{Fintype}(\iota )],\\ \forall p,q:\iota \to \mathbb{R},\\ \mathrm{BC}(p,q):=\sum _i\sqrt{p(i)q(i)}.\end{array}$$

Formalization. D5/S3/TotalVariation/Bhattacharyya.bhattacharyya (✓ std3).

Source. Repository-derived.

Commentary.

For finite real mass functions p and q, the Bhattacharyya coefficient, also called their Hellinger affinity, is the sum of the square roots of the coordinatewise products. The definition itself imposes no sign or normalization hypotheses; the probability assumptions enter the identities and inequalities below.

This coefficient is the intermediate quantity that connects total variation to relative entropy. It also provides the natural intermediate for future comparisons with Hellinger distance and Renyi divergence, without defining either notion in the present module.

Theorem 1.2 (Normalized nonnegative mass has self-affinity one).

$$\begin{array}{c}\forall \iota [\mathrm{Fintype}(\iota )],\\ \forall p:\iota \to \mathbb{R},\\ ((\forall i,0\le p(i))\wedge \sum _{i}p(i)=1)\Rightarrow \\ \mathrm{BC}(p,p)=1.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/TotalVariation/Bhattacharyya.bhattacharyya_self (✓ std3). ∎

Source. Repository-derived.

Commentary.

A new definition must be pinned by identities: inequalities alone do not certify what has been defined. Self-affinity is the first pin. It rules out dropping the square root, because the resulting sum of p(i)^2 is 1/2 for the uniform law on Bool. It also rules out replacing the product by a sum, which gives sqrt(2) on a Bool point mass, and it rules out every incorrect constant factor c, which returns c rather than one.

Self-affinity nevertheless does not determine the definition by itself. The one-sided corruption obtained by summing sqrt(p(i)p(i)) and ignoring q passes this identity perfectly. A single identity initially appeared sufficient and was not; the gap was found by actively seeking a corruption that survives the proposed pin, rather than by assuming that one identity must suffice.

Theorem 1.3 (Pointwise-disjoint masses have zero affinity).

$$\begin{array}{c}\forall \iota [\mathrm{Fintype}(\iota )],\\ \forall p,q:\iota \to \mathbb{R},\\ (\forall i,p(i)q(i)=0)\Rightarrow \\ \mathrm{BC}(p,q)=0.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/TotalVariation/Bhattacharyya.bhattacharyya_eq_zero_of_mul_eq_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Pointwise disjointness is the second pin. On two opposite Bool point masses, every product p(i)q(i) vanishes, so the true coefficient is zero. The one-sided corruption from the preceding discussion instead evaluates to one, because it sees only the self-affinity of p.

Thus the second identity detects exactly the dependence on both inputs that self-affinity cannot test. The caller independently compiled both the surviving corruption and its refutation on the opposite-point-mass instance; the module freezes the refuting identity as a theorem rather than leaving the issue to an informal example.

Theorem 1.4 (Probability affinity is at most one).

$$\begin{array}{c}\forall \iota [\mathrm{Fintype}(\iota )],\\ \forall p,q:\iota \to \mathbb{R},\\ ((\forall i,0\le p(i))\wedge \sum _{i}p(i)=1)\wedge \\ ((\forall i,0\le q(i))\wedge \sum _{i}q(i)=1)\Rightarrow \\ \mathrm{BC}(p,q)\le 1.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/TotalVariation/Bhattacharyya.bhattacharyya_le_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

For two nonnegative normalized laws, finite Cauchy–Schwarz bounds the sum of sqrt(p(i))sqrt(q(i)) by the geometric mean of their total masses, which is one. This is an inequality associated with the pinned coefficient, not a substitute for either defining identity.

Both laws are nonnegative and normalized in this statement. These are exactly the hypotheses used to identify the two squared Euclidean norms with unit mass.

Theorem 1.5 (Total variation square is controlled by affinity).

$$\begin{array}{c}\forall \iota [\mathrm{Fintype}(\iota )],\\ \forall p,q:\iota \to \mathbb{R},\\ ((\forall i,0\le p(i))\wedge \sum _{i}p(i)=1)\wedge \\ ((\forall i,0\le q(i))\wedge \sum _{i}q(i)=1)\Rightarrow \\ \mathrm{TV}(p,q{)}^2\le 1-\mathrm{BC}(p,q{)}^2.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/TotalVariation/Bhattacharyya.total_variation_sq_le_one_sub_bhattacharyya_sq (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is the first bridge in the final proof. Factoring each absolute difference through sqrt(p(i))-sqrt(q(i)) and sqrt(p(i))+sqrt(q(i)), and then applying finite Cauchy–Schwarz, yields TV(p,q)^2 <= 1-BC(p,q)^2.

The calculation uses both probability laws in full: p and q must each be coordinatewise nonnegative and normalized to total mass one. Their normalizations evaluate the squared sums that arise after Cauchy–Schwarz.

Theorem 1.6 (Negative-divergence exponential is controlled by affinity).

$$\begin{array}{c}\forall \iota [\mathrm{Fintype}(\iota )],\\ \forall p,q:\iota \to \mathbb{R},\\ ((\forall i,0\le p(i))\wedge \sum _{i}p(i)=1)\wedge \\ (\forall i,0\le q(i))\wedge \\ (\forall i,q(i)=0\Rightarrow p(i)=0)\Rightarrow \\ \exp (-D(p\Vert \Vert q))\le \mathrm{BC}(p,q{)}^2.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/TotalVariation/Bhattacharyya.exp_neg_kl_divergence_le_bhattacharyya_sq (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is the second bridge. Jensen’s inequality is applied with p as the normalized system of weights to the logarithm of sqrt(q(i)/p(i)) on the positive support of p. Exponentiation then gives exp(-D(p||q)) <= BC(p,q)^2.

Its hypotheses are deliberately asymmetric. The law p is nonnegative and normalized, whereas q is required only to be nonnegative; the argument never uses the total mass of q. The logarithm instead forces the repository’s discrete absolute-continuity convention q(i)=0 implies p(i)=0, which makes every ratio on the positive support of p strictly positive.

The first bridge needs two normalized laws, while the second needs only one normalized law and a nonnegative reference mass. These hypothesis sets were derived statement by statement rather than copied from the final theorem, continuing the standing practice in this bucket across five waves.

Theorem 1.7 (Bretagnolle–Huber complements Pinsker).

$$\begin{array}{c}\forall \iota [\mathrm{Fintype}(\iota )],\\ \forall p,q:\iota \to \mathbb{R},\\ ((\forall i,0\le p(i))\wedge \sum _{i}p(i)=1)\wedge \\ ((\forall i,0\le q(i))\wedge \sum _{i}q(i)=1)\wedge \\ (\forall i,q(i)=0\Rightarrow p(i)=0)\Rightarrow \\ \mathrm{TV}(p,q)\le \sqrt{1-\exp (-D(p\Vert \Vert q))}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/TotalVariation/Bhattacharyya.bretagnolle_huber (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof is the direct composition of the two bridges. The first gives TV(p,q)^2 <= 1-BC(p,q)^2, and the Jensen bridge gives exp(-D(p||q)) <= BC(p,q)^2. Substitution, nonnegativity of relative entropy, and monotonicity of the square root yield the displayed bound.

This bound exists because Pinsker and Bretagnolle–Huber govern different regimes. Pinsker gives 2 TV(p,q)^2 <= D(p||q), equivalently TV(p,q) <= sqrt(D(p||q)/2). At divergence two it recovers only the universal bound one, and above two it permits an upper bound greater than one even though total variation never exceeds one. It is therefore vacuous for D(p||q) >= 2 as an improvement over the probability unit bound.

By contrast, the Bretagnolle–Huber right side is strictly below one for every finite divergence and approaches one only as the divergence tends to infinity. The inequalities are complementary, not redundant: Pinsker is sharper for small divergence, whereas Bretagnolle–Huber continues to give nontrivial information when the laws are far apart. All logarithms are natural, so divergence is measured in nats.

Theorem 1.8 (Bretagnolle–Huber is strict on a Bool witness).

$$\begin{array}{c}p={\Delta }_{\mathrm{true}},q=u_{\mathrm{Bool}},\\ \mathrm{TV}(p,q)<\sqrt{1-\exp (-D(p\Vert \Vert q))}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/TotalVariation/Bhattacharyya.bretagnolle_huber_strict_witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

The strictness claim is itself a theorem in the formal module. The concrete Bool instance takes p to be the point mass at true and q to be the uniform law. Lean computes total variation as 1/2 and relative entropy as log(2), reducing the strict inequality to 1/2 < sqrt(1/2). Thus non-equality is machine-checked and frozen rather than asserted in a comment or inferred from a numerical approximation.

The TotalVariation bucket now contains Pinsker’s bound, the metric laws with the attained variational characterization, data-processing contraction, and the complementary Bretagnolle–Huber bound with its Bhattacharyya coefficient. The coefficient is a natural bridge for future Hellinger and Renyi comparisons. No Hellinger distance, Renyi divergence, equality analysis of either bound, measure-theoretic analogue, or other extension is claimed here.

References

• Truth anchor: D5/S3/TotalVariation/Bhattacharyya.bhattacharyya
• Truth anchor: D5/S3/TotalVariation/Bhattacharyya.bhattacharyya_eq_zero_of_mul_eq_zero
• Truth anchor: D5/S3/TotalVariation/Bhattacharyya.bhattacharyya_le_one
• Truth anchor: D5/S3/TotalVariation/Bhattacharyya.bhattacharyya_self
• Truth anchor: D5/S3/TotalVariation/Bhattacharyya.bretagnolle_huber
• Truth anchor: D5/S3/TotalVariation/Bhattacharyya.bretagnolle_huber_strict_witness
• Truth anchor: D5/S3/TotalVariation/Bhattacharyya.exp_neg_kl_divergence_le_bhattacharyya_sq
• Truth anchor: D5/S3/TotalVariation/Bhattacharyya.total_variation_sq_le_one_sub_bhattacharyya_sq
• Dependency: D5/S3/TotalVariation/Metric