Mean Energy eq neg deriv log math Z of beta

lemma meanEnergy_eq_neg_deriv_log_mathZ_of_beta    (𝓒 : CanonicalEnsemble ι) (T : Temperature)    (hT_pos : 0 < T.val) [IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ]    (h_deriv :        HasDerivWithinAt          (fun β : ℝ => ∫ i, Real.exp (-β * 𝓒.energy i) ∂ 𝓒.μ)          (- ∫ i, 𝓒.energy i * Real.exp (-(T.β : ℝ) * 𝓒.energy i) ∂𝓒.μ)          (Set.Ioi 0) (T.β : ℝ)) :    𝓒.meanEnergy T =      - (derivWithin          (fun β : ℝ => Real.log (∫ i, Real.exp (-β * 𝓒.energy i) ∂𝓒.μ))          (Set.Ioi 0) (T.β : ℝ)) := by  set f : ℝ → ℝ := fun β => ∫ i, Real.exp (-β * 𝓒.energy i) ∂𝓒.μ  have hβ_pos : 0 < (T.β : ℝ) := beta_pos T hT_pos  have hZpos : 0 < f (T.β : ℝ) := by    simpa [f, mathematicalPartitionFunction_eq_integral (𝓒 := 𝓒) (T := T)]      using mathematicalPartitionFunction_pos (𝓒 := 𝓒) (T := T)  have h_log : HasDerivWithinAt (fun β : ℝ => Real.log (f β))      ((1 / f (T.β : ℝ)) * (- ∫ i, 𝓒.energy i * Real.exp (-(T.β : ℝ) * 𝓒.energy i) ∂𝓒.μ))      (Set.Ioi 0) (T.β : ℝ) := by    simpa [f] using hasDerivWithinAt_log_comp' (hf := h_deriv) (hx := hZpos.ne')  have hUD : UniqueDiffWithinAt ℝ (Set.Ioi (0:ℝ)) (T.β : ℝ) :=    isOpen_Ioi.uniqueDiffWithinAt hβ_pos  rw [meanEnergy_eq_ratio_of_integrals, h_log.derivWithin hUD]  simp only [f]  ring