Thermodynamic Entropy eq differential Entropy sub correction

lemma thermodynamicEntropy_eq_differentialEntropy_sub_correction    (T : Temperature)    (hE : Integrable 𝓒.energy (𝓒.μProd T))    [IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] :    𝓒.thermodynamicEntropy T      = 𝓒.differentialEntropy T        - kB * 𝓒.dof * Real.log 𝓒.phaseSpaceunit := by  have h_int_log_prob : Integrable (fun i => Real.log (𝓒.probability T i)) (𝓒.μProd T) := by    have h_eq : (fun i => Real.log (𝓒.probability T i))        = fun i => -(T.β : ℝ) * 𝓒.energy i            - Real.log (𝓒.mathematicalPartitionFunction T) :=      funext fun i => 𝓒.log_probability T i    rw [h_eq]    exact (hE.const_mul _).sub (integrable_const _)  simp only [thermodynamicEntropy_def, differentialEntropy]  rw [integral_congr_ae (ae_of_all _ fun i => 𝓒.log_physicalProbability T i),    integral_add h_int_log_prob (integrable_const _), integral_const]  simp only [probReal_univ, smul_eq_mul]  ring