ProbDist

formal source

  41/-! ## VFE definition -/
  42
  43/-- A probability distribution on `ι` is a positive function summing to 1. -/
  44structure ProbDist (ι : Type*) [Fintype ι] where
  45  prob : ι → ℝ
  46  prob_pos : ∀ i, 0 < prob i
  47  prob_sum : ∑ i, prob i = 1
  48
  49theorem ProbDist.prob_nonneg (q : ProbDist ι) (i : ι) : 0 ≤ q.prob i :=
  50  le_of_lt (q.prob_pos i)
  51
  52/-- The variational free energy F[q ; E, β]. -/
  53def VFE (q : ProbDist ι) (E : ι → ℝ) (β : ℝ) : ℝ :=
  54  ∑ i, q.prob i * E i + (1 / β) * ∑ i, q.prob i * Real.log (q.prob i)
  55
  56/-- The Boltzmann reference probability for `(E, β)`. -/
  57def boltzmannDist (E : ι → ℝ) (β : ℝ) : ProbDist ι :=
  58{ prob := fun i => boltzmannProb E β i
  59  prob_pos := boltzmannProb_pos E β
  60  prob_sum := boltzmannProb_sum_one E β }
  61
  62/-! ## Gibbs inequality (KL nonnegativity)
  63
  64For two strictly positive distributions p, q on the same finite type with
  65sum 1, KL(p || q) := sum_i p_i log(p_i / q_i) >= 0, with equality iff p = q.
  66
  67We prove the inequality directly using `Real.log_le_sub_one_of_pos`. -/
  68
  69theorem kl_nonneg (p q : ProbDist ι) :
  70    0 ≤ ∑ i, p.prob i * Real.log (p.prob i / q.prob i) := by
  71  -- Equivalent: sum_i p_i log(p_i/q_i) >= 0
  72  -- Use log(x) >= 1 - 1/x (i.e. -log(1/x) <= 1 - 1/x → log(x) >= 1 - 1/x).
  73  -- Equivalent statement: -KL = sum p log(q/p) <= sum p (q/p - 1) = sum q - sum p = 0.
  74  -- So KL >= 0 follows.