Total variation distance between probability measures (ℝ-valued, metric form)

tvDistReal P Q = sup { |P(A).toReal - Q(A).toReal| | A measurable }. The supremum form used by the Pinsker argument; equivalent to the L1 form on discrete supports up to a factor of 2.

This is distinct from ProbabilityTheory.FintypePMF.tvDistance, which is the Fintype L1 form.

noncomputable def MeasureTheory.tvDistReal {α : Type u_1} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : ℝ

Total variation distance between two probability measures, metric form.

Defined as the supremum of |P(A).toReal - Q(A).toReal| over measurable sets A.

Equations

• MeasureTheory.tvDistReal P Q = sSup {x : ℝ | ∃ (A : Set α), MeasurableSet A ∧ x = |(P A).toReal - (Q A).toReal|}

theorem MeasureTheory.tvDistReal_set_nonempty {α : Type u_1} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : {x : ℝ | ∃ (A : Set α), MeasurableSet A ∧ x = |(P A).toReal - (Q A).toReal|}.Nonempty

theorem MeasureTheory.tvDistReal_set_bddAbove {α : Type u_1} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : BddAbove {x : ℝ | ∃ (A : Set α), MeasurableSet A ∧ x = |(P A).toReal - (Q A).toReal|}