noncomputable def Chapter5.TVNP.tvDist {Ω : Type u_1} [MeasurableSpace Ω] (P₀ P₁ : MeasureTheory.Measure Ω) : ℝ

Total variation distance between two finite measures. TV(P₀, P₁) = sup_{A measurable} |P₀(A) − P₁(A)|

theorem Chapter5.TVNP.measure_toReal_le_one {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (S : Set Ω) : (P S).toReal ≤ 1

For probability measures, any set has measure ≤ 1 in real terms.

theorem Chapter5.TVNP.tvDist_bddAbove {Ω : Type u_1} [MeasurableSpace Ω] (P₀ P₁ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P₀] [MeasureTheory.IsProbabilityMeasure P₁] : BddAbove {x : ℝ | ∃ (S : Set Ω), MeasurableSet S ∧ x = |(P₀ S).toReal - (P₁ S).toReal|}

The set defining TV distance is bounded above for probability measures.

theorem Chapter5.TVNP.tvDist_ge_abs_diff {Ω : Type u_1} [MeasurableSpace Ω] (P₀ P₁ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P₀] [MeasureTheory.IsProbabilityMeasure P₁] (S : Set Ω) (hS : MeasurableSet S) : |(P₀ S).toReal - (P₁ S).toReal| ≤ tvDist P₀ P₁

TV distance is ≥ |P₀(S) - P₁(S)| for any measurable S.

theorem Chapter5.TVNP.neyman_pearson_lower {Ω : Type u_1} {x✝ : MeasurableSpace Ω} (P₀ P₁ : MeasureTheory.Measure Ω) (hP₀ : MeasureTheory.IsProbabilityMeasure P₀) (hP₁ : MeasureTheory.IsProbabilityMeasure P₁) (ψ : Ω → Bool) (hψ : Measurable ψ) : (P₀ {ω : Ω | ψ ω = true}).toReal + (P₁ {ω : Ω | ψ ω = false}).toReal ≥ 1 - tvDist P₀ P₁

Lemma 5.3 (Neyman-Pearson lower bound). For any measurable test ψ : Ω → Bool, the sum of type I and type II errors satisfies P₀(ψ=1) + P₁(ψ=0) ≥ 1 − TV(P₀,P₁).

noncomputable def Chapter5.TVNP.lrTest {Ω : Type u_1} [MeasurableSpace Ω] (P₁ P₀ ν : MeasureTheory.Measure Ω) : Ω → Bool

The Likelihood Ratio test ψ*(ω) = 𝕀(p₁(ω) ≥ p₀(ω)), where p₀, p₁ are Radon-Nikodym derivatives of P₀, P₁ with respect to a common dominating measure ν. Returns true when p₁(ω) ≥ p₀(ω), i.e., when the evidence favors P₁ over P₀.

theorem Chapter5.TVNP.lrTest_measurable {Ω : Type u_1} [MeasurableSpace Ω] (P₁ P₀ ν : MeasureTheory.Measure Ω) : Measurable (lrTest P₁ P₀ ν)

The Likelihood Ratio test is measurable.

theorem Chapter5.TVNP.measure_sub_le_on_positive_set {Ω : Type u_1} {x✝ : MeasurableSpace Ω} (P₀ P₁ ν : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P₀] [MeasureTheory.IsProbabilityMeasure P₁] [MeasureTheory.SigmaFinite ν] (hν₀ : P₀.AbsolutelyContinuous ν) (hν₁ : P₁.AbsolutelyContinuous ν) (T : Set Ω) (hT : MeasurableSet T) : (P₀ T).toReal - (P₁ T).toReal ≤ (P₀ {ω : Ω | P₁.rnDeriv ν ω < P₀.rnDeriv ν ω}).toReal - (P₁ {ω : Ω | P₁.rnDeriv ν ω < P₀.rnDeriv ν ω}).toReal

Helper: for any measurable T, P₀(T) − P₁(T) ≤ P₀(R) − P₁(R) where R = {ω | P₁.rnDeriv ν ω < P₀.rnDeriv ν ω}. Uses the integral splitting argument: on R, p₀ − p₁ ≥ 0, and on Rᶜ, p₀ − p₁ ≤ 0.

theorem Chapter5.TVNP.neyman_pearson_equality {Ω : Type u_1} {x✝ : MeasurableSpace Ω} (P₀ P₁ ν : MeasureTheory.Measure Ω) (hP₀ : MeasureTheory.IsProbabilityMeasure P₀) (hP₁ : MeasureTheory.IsProbabilityMeasure P₁) (hν₀ : P₀.AbsolutelyContinuous ν) (hν₁ : P₁.AbsolutelyContinuous ν) [MeasureTheory.SigmaFinite ν] : (P₀ {ω : Ω | lrTest P₁ P₀ ν ω = true}).toReal + (P₁ {ω : Ω | lrTest P₁ P₀ ν ω = false}).toReal = 1 - tvDist P₀ P₁

Lemma 5.3 (Neyman-Pearson, equality part, book lines 3319-3321). Moreover, equality holds for the Likelihood Ratio test ψ* = 𝕀(p₁ ≥ p₀): P₀(ψ*=1) + P₁(ψ*=0) = 1 − TV(P₀, P₁).

Here ν is a common dominating measure for P₀ and P₁ (e.g. ν = P₀ + P₁), and the LR test is defined using Radon-Nikodym derivatives dP₀/dν and dP₁/dν. The proof follows the book: on {p₁ ≥ p₀}, p₀ = min(p₀, p₁), and on {p₁ < p₀}, p₁ = min(p₀, p₁), so the sum telescopes to ∫ min(p₀, p₁) = 1 − TV(P₀, P₁).

noncomputable def Chapter5.TVNP.klDiv_real {Ω : Type u_1} [MeasurableSpace Ω] (P Q : MeasureTheory.Measure Ω) : ℝ

Real-valued KL divergence. Defined as (klDiv P Q).toReal, where klDiv is Mathlib's InformationTheory.klDiv taking values in ℝ≥0∞. For probability measures P absolutely continuous w.r.t. Q with integrable log-likelihood ratio, this equals ∫ log(dP/dQ) dP. When P is not absolutely continuous w.r.t. Q, klDiv P Q = ⊤ and toReal returns 0.

theorem Chapter5.TVNP.klDiv_real_nonneg {Ω : Type u_1} [MeasurableSpace Ω] (P Q : MeasureTheory.Measure Ω) (_hP : MeasureTheory.IsProbabilityMeasure P) (_hQ : MeasureTheory.IsProbabilityMeasure Q) : 0 ≤ klDiv_real P Q

KL divergence (real-valued) is nonneg, since it is the toReal of an ENNReal value.

theorem Chapter5.TVNP.tvDist_eq_infoTheory {Ω : Type u_1} [MeasurableSpace Ω] (P Q : MeasureTheory.Measure Ω) : tvDist P Q = InfoTheory.tvDist P Q

The TVNP.tvDist and InfoTheory.tvDist are definitionally equal.

theorem Chapter5.TVNP.klDiv_real_eq_infoTheory {Ω : Type u_1} [MeasurableSpace Ω] (P Q : MeasureTheory.Measure Ω) : klDiv_real P Q = InfoTheory.klDiv_real P Q

The TVNP.klDiv_real and InfoTheory.klDiv_real are definitionally equal.

theorem Chapter5.TVNP.tvDist_nonneg {Ω : Type u_1} [MeasurableSpace Ω] (P Q : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] : 0 ≤ tvDist P Q

TV distance is nonneg for probability measures.

theorem Chapter5.TVNP.tvDist_le_one {Ω : Type u_1} [MeasurableSpace Ω] (P Q : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] : tvDist P Q ≤ 1

TV distance is ≤ 1 for probability measures.

theorem Chapter5.TVNP.two_sub_two_sqrt_one_sub_ge (x : ℝ) (hx1 : x ≤ 1) : 2 - 2 * √(1 - x) ≥ x

Step 3 of Pinsker's proof (pure real analysis): For x ∈ [0,1], 2 − 2√(1−x) ≥ x. Proof: set s = √(1−x), then 2 − 2s − x = 2 − 2s − (1−s²) = (1−s)² ≥ 0.

theorem Chapter5.TVNP.pinsker_inequality {Ω : Type u_1} {x✝ : MeasurableSpace Ω} (P Q : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (hac : P.AbsolutelyContinuous Q) (hKL : InformationTheory.klDiv P Q ≠ ⊤) : tvDist P Q ≤ √(klDiv_real P Q)

Lemma 5.8 (Pinsker's inequality). TV(P,Q) ≤ √(KL(P‖Q)). This is stated in terms of our real-valued KL divergence definition. The hypothesis hKL ensures KL(P‖Q) is finite (i.e. not ⊤), which is needed for klDiv_real (defined via ENNReal.toReal) to be meaningful; without it, toReal maps ⊤ to 0, making the inequality vacuously weak.

The proof follows the book (Rigollet, Lemma 5.8, Steps 1–3): Step 1: KL ≥ 2 − 2·BC (log inequality) Step 2: BC² ≤ 1 − TV² (Cauchy-Schwarz) Step 3: 2 − 2√(1−TV²) ≥ TV² (pure real analysis) Combining: KL ≥ 2 − 2√(1−TV²) ≥ TV², hence TV ≤ √KL.

theorem Chapter5.TVNP.neyman_pearson {Ω : Type u_1} {x✝ : MeasurableSpace Ω} (P₀ P₁ ν : MeasureTheory.Measure Ω) (hP₀ : MeasureTheory.IsProbabilityMeasure P₀) (hP₁ : MeasureTheory.IsProbabilityMeasure P₁) (hν₀ : P₀.AbsolutelyContinuous ν) (hν₁ : P₁.AbsolutelyContinuous ν) [MeasureTheory.SigmaFinite ν] : (∀ (ψ : Ω → Bool), Measurable ψ → (P₀ {ω : Ω | ψ ω = true}).toReal + (P₁ {ω : Ω | ψ ω = false}).toReal ≥ 1 - tvDist P₀ P₁) ∧ (P₀ {ω : Ω | lrTest P₁ P₀ ν ω = true}).toReal + (P₁ {ω : Ω | lrTest P₁ P₀ ν ω = false}).toReal = 1 - tvDist P₀ P₁

Lemma 5.3 (Neyman-Pearson, bundled). The likelihood ratio test is optimal for simple hypothesis testing: (a) For any measurable test ψ, P₀(ψ=1) + P₁(ψ=0) ≥ 1 − TV(P₀,P₁). (b) Equality holds for the likelihood ratio test ψ⋆ = 𝕀(p₁ ≥ p₀): P₀(ψ⋆=1) + P₁(ψ⋆=0) = 1 − TV(P₀,P₁).