Pinsker's inequality with the sharp constant. tvDistReal P Q ≤ sqrt(klDivReal P Q / 2) for probability measures P ≪ Q with finite KL divergence.
DeclInformationTheory.pinsker_proof
∀ {α : Type u_1} [inst : MeasurableSpace α] (P Q : MeasureTheory.Measure α)
[inst_1 : MeasureTheory.IsProbabilityMeasure P] [inst_2 : MeasureTheory.IsProbabilityMeasure Q],
P.AbsolutelyContinuous Q →
MeasureTheory.Integrable (MeasureTheory.llr P Q) P →
MeasureTheory.tvDistReal P Q ≤ √(InformationTheory.klDivReal P Q / 2)TopicInformation theory
Arguments
| DOI | Author | Date |
|---|---|---|
| MTH.R-2026-6024 | Dhruv Gupta | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6024
Cite
Verification
- Library
- ZPM.InformationTheory.Pinsker.General
- Statement digest
- 19e1fb4bee5e
- First verified
- 2026-09-24T00:00:00Z