TV-based transfer principle for Bool-valued tests #
If tvDistance p q ≤ δ, then for every Bool-valued test f,
|E_p[f] - E_q[f]| ≤ δ. A single TV bound therefore implies uniform
test-expectation approximation across any finite family of tests without
a union bound. This is the mechanism that lets a compression argument
swap a target distribution for an empirical one.
theorem
ProbabilityTheory.FintypePMF.expectation_approx_of_tv
{α : Type u_1}
[Fintype α]
(p q : FintypePMF α)
(f : α → Bool)
(δ : ℝ)
(hδ : p.tvDistance q ≤ δ)
:
Transfer principle. If tvDistance p q ≤ δ, then for every Bool-valued test
f, the expectations under p and q differ by at most δ.
theorem
ProbabilityTheory.FintypePMF.tv_bound_implies_all_tests
{α : Type u_1}
[Fintype α]
(p q : FintypePMF α)
(ε : ℝ)
(hε : p.tvDistance q ≤ ε)
(tests : Finset (α → Bool))
(f : α → Bool)
:
f ∈ tests → |p.boolTestExpectation f - q.boolTestExpectation f| ≤ ε
Uniform version of expectation_approx_of_tv: a single TV bound suffices for
every test in any finite family simultaneously, with no union bound.