Probability-normalized total variation

The probability convention used for Poisson approximation is half of mathlib's MeasureTheory.tvDist. For probability measures, the distance defined here is in [0, 1] and is exactly the maximum absolute discrepancy over measurable events. The event bound and its attained converse justify the normalization.

This is a general library bridge, not a proof of a Poisson approximation or of any conditioned-tree theorem from the paper. The definition paperTVDist itself is in PoissonDeclumping.Statements.Defs (from the upstream statement contract).

theorem PoissonDeclumping.paperTVDist_nonneg {α : Type u_1} [MeasurableSpace α] (μ ν : MeasureTheory.Measure α) : 0 ≤ paperTVDist μ ν

The normalized distance is nonnegative.

@[simp]

theorem PoissonDeclumping.paperTVDist_self {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) : paperTVDist μ μ = 0

A measure has zero distance from itself.

theorem PoissonDeclumping.paperTVDist_comm {α : Type u_1} [MeasurableSpace α] (μ ν : MeasureTheory.Measure α) : paperTVDist μ ν = paperTVDist ν μ

Symmetry of normalized total variation.

theorem PoissonDeclumping.abs_sub_measureReal_le_paperTVDist {α : Type u_1} [MeasurableSpace α] (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {s : Set α} (hs : MeasurableSet s) : |μ.real s - ν.real s| ≤ paperTVDist μ ν

The probability difference of any measurable event is bounded by the paper-normalized total variation distance.

theorem PoissonDeclumping.paperTVDist_le_one {α : Type u_1} [MeasurableSpace α] (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : paperTVDist μ ν ≤ 1

The normalized distance between probability measures is at most one.

@[simp]

theorem PoissonDeclumping.paperTVDist_eq_zero_iff {α : Type u_1} [MeasurableSpace α] (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : paperTVDist μ ν = 0 ↔ μ = ν

On finite measures, zero distance characterizes equality.

theorem PoissonDeclumping.paperTVDist_triangle {α : Type u_1} [MeasurableSpace α] (μ ν ξ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν] : paperTVDist μ ξ ≤ paperTVDist μ ν + paperTVDist ν ξ

The triangle inequality, with the same finiteness condition as mathlib's real-valued total variation distance.

theorem PoissonDeclumping.exists_measurableSet_abs_sub_measureReal_eq_paperTVDist {α : Type u_1} [MeasurableSpace α] (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : ∃ (s : Set α), MeasurableSet s ∧ |μ.real s - ν.real s| = paperTVDist μ ν

A Hahn decomposition supplies a measurable event attaining the normalized total variation distance between two probability measures.

theorem PoissonDeclumping.paperTVDist_le_iff {α : Type u_1} [MeasurableSpace α] (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (ε : ℝ) : paperTVDist μ ν ≤ ε ↔ ∀ (s : Set α), MeasurableSet s → |μ.real s - ν.real s| ≤ ε

Bounding normalized total variation is equivalent to uniformly bounding the probability discrepancy of every measurable event.