§3.2, p. 16 — χ²(ν, π) = Σ_x ν(x)²/π(x) − 1

Proved

QuantumMC.Cooling.chiSq_eq_sum_sq_div_sub_one

by mikedeng1 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

chi-squareddivergencep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\nu$ and $\pi$ be functions on a finite set $\Omega$ with $\sum_x\nu(x)=1$ , $\sum_x\pi(x)=1$ and $\pi(x)>0$ for every $x$ . Then the chi-squared divergence has the second form

\chi^2(\nu,\pi)=\sum_{x\in\Omega}\pi(x)\Big(\frac{\nu(x)}{\pi(x)}-1\Big)^2=\sum_{x\in\Omega}\frac{\nu(x)^2}{\pi(x)}-1.

This is the form in which the paper evaluates $\chi^2$ between consecutive Gibbs distributions.

Formalization Note The positivity of $\pi$ is implicit on the page, which divides by $\pi(x)$ ; it is stated as a hypothesis.

Preamble

import Mathlib
import Definitions.Def_QuantumMC_Cooling_Setting

open scoped ENNReal InnerProductSpace

Formal statement

namespace QuantumMC.Cooling

/-- §3.2, p. 16: for probability vectors `ν, π` on `Ω` with `π > 0`,
`χ²(ν, π) = ∑_x π(x)(ν(x)/π(x) - 1)² = ∑_x ν(x)²/π(x) - 1`. -/
theorem chiSq_eq_sum_sq_div_sub_one {Ω : Type*} [Fintype Ω] (ν π : Ω → ℝ)
    (hν : ∑ x, ν x = 1) (hπ : ∑ x, π x = 1) (hπpos : ∀ x, 0 < π x) :
    chiSq ν π = ∑ x, ν x ^ 2 / π x - 1 := by sorry

end QuantumMC.Cooling

Source

Montanaro, Quantum speedup of Monte Carlo methods, arXiv:1504.06987v3, §3.2, p. 16, display defining χ²

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph