Total Variation Distance Estimation through Domain Reduction
Arnab Bhattacharyya, Graham Cormode, Yucheng Fu, Kuldeep S. Meel
cs.DS
Sep 16, 2026 · v2
math.PR
TL;DR
The main FPRAS results for mixtures and structured probabilistic circuits, including Lewis-weight sparsification, are formalized end-to-end in Lean 4 with AI-assisted tooling.
Abstract
Computing the total variation (TV) distance between succinctly represented high-dimensional distributions is generally intractable. We give an FPRAS for TV distance between mixtures of product distributions and, more generally, for a natural class of structured probabilistic circuits. Our main technique is a novel application of domain reduction: Given a family of feature vectors indexed by assignments, we use Lewis-weight sampling to replace the assignment domain by a polynomial-size weighted subset that simultaneously approximates the sum of absolute values of every linear projection. For mixtures of product distributions, we construct such reduced domains incrementally over the coordinates, obtaining the first FPRAS with running time polynomial in both the dimension and the number of mixture components. We then extend the approach to smooth, structured-decomposable probabilistic circuits with a common structured architecture.
Problem
Computing total variation distance between succinctly represented high-dimensional distributions is generally intractable. No FPRAS polynomial in both dimension and number of components was known for mixtures of product distributions.
Approach
Domain reduction via Lewis-weight sampling replaces the assignment domain with a polynomial-size weighted subset that approximates the sum of absolute values of every linear projection. For mixtures, reduced domains are built incrementally over coordinates. The method extends to smooth, structured-decomposable probabilistic circuits that share a v-tree. The results, including the Lewis-weight sparsification, are formalized in Lean 4 with help from the Tex2Lean tool.
Results
The paper gives the first FPRAS for TV distance between mixtures of product distributions running in time polynomial in dimension and number of components. It also gives FPRAS extensions to structured probabilistic circuits and weighted tree automata. The Lean formalization is end-to-end and depends only on Lean's classical axioms.
