InformationTheory.Shannon.EPI.G2.KLVariationalLower
Donsker–Varadhan variational lower bound (easy direction) #
The variational lower bound on KL divergence:
KL(μ ‖ ν) ≥ ∫ g dμ − log (∫ exp(g) dν) for all bounded measurable g.
Main statements #
integral_exp_sub_llr_le: change-of-measure lemma∫ exp(g − llr μ ν) ∂μ ≤ ∫ exp(g) ∂ν.klDiv_variational_lower_bound: main theorem∫ g dμ − log (∫ exp(g) dν) ≤ (klDiv μ ν).toReal.
Implementation notes #
The proof applies Jensen's inequality (ConvexOn.map_integral_le) to h := g − llr μ ν,
then uses the change-of-measure identity (integral_toReal_rnDeriv_mul) to push to ν.
The hard direction of Donsker–Varadhan (sup attainment) is not in scope here.
InformationTheory.Shannon.integral_exp_sub_llr_le
source{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
(hμν : μ.AbsolutelyContinuous ν)
{g : α → ℝ}
(hg_meas : Measurable g)
{C : ℝ}
(hg_bdd : ∀ (x : α), |g x| ≤ C)
:
Change-of-measure inequality: when μ ≪ ν,
∫ exp (g x − llr μ ν x) ∂μ ≤ ∫ exp (g x) ∂ν for all bounded measurable g.
@audit:ok
Used by
InformationTheory.Shannon.klDiv_variational_lower_bound
source{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
(hμν : μ.AbsolutelyContinuous ν)
(h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ)
{g : α → ℝ}
(hg_meas : Measurable g)
{C : ℝ}
(hg_bdd : ∀ (x : α), |g x| ≤ C)
:
Donsker–Varadhan variational lower bound (easy direction):
∫ g ∂μ − log (∫ exp g ∂ν) ≤ (klDiv μ ν).toReal for all bounded measurable g.
@audit:ok