boltzmann_minimizes_vfe

proof body

Tactic-mode proof.

 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) -
 157          boltzmannProb E β i * Real.log (partitionFunction E β) := by
 158        intro i; rw [h_log_p i]; ring
 159      simp only [hexp]
 160      rw [Finset.sum_sub_distrib]
 161      have h1 : ∑ i, boltzmannProb E β i * (-β * E i) =
 162          -β * ∑ i, boltzmannProb E β i * E i := by
 163        rw [Finset.mul_sum]
 164        apply Finset.sum_congr rfl
 165        intro i _; ring
 166      have h2 : ∑ i, boltzmannProb E β i * Real.log (partitionFunction E β) =
 167          Real.log (partitionFunction E β) := by
 168        rw [← Finset.sum_mul, boltzmannProb_sum_one E β, one_mul]
 169      rw [h1, h2]
 170    -- Expand the cross term sum q_i log p_i
 171    have h_qlogp : ∑ i, q.prob i * Real.log (boltzmannProb E β i) =
 172        -β * (∑ i, q.prob i * E i) - Real.log (partitionFunction E β) := by
 173      have hexp : ∀ i, q.prob i * Real.log (boltzmannProb E β i) =
 174          q.prob i * (-β * E i) - q.prob i * Real.log (partitionFunction E β) := by
 175        intro i; rw [h_log_p i]; ring
 176      simp only [hexp]
 177      rw [Finset.sum_sub_distrib]
 178      have h1 : ∑ i, q.prob i * (-β * E i) =
 179          -β * ∑ i, q.prob i * E i := by
 180        rw [Finset.mul_sum]
 181        apply Finset.sum_congr rfl
 182        intro i _; ring
 183      have h2 : ∑ i, q.prob i * Real.log (partitionFunction E β) =
 184          Real.log (partitionFunction E β) := by
 185        rw [← Finset.sum_mul, q.prob_sum, one_mul]
 186      rw [h1, h2]
 187    -- Now compute log(q/p) = log q - log p
 188    have h_log_div : ∀ i, Real.log (q.prob i / boltzmannProb E β i) =
 189        Real.log (q.prob i) - Real.log (boltzmannProb E β i) := by
 190      intro i
 191      rw [Real.log_div (ne_of_gt (q.prob_pos i)) (ne_of_gt (boltzmannProb_pos E β i))]
 192    have h_qlog_div : ∑ i, q.prob i * Real.log (q.prob i / boltzmannProb E β i) =
 193        (∑ i, q.prob i * Real.log (q.prob i)) - (∑ i, q.prob i * Real.log (boltzmannProb E β i)) := by
 194      rw [← Finset.sum_sub_distrib]
 195      apply Finset.sum_congr rfl
 196      intro i _; rw [h_log_div i]; ring
 197    rw [h_qlog_div, h_qlogp, h_entropy_boltz]
 198    field_simp
 199    ring
 200  -- KL >= 0 implies the difference is nonneg
 201  have hKL := kl_nonneg q (boltzmannDist E β)
 202  have hβ_inv_pos : 0 < 1 / β := one_div_pos.mpr hβ
 203  have h_diff_nonneg : 0 ≤ VFE q E β - VFE (boltzmannDist E β) E β := by
 204    rw [h_diff]
 205    exact mul_nonneg (le_of_lt hβ_inv_pos) hKL
 206  linarith
 207
 208-- ... 3 more lines elided ...