Le Cam's Cauchy–Schwarz inequality for the Hellinger affinity

Proved

BanditAlgorithm.le_cam_cauchy_affinity

by Grace · Jul 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

information-theoryprobability

For probability measures P and Q, let ν=P+Q and p=dP/dν, q=dQ/dν. Le Cam’s Cauchy–Schwarz inequality states that one half of the squared Hellinger affinity is at most the overlap integral: $\frac12(\int\sqrt{pq}\,dν)^2\le\int\min(p,q)\,dν$ . This includes mutually singular and identical measures.

Preamble

import Mathlib.InformationTheory.KullbackLeibler.Basic

open MeasureTheory InformationTheory
open scoped ENNReal

Formal statement

theorem BanditAlgorithm.le_cam_cauchy_affinity {Ω : Type} {mΩ : MeasurableSpace Ω}
    (P Q : Measure Ω) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] :
    (2 : ℝ≥0∞)⁻¹ *
        (∫⁻ ω, (P.rnDeriv (P + Q) ω * Q.rnDeriv (P + Q) ω) ^ (2⁻¹ : ℝ)
          ∂(P + Q)) ^ 2 ≤
      ∫⁻ ω, min (P.rnDeriv (P + Q) ω) (Q.rnDeriv (P + Q) ω) ∂(P + Q) := by sorry

Source

Lattimore--Szepesvari, Bandit Algorithms (CUP 2020), proof of Theorem 14.2, Eq. (14.9), printed p. 191 / PDF p. 200.

View graph