Pinsker's inequality (general, sharp constant)

Assembles the three layers:

• Binary Pinsker gives 2 (p − q)² ≤ klBin p q.
• DPI for indicators gives klBin(P(A), Q(A)) ≤ klDivReal P Q.
• Combining them gives the per-set squared bound 2 (P(A) − Q(A))² ≤ klDivReal P Q for every measurable A.

Taking sSup over measurable sets gives tvDistReal P Q ≤ sqrt(klDivReal P Q / 2), Pinsker's inequality with the sharp constant.

theorem InformationTheory.two_sq_sub_le_klDivReal {α : Type u_1} [MeasurableSpace α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (hac : P.AbsolutelyContinuous Q) (h_int : MeasureTheory.Integrable (MeasureTheory.llr P Q) P) (A : Set α) (hA : MeasurableSet A) : 2 * (P.real A - Q.real A) ^ 2 ≤ klDivReal P Q

Per-set squared bound. 2 (P(A) − Q(A))² ≤ klDivReal P Q for any measurable set A, given P ≪ Q and finite KL.

theorem InformationTheory.pinsker_proof {α : Type u_1} [MeasurableSpace α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (hac : P.AbsolutelyContinuous Q) (h_int : MeasureTheory.Integrable (MeasureTheory.llr P Q) P) : MeasureTheory.tvDistReal P Q ≤ √(klDivReal P Q / 2)

Pinsker's inequality with the sharp constant. tvDistReal P Q ≤ sqrt(klDivReal P Q / 2) for probability measures P ≪ Q with finite KL divergence.