boltzmann_minimizes_vfe

formal source

 123  linarith
 124
 125/-- The Boltzmann distribution minimizes the VFE. (Gibbs inequality.) -/
 126theorem boltzmann_minimizes_vfe (E : ι → ℝ) (β : ℝ) (hβ : 0 < β) (q : ProbDist ι) :
 127    VFE (boltzmannDist E β) E β ≤ VFE q E β := by
 128  -- VFE[q] - VFE[Boltz] = (1/β) * KL(q || Boltz) >= 0.
 129  -- Compute the difference algebraically.
 130  have h_diff : VFE q E β - VFE (boltzmannDist E β) E β =
 131      (1 / β) * ∑ i, q.prob i * Real.log (q.prob i / (boltzmannDist E β).prob i) := by
 132    unfold VFE boltzmannDist
 133    simp only []
 134    have hβ_ne : β ≠ 0 := ne_of_gt hβ
 135    -- Expand: VFE[q] - VFE[Boltz]
 136    -- = sum q_i E_i - sum p_i E_i + (1/β)(sum q_i log q_i - sum p_i log p_i)
 137    -- = (1/β) sum q_i log(q_i / p_i) + boundary terms
 138    -- Specifically using log(q_i/p_i) = log q_i - log p_i where p_i = exp(-βE_i)/Z:
 139    -- (1/β) sum q_i log(q_i / p_i) = (1/β) sum q_i log q_i - (1/β) sum q_i (-β E_i - log Z)
 140    -- = (1/β) sum q_i log q_i + sum q_i E_i + (1/β) log Z (using sum q_i = 1)
 141    -- And helmholtzF = -log Z / β = (1/β) sum p_i log p_i + sum p_i E_i
 142    -- So both sides reconcile.
 143    have h_log_p : ∀ i, Real.log (boltzmannProb E β i) =
 144        -β * E i - Real.log (partitionFunction E β) := by
 145      intro i
 146      unfold boltzmannProb
 147      rw [Real.log_div (ne_of_gt (Real.exp_pos _)) (ne_of_gt (partitionFunction_pos E β))]
 148      rw [Real.log_exp]
 149    -- Simplify the difference using h_log_p
 150    have hZ_pos := partitionFunction_pos E β
 151    have hZ_ne := ne_of_gt hZ_pos
 152    -- Expand the entropy term for Boltzmann
 153    have h_entropy_boltz : ∑ i, boltzmannProb E β i * Real.log (boltzmannProb E β i) =
 154        -β * (∑ i, boltzmannProb E β i * E i) - Real.log (partitionFunction E β) := by
 155      have hexp : ∀ i, boltzmannProb E β i * Real.log (boltzmannProb E β i) =
 156          boltzmannProb E β i * (-β * E i) -