theorem logZ_eq_rho_eff_plus_entropy [NeZero J]
(x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
Real.log (escortPartitionZ x ρ) =
ρ * efficiencyTerm x ρ + escortEntropy x ρ := by
unfold efficiencyTerm escortEntropy shannonEntropy escortExpectation
escortProbability escortPartitionZ
set Z := ∑ j : Fin J, x j ^ ρ with hZdef
have hZ : (0 : ℝ) < Z :=
sum_pos (fun j _ => rpow_pos_of_pos (hx j) ρ) Finset.univ_nonempty
have hZne : Z ≠ 0 := ne_of_gt hZ
-- Strategy: show -H(s) = rho * U_eff - ln Z using ln s_j = rho ln x_j - ln Z
have hsum1 : ∑ j : Fin J, x j ^ ρ / Z = 1 := by
rw [← Finset.sum_div, div_self hZne]
-- log(x_j^rho / Z) = rho * log(x_j) - log Z
have hlog : ∀ j : Fin J, Real.log (x j ^ ρ / Z) =
ρ * Real.log (x j) - Real.log Z := by
intro j
rw [Real.log_div (ne_of_gt (rpow_pos_of_pos (hx j) ρ)) hZne,
Real.log_rpow (hx j)]
-- Sum s_j * log s_j = rho * Sum s_j * log x_j - log Z
have hH : ∑ j, x j ^ ρ / Z * Real.log (x j ^ ρ / Z) =
ρ * ∑ j, x j ^ ρ / Z * Real.log (x j) - Real.log Z := by
simp_rw [hlog, mul_sub, Finset.sum_sub_distrib]
have h1 : ∑ j : Fin J, x j ^ ρ / Z * (ρ * Real.log (x j)) =
ρ * ∑ j, x j ^ ρ / Z * Real.log (x j) := by
rw [Finset.mul_sum]; exact Finset.sum_congr rfl (fun j _ => by ring)
have h2 : ∑ j : Fin J, x j ^ ρ / Z * Real.log Z =
Real.log Z := by
simp_rw [← Finset.sum_mul]; rw [hsum1, one_mul]
linarith
-- Now: log Z = rho * U_eff + H(s)
-- = rho * Sum(s_j * log x_j) + (-Sum(s_j * log s_j))
-- = rho * Sum(s_j * log x_j) - (rho * Sum(s_j * log x_j) - log Z)
-- = log Z ✓
linarith### The Thermodynamic Decomposition of Value