Source indexedlemma · leanprover/lean4:v4.33.0-rc1

KLDiv_of_convex

PFR.Kullback · PFR/Kullback.lean:120 to 150

Source documentation

If $S$ is a finite set, $w_s$ is non-negative, and ${\bf P}(X=x) = \sum_{s\in S} w_s {\bf P}(X_s=x)$ , ${\bf P}(Y=x) = \sum_{s\in S} w_s {\bf P}(Y_s=x)$ for all $x$ , then $D_{KL}(X\Vert Y) \le \sum_{s\in S} w_s D_{KL}(X_s\Vert Y_s).$

Exact Lean statement

lemma KLDiv_of_convex [Finite G]
    {ι : Type*} {S : Finset ι} {w : ι → ℝ} (hw : ∀ s ∈ S, 0 ≤ w s)
    (X' : ι → Ω'' → G) (Y' : ι → Ω''' → G)
    (hconvex : ∀ x, (μ.map X).real {x} = ∑ s ∈ S, w s * (μ''.map (X' s)).real {x})
    (hconvex' : ∀ x, (μ'.map Y).real {x} = ∑ s ∈ S, w s * (μ'''.map (Y' s)).real {x})
    (habs : ∀ s ∈ S, ∀ x, (μ'''.map (Y' s)).real {x} = 0 → (μ''.map (X' s)).real {x} = 0) :
    KL[X ; μ # Y ; μ'] ≤ ∑ s ∈ S, w s * KL[X' s ; μ'' # Y' s ; μ''']

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma KLDiv_of_convex [Finite G]    {ι : Type*} {S : Finset ι} {w : ι → ℝ} (hw : ∀ s ∈ S, 0 ≤ w s)    (X' : ι → Ω'' → G) (Y' : ι → Ω''' → G)    (hconvex : ∀ x, (μ.map X).real {x} = ∑ s ∈ S, w s * (μ''.map (X' s)).real {x})    (hconvex' : ∀ x, (μ'.map Y).real {x} = ∑ s ∈ S, w s * (μ'''.map (Y' s)).real {x})    (habs : ∀ s ∈ S, ∀ x, (μ'''.map (Y' s)).real {x} = 0 → (μ''.map (X' s)).real {x} = 0) :    KL[X ; μ # Y ; μ'] ≤ ∑ s ∈ S, w s * KL[X' s ; μ'' # Y' s ; μ'''] := by  cases nonempty_fintype G  conv_lhs => rw [KLDiv_eq_sum]  have A x : (μ.map X).real {x} * log ((μ.map X).real {x} / ((μ'.map Y).real {x}))    ≤ ∑ s ∈ S, (w s * (μ''.map (X' s)).real {x}) *        log ((w s * (μ''.map (X' s)).real {x}) / (w s * ((μ'''.map (Y' s)).real {x}))) := by    rw [hconvex, hconvex']    apply sum_mul_log_div_leq (fun s hs ↦ ?_) (fun s hs ↦ ?_) (fun s hs h's ↦ ?_)    · exact mul_nonneg (by simp [hw s hs]) (by simp)    · exact mul_nonneg (by simp [hw s hs]) (by simp)    · rcases mul_eq_zero.1 h's with h | h      · simp [h]      · simp [habs s hs x h]  have B x : (μ.map X).real {x} * log ((μ.map X).real {x} / ((μ'.map Y).real {x}))    ≤ ∑ s ∈ S, (w s * (μ''.map (X' s)).real {x}) *        log ((μ''.map (X' s)).real {x} / ((μ'''.map (Y' s)).real {x})) := by    apply (A x).trans_eq    apply Finset.sum_congr rfl (fun s _ ↦ ?_)    rcases eq_or_ne (w s) 0 with h's | h's    · simp [h's]    · congr 2      rw [mul_div_mul_left _ _ h's]  apply (Finset.sum_le_sum (fun x _ ↦ B x)).trans_eq  rw [Finset.sum_comm]  simp_rw [mul_assoc, ← Finset.mul_sum, KLDiv_eq_sum]