Mathesis
Dhruv GuptaDhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z
ClaimMTH.C-2026-6024ArgumentMTH.R-2026-6024

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
Layout
ThesisStepHypothesisDefinition
pinsker_prooftheoremP.AbsolutelyContinuous QhacMeasureTheory.Integrable …h_inttvDistReal_set_nonemptytheoremtwo_sq_sub_le_klDivRealtheoremklBin_le_klDivRealtheoremklFun_integral_ge_of_meas…theoremklBin_eq_klFun_sumtheorembinary_pinskertheoremtwo_sq_le_neg_logtheoremtwo_sq_le_neg_log_one_subtheoremmonotoneOn_h_zerotheoremhasDerivAt_h_zerotheoremmonotoneOn_gtheoremderiv_g_nonneg_of_getheoremcontinuousOn_g_IcotheoremcontinuousOn_klBin_IcotheoremklBin_zero_lefttheoremklBin_selftheoremklBin_one_lefttheoremantitoneOn_gtheoremhasDerivAt_gtheoremhasDerivAt_sub_sqtheoremderiv_g_nonpos_of_letheoremderiv_factor_nonnegtheoremcontinuousOn_g_IoctheoremcontinuousOn_sub_sqtheoremcontinuousOn_klBin_IoctheoremhasDerivAt_klBin_qtheoremklBin_expandtheoremklDivReal_nonnegtheoremklDivReal_eq_toReal_klDivtheoremintegrand_eq_llrtheoremklBindefklDivRealdeftvDistRealdef
  1. DeclInformationTheory.pinsker_proofDeclaration kindtheorem
    ∀ {α : 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)
    InformationTheory.klDivRealMeasureTheory.tvDistReal
    Uses
  2. DeclMeasureTheory.tvDistReal_set_nonemptyDeclaration kindtheorem
    ∀ {α : Type u_1} [inst : MeasurableSpace α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure P]
  [MeasureTheory.IsFiniteMeasure Q], {x | ∃ A, MeasurableSet A ∧ x = |(P A).toReal - (Q A).toReal|}.Nonempty
    Used by
  3. DeclInformationTheory.two_sq_sub_le_klDivRealDeclaration kindtheorem

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

    ∀ {α : Type u_1} [inst : MeasurableSpace α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P]
  [MeasureTheory.IsProbabilityMeasure Q],
  P.AbsolutelyContinuous Q →
    MeasureTheory.Integrable (MeasureTheory.llr P Q) P →
      ∀ (A : Set α), MeasurableSet A → 2 * (P.real A - Q.real A) ^ 2 ≤ InformationTheory.klDivReal P Q
    InformationTheory.klBinInformationTheory.klDivReal
    Uses
    Used by
  4. DeclInformationTheory.klBin_le_klDivRealDeclaration kindtheorem

    Data processing inequality for indicators. For probability measures P ≪ Q with finite KL divergence and any measurable set A, the binary KL between the marginals on (A, Aᶜ) is bounded by the full KL: klBin(P(A), Q(A)) ≤ klDivReal P Q.

    ∀ {α : Type u_1} [inst : MeasurableSpace α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P]
  [MeasureTheory.IsProbabilityMeasure Q],
  P.AbsolutelyContinuous Q →
    MeasureTheory.Integrable (MeasureTheory.llr P Q) P →
      ∀ (A : Set α), MeasurableSet A → InformationTheory.klBin (P.real A) (Q.real A) ≤ InformationTheory.klDivReal P Q
    InformationTheory.klBinInformationTheory.klDivReal
    Uses
    Used by
  5. DeclInformationTheory.klFun_integral_ge_of_measurableSetDeclaration kindtheorem

    Jensen on a subset. For a finite measure Q and a measurable set A with positive mass, if f and klFun ∘ f are integrable and f ≥ 0 almost everywhere, then Q(A) · klFun((1/Q(A)) · ∫_A f dQ) ≤ ∫_A klFun(f) dQ.

    ∀ {α : Type u_1} [inst : MeasurableSpace α] {Q : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure Q] (f : α → ℝ),
  MeasureTheory.Integrable f Q →
    MeasureTheory.Integrable (fun x => InformationTheory.klFun (f x)) Q →
      (∀ᵐ (x : α) ∂Q, 0 ≤ f x) →
        ∀ {A : Set α},
          0 < Q.real A →
            Q.real A * InformationTheory.klFun ((Q.real A)⁻¹ * ∫ (x : α) in A, f x ∂Q) ≤
              ∫ (x : α) in A, InformationTheory.klFun (f x) ∂Q
    Used by
  6. DeclInformationTheory.klBin_eq_klFun_sumDeclaration kindtheorem

    Algebraic identity. The binary KL factors through klFun: klBin p q = q · klFun(p/q) + (1 − q) · klFun((1 − p)/(1 − q)).

    ∀ (p q : ℝ),
  0 < q →
    q < 1 →
      InformationTheory.klBin p q =
        q * InformationTheory.klFun (p / q) + (1 - q) * InformationTheory.klFun ((1 - p) / (1 - q))
    InformationTheory.klBin
    Used by
  7. DeclInformationTheory.binary_pinskerDeclaration kindtheorem

    Binary Pinsker inequality. 2 (p − q)² ≤ klBin p q for p ∈ [0, 1], q ∈ (0, 1). Sharp constant 2.

    ∀ (p q : ℝ), 0 ≤ p → p ≤ 1 → 0 < q → q < 1 → 2 * (p - q) ^ 2 ≤ InformationTheory.klBin p q
    InformationTheory.klBin
    Uses
    Used by
  8. DeclInformationTheory.two_sq_le_neg_logDeclaration kindtheorem

    2 (1 - q)² ≤ -log q for q ∈ (0, 1]. Substitute r = 1 - q into the previous.

    ∀ (q : ℝ), 0 < q → q ≤ 1 → 2 * (1 - q) ^ 2 ≤ -Real.log q
    Uses
    Used by
  9. DeclInformationTheory.two_sq_le_neg_log_one_subDeclaration kindtheorem

    2 q² ≤ -log(1 - q) for q ∈ [0, 1).

    ∀ (q : ℝ), 0 ≤ q → q < 1 → 2 * q ^ 2 ≤ -Real.log (1 - q)
    Uses
    Used by
  10. DeclInformationTheory.monotoneOn_h_zeroDeclaration kindtheorem

    h(q) = -log(1-q) - 2 q² is monotone on [0, 1).

    MonotoneOn (fun q => -Real.log (1 - q) - 2 * q ^ 2) (Set.Ico 0 1)
    Uses
    Used by
  11. DeclInformationTheory.hasDerivAt_h_zeroDeclaration kindtheorem

    Derivative of h(q) = -log(1-q) - 2 q² at q < 1.

    ∀ q < 1, HasDerivAt (fun q => -Real.log (1 - q) - 2 * q ^ 2) ((2 * q - 1) ^ 2 / (1 - q)) q
    Used by
  12. DeclInformationTheory.monotoneOn_gDeclaration kindtheorem

    g(q) = klBin p q − 2 (p − q)² is monotone on [p, 1).

    ∀ (p : ℝ), 0 < p → p < 1 → MonotoneOn (fun q => InformationTheory.klBin p q - 2 * (p - q) ^ 2) (Set.Ico p 1)
    InformationTheory.klBin
    Uses
    Used by
  13. DeclInformationTheory.deriv_g_nonneg_of_geDeclaration kindtheorem

    On [p, 1): derivative of g is nonnegative.

    ∀ (p q : ℝ), p ≤ q → 0 < q → q < 1 → 0 ≤ (q - p) * (1 - 2 * q) ^ 2 / (q * (1 - q))
    Uses
    Used by
  14. DeclInformationTheory.continuousOn_g_IcoDeclaration kindtheorem

    Continuity of g on Ico p 1.

    ∀ (p : ℝ), 0 < p → p < 1 → ContinuousOn (fun q => InformationTheory.klBin p q - 2 * (p - q) ^ 2) (Set.Ico p 1)
    InformationTheory.klBin
    Uses
    Used by
  15. DeclInformationTheory.continuousOn_klBin_IcoDeclaration kindtheorem

    Continuity of klBin p · on Ico p 1.

    ∀ (p : ℝ), 0 < p → p < 1 → ContinuousOn (fun q => InformationTheory.klBin p q) (Set.Ico p 1)
    InformationTheory.klBin
    Uses
    Used by
  16. DeclInformationTheory.klBin_zero_leftDeclaration kindtheorem

    Boundary case: klBin 0 q = -log(1 - q).

    ∀ (q : ℝ), InformationTheory.klBin 0 q = -Real.log (1 - q)
    InformationTheory.klBin
    Used by
  17. DeclInformationTheory.klBin_selfDeclaration kindtheorem

    klBin p p = 0 for p ∈ (0, 1).

    ∀ (p : ℝ), 0 < p → p < 1 → InformationTheory.klBin p p = 0
    InformationTheory.klBin
    Used by
  18. DeclInformationTheory.klBin_one_leftDeclaration kindtheorem

    Boundary case: klBin 1 q = -log q.

    ∀ (q : ℝ), InformationTheory.klBin 1 q = -Real.log q
    InformationTheory.klBin
    Used by
  19. DeclInformationTheory.antitoneOn_gDeclaration kindtheorem

    g(q) = klBin p q − 2 (p − q)² is antitone on (0, p].

    ∀ (p : ℝ), 0 < p → p < 1 → AntitoneOn (fun q => InformationTheory.klBin p q - 2 * (p - q) ^ 2) (Set.Ioc 0 p)
    InformationTheory.klBin
    Uses
    Used by
  20. DeclInformationTheory.hasDerivAt_gDeclaration kindtheorem

    Factored derivative identity. Derivative of g(q) := klBin(p, q) − 2 (p − q)² has the factored form (q − p) · (1 − 2q)² / (q · (1 − q)), reducing the sign of the derivative to sign(q − p).

    ∀ (p q : ℝ),
  0 < p →
    p < 1 →
      0 < q →
        q < 1 →
          HasDerivAt (fun q => InformationTheory.klBin p q - 2 * (p - q) ^ 2)
            ((q - p) * (1 - 2 * q) ^ 2 / (q * (1 - q))) q
    InformationTheory.klBin
    Uses
    Used by
  21. DeclInformationTheory.hasDerivAt_sub_sqDeclaration kindtheorem

    Derivative of (p − q)² with respect to q.

    ∀ (p q : ℝ), HasDerivAt (fun q => (p - q) ^ 2) (-2 * (p - q)) q
    Used by
  22. DeclInformationTheory.deriv_g_nonpos_of_leDeclaration kindtheorem

    On (0, p]: derivative of g is nonpositive.

    ∀ (p q : ℝ), q ≤ p → 0 < q → q < 1 → (q - p) * (1 - 2 * q) ^ 2 / (q * (1 - q)) ≤ 0
    Uses
    Used by
  23. DeclInformationTheory.deriv_factor_nonnegDeclaration kindtheorem

    The derivative factor (1 − 2q)² / (q (1 − q)) is nonnegative on (0, 1).

    ∀ (q : ℝ), 0 < q → q < 1 → 0 ≤ (1 - 2 * q) ^ 2 / (q * (1 - q))
    Used by
  24. DeclInformationTheory.continuousOn_g_IocDeclaration kindtheorem

    Continuity of g on Ioc 0 p.

    ∀ (p : ℝ), 0 < p → p < 1 → ContinuousOn (fun q => InformationTheory.klBin p q - 2 * (p - q) ^ 2) (Set.Ioc 0 p)
    InformationTheory.klBin
    Uses
    Used by
  25. DeclInformationTheory.continuousOn_sub_sqDeclaration kindtheorem

    Continuity of fun q => (p - q)² on any set.

    ∀ (p : ℝ) (s : Set ℝ), ContinuousOn (fun q => (p - q) ^ 2) s
    Used by
  26. DeclInformationTheory.continuousOn_klBin_IocDeclaration kindtheorem

    Continuity of klBin p · on Ioc 0 p.

    ∀ (p : ℝ), 0 < p → p < 1 → ContinuousOn (fun q => InformationTheory.klBin p q) (Set.Ioc 0 p)
    InformationTheory.klBin
    Uses
    Used by
  27. DeclInformationTheory.hasDerivAt_klBin_qDeclaration kindtheorem

    Derivative of klBin p · at a point q ∈ (0, 1) with p ∈ (0, 1).

    ∀ (p q : ℝ),
  0 < p → p < 1 → 0 < q → q < 1 → HasDerivAt (fun q => InformationTheory.klBin p q) ((q - p) / (q * (1 - q))) q
    InformationTheory.klBin
    Uses
    Used by
  28. DeclInformationTheory.klBin_expandDeclaration kindtheorem

    Expanded form: split into constants and q-dependent pieces. Used to compute the derivative via HasDerivAt in the next shard.

    ∀ (p q : ℝ),
  0 < p →
    p < 1 →
      0 < q →
        q < 1 →
          InformationTheory.klBin p q =
            p * Real.log p - p * Real.log q + (1 - p) * Real.log (1 - p) - (1 - p) * Real.log (1 - q)
    InformationTheory.klBin
    Used by
  29. DeclInformationTheory.klDivReal_nonnegDeclaration kindtheorem

    ℝ-valued KL is nonnegative for probability measures.

    ∀ {α : Type u_1} [inst : MeasurableSpace α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P]
  [MeasureTheory.IsProbabilityMeasure Q], 0 ≤ InformationTheory.klDivReal P Q
    InformationTheory.klDivReal
    Uses
    Used by
  30. DeclInformationTheory.klDivReal_eq_toReal_klDivDeclaration kindtheorem

    For probability measures with P ≪ Q, the ℝ-valued KL equals (Mathlib.klDiv P Q).toReal. Both measures have total mass 1, so the Mathlib correction term vanishes.

    ∀ {α : Type u_1} [inst : MeasurableSpace α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P]
  [MeasureTheory.IsProbabilityMeasure Q],
  P.AbsolutelyContinuous Q → InformationTheory.klDivReal P Q = (InformationTheory.klDiv P Q).toReal
    InformationTheory.klDivReal
    Uses
    Used by
  31. DeclInformationTheory.integrand_eq_llrDeclaration kindtheorem

    The integrand log ((P.rnDeriv Q x).toReal) is definitionally Mathlib's log-likelihood ratio llr P Q x.

    ∀ {α : Type u_1} [inst : MeasurableSpace α] (P Q : MeasureTheory.Measure α),
  (fun x => Real.log (P.rnDeriv Q x).toReal) = MeasureTheory.llr P Q
    Used by
  32. Hypothesishac
    P.AbsolutelyContinuous Q
  33. Hypothesish_int
    MeasureTheory.Integrable (MeasureTheory.llr P Q) P
  34. DefinitionInformationTheory.klBindef

    Binary KL divergence between Bernoulli(p) and Bernoulli(q).

    ℝ → ℝ → ℝ
  35. DefinitionInformationTheory.klDivRealdef

    ℝ-valued KL divergence. Returns 0 when P is not absolutely continuous with respect to Q (by convention; the ℝ≥0∞-valued klDiv returns ⊤ in that case).

    {α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.Measure α → MeasureTheory.Measure α → ℝ
  36. DefinitionMeasureTheory.tvDistRealdef

    Total variation distance between two probability measures, metric form.

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

    {α : Type u_1} →
  [inst : MeasurableSpace α] →
    (P Q : MeasureTheory.Measure α) → [MeasureTheory.IsFiniteMeasure P] → [MeasureTheory.IsFiniteMeasure Q] → ℝ
DOIMTH.R-2026-6024
Cite

Verification

Replay
accepted
Axioms
Classical.choiceQuot.soundpropext
Statement identity
not-applicable
Substrate
Lean 4 kernel v4.31.0
Dictionary pin
design-lab@5802df4 · initial
Frozen export
6e4db0a56fec
Verified
2026-09-24T00:00:00Z