Physlib.StatisticalMechanics.MicroCanonicalEnsemble.ThermoQuantities

Imports

/-
Copyright (c) 2025 Alex Meiburg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alex Meiburg
-/
module

public import Physlib.StatisticalMechanics.MicroCanonicalEnsemble.Basic
public import QuantumInfo.ForMathlib.ComplexLaplaceTransform

The theormodynamical quantities of a microcanonical ensemble

@[expose] public section

The partition function corresponding to a given MicroHamiltonian. This is a function taking a thermodynamic β, not a temperature. It also depends on the data D defining the system extrinsincs.

Ideally this would be an NNReal, but ∫ (NNReal) doesn't work right now, so it would just be a separate proof anyway

def partitionZ (β : ℝ) : ℝ :=
  ∫ (config : H.dim d → ℝ),
    let E := H.H config
    if h : E = ⊤ then 0 else Real.exp (-β * (E.untop h))

The complexified partition function, viewed as a Laplace transform.

def PartitionZComplex (z : ℂ) : ℂ :=
  ComplexLaplaceTransform (fun config : H.dim d → ℝ => H.H config) z

The complex convergence domain of the partition-function Laplace transform.

def ZComplexConvergenceDomain : Set ℂ :=
  ComplexLaplaceConvergenceDomain (fun config : H.dim d → ℝ => H.H config)



private theorem partitionZ_eq_re_partitionZComplex {β : ℝ}
    (hβ : (β : ℂ) ∈ H.ZComplexConvergenceDomain d) :
    H.partitionZ d β = (H.PartitionZComplex d β).re := byD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain d⊢ H.partitionZ d β = (H.PartitionZComplex d ↑β).re
  have hInt : MeasureTheory.Integrable (μ := MeasureTheory.volume)
      (ComplexLaplaceIntegrand (fun config : H.dim d → ℝ => H.H config) (β : ℂ)) := hβD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volume⊢ H.partitionZ d β = (H.PartitionZComplex d ↑β).re
  rw [partitionZ,D:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volume⊢ (∫ (config : H.dim d → ℝ),
    have E := H.H config;
    if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  (H.PartitionZComplex d ↑β).reD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volume⊢ (∫ (config : H.dim d → ℝ),
    have E := H.H config;
    if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  (∫ (x : H.dim d → ℝ), ComplexLaplaceIntegrand (fun config => H.H config) (↑β) x).re PartitionZComplex,D:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volume⊢ (∫ (config : H.dim d → ℝ),
    have E := H.H config;
    if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  (ComplexLaplaceTransform (fun config => H.H config) ↑β).reD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volume⊢ (∫ (config : H.dim d → ℝ),
    have E := H.H config;
    if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  (∫ (x : H.dim d → ℝ), ComplexLaplaceIntegrand (fun config => H.H config) (↑β) x).re ComplexLaplaceTransformD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volume⊢ (∫ (config : H.dim d → ℝ),
    have E := H.H config;
    if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  (∫ (x : H.dim d → ℝ), ComplexLaplaceIntegrand (fun config => H.H config) (↑β) x).reD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volume⊢ (∫ (config : H.dim d → ℝ),
    have E := H.H config;
    if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  (∫ (x : H.dim d → ℝ), ComplexLaplaceIntegrand (fun config => H.H config) (↑β) x).re]D:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volume⊢ (∫ (config : H.dim d → ℝ),
    have E := H.H config;
    if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  (∫ (x : H.dim d → ℝ), ComplexLaplaceIntegrand (fun config => H.H config) (↑β) x).re
  calc
    (∫ (config : H.dim d → ℝ),
        have E := H.H config
        if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
        ∫ x, RCLike.re (ComplexLaplaceIntegrand
          (fun config : H.dim d → ℝ => H.H config) (β : ℂ) x) := byD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volume⊢ (∫ (config : H.dim d → ℝ),
    have E := H.H config;
    if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  ∫ (x : H.dim d → ℝ), RCLike.re (ComplexLaplaceIntegrand (fun config => H.H config) (↑β) x)
      apply MeasureTheory.integral_congr_aeD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volume⊢ (fun a =>
    have E := H.H a;
    if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =ᵐ[MeasureTheory.volume]
  fun a => RCLike.re (ComplexLaplaceIntegrand (fun config => H.H config) (↑β) a)
      filter_upwards with configD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volumeconfig:H.dim d → ℝ⊢ (have E := H.H config;
  if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  RCLike.re (ComplexLaplaceIntegrand (fun config => H.H config) (↑β) config)
      unfold ComplexLaplaceIntegrandD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volumeconfig:H.dim d → ℝ⊢ (have E := H.H config;
  if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  RCLike.re
    (if h : (fun config => H.H config) config = ⊤ then 0
    else Complex.exp (-↑β * ↑(((fun config => H.H config) config).untop h)))
      by_cases h : H.H config = ⊤posD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volumeconfig:H.dim d → ℝh:H.H config = ⊤⊢ (have E := H.H config;
  if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  RCLike.re
    (if h : (fun config => H.H config) config = ⊤ then 0
    else Complex.exp (-↑β * ↑(((fun config => H.H config) config).untop h)))negD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volumeconfig:H.dim d → ℝh:¬H.H config = ⊤⊢ (have E := H.H config;
  if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  RCLike.re
    (if h : (fun config => H.H config) config = ⊤ then 0
    else Complex.exp (-↑β * ↑(((fun config => H.H config) config).untop h)))
      ·posD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volumeconfig:H.dim d → ℝh:H.H config = ⊤⊢ (have E := H.H config;
  if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  RCLike.re
    (if h : (fun config => H.H config) config = ⊤ then 0
    else Complex.exp (-↑β * ↑(((fun config => H.H config) config).untop h))) simp [h]All goals completed! 🐙
      ·negD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volumeconfig:H.dim d → ℝh:¬H.H config = ⊤⊢ (have E := H.H config;
  if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)) =
  RCLike.re
    (if h : (fun config => H.H config) config = ⊤ then 0
    else Complex.exp (-↑β * ↑(((fun config => H.H config) config).untop h))) simp only [h, dite_false]negD:TypeH:MicroHamiltonian Dd:Dβ:ℝhβ:↑β ∈ H.ZComplexConvergenceDomain dhInt:MeasureTheory.Integrable (ComplexLaplaceIntegrand (fun config => H.H config) ↑β) MeasureTheory.volumeconfig:H.dim d → ℝh:¬H.H config = ⊤⊢ Real.exp (-β * (H.H config).untop ⋯) = RCLike.re (Complex.exp (-↑β * ↑((H.H config).untop ⋯)))
        simpa [Complex.ofReal_mul] using
          (Complex.exp_ofReal_re (-(β * (H.H config).untop h))).symmAll goals completed! 🐙
    _ = RCLike.re (∫ x, ComplexLaplaceIntegrand
        (fun config : H.dim d → ℝ => H.H config) (β : ℂ) x) := integral_re hInt

The partition function as a function of temperature T instead of β.

def partitionZT (T : ℝ) : ℝ :=
  partitionZ H d (1/T)

The Internal Energy, U or E, defined as -∂(ln Z)/∂β. Parameterized here with β.

def internalU (β : ℝ) : ℝ :=
  -deriv (fun β' ↦ (partitionZ H d β').log) β

The Helmholtz Free Energy, -T * ln Z. Also denoted F. Parameterized here with temperature T, not β.

def helmholtzA (T : ℝ) : ℝ :=
  -T * (partitionZT H d T).log

The entropy, defined as the -∂A/∂T. Function of T.

def entropyS (T : ℝ) : ℝ :=
  -deriv (helmholtzA H d) T

The entropy, defined as ln Z + β*U. Function of β.

def entropySβ (β : ℝ) : ℝ :=
  (partitionZ H d β).log + β * internalU H d β

To be able to compute or define anything from a Hamiltonian, we need its partition function to be a computable integral. A Hamiltonian is ZIntegrable at β if PartitionZ is Lesbegue integrable and nonzero.

def ZIntegrable (β : ℝ) : Prop :=
  MeasureTheory.Integrable (fun (config : H.dim d → ℝ) ↦
    let E := H.H config;
    if h : E = ⊤ then 0 else Real.exp (-β * (E.untop h))) ∧ (H.partitionZ d β ≠ 0)

This Prop defines the most common case of ZIntegrable, that it is integrable at all finite temperatures (aka all positive β).

def PositiveβIntegrable : Prop :=
  ∀ β > 0, H.ZIntegrable d β

The two definitions of entropy, in terms of T or β = 1 / T, are equivalent.


theorem entropy_A_eq_entropy_Z (T : ℝ) (hT : T ≠ 0)
    (hZne : H.partitionZ d (1 / T) ≠ 0)
    (hZint : ((1 / T : ℝ) : ℂ) ∈ interior (H.ZComplexConvergenceDomain d)) :
    entropyS H d T = entropySβ H d (1 / T) := byD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)⊢ H.entropyS d T = H.entropySβ d (1 / T)
  have hZdiff : DifferentiableAt ℝ (H.partitionZ d) (1 / T) :=
    (H.contDiffAt_partitionZ_of_mem_interior_convergenceDomain d hZint).differentiableAt
      (byD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)⊢ ⊤ ≠ 0D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ H.entropyS d T = H.entropySβ d (1 / T) simpAll goals completed! 🐙D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ H.entropyS d T = H.entropySβ d (1 / T))D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ H.entropyS d T = H.entropySβ d (1 / T)
  dsimp [entropyS, entropySβ, internalU, partitionZT]D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -deriv (H.helmholtzA d) T =
  Real.log (H.partitionZ d (1 / T)) + 1 / T * -deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T)
  unfold helmholtzAD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -deriv (fun T => -T * Real.log (H.partitionZT d T)) T =
  Real.log (H.partitionZ d (1 / T)) + 1 / T * -deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T)
  erw [deriv_mulD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -(deriv Neg.neg T * Real.log (H.partitionZT d T) + -T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + 1 / T * -deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T)hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T]D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -(deriv Neg.neg T * Real.log (H.partitionZT d T) + -T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + 1 / T * -deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T)hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T
  rw [deriv_neg'',D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -(-1 * Real.log (H.partitionZT d T) + -T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + 1 / T * -deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T)hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) TD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ Real.log (H.partitionZT d T) + -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T neg_mul,D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -(-(1 * Real.log (H.partitionZT d T)) + -T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + 1 / T * -deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T)hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) TD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ Real.log (H.partitionZT d T) + -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T one_mul,D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -(-Real.log (H.partitionZT d T) + -T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + 1 / T * -deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T)hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) TD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ Real.log (H.partitionZT d T) + -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T neg_add_rev,D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) + - -Real.log (H.partitionZT d T) =
  Real.log (H.partitionZ d (1 / T)) + 1 / T * -deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T)hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) TD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ Real.log (H.partitionZT d T) + -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T neg_neg,D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) + Real.log (H.partitionZT d T) =
  Real.log (H.partitionZ d (1 / T)) + 1 / T * -deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T)hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) TD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ Real.log (H.partitionZT d T) + -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T mul_neg,D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) + Real.log (H.partitionZT d T) =
  Real.log (H.partitionZ d (1 / T)) + -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) TD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ Real.log (H.partitionZT d T) + -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T add_commD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ Real.log (H.partitionZT d T) + -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) TD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ Real.log (H.partitionZT d T) + -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T]D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ Real.log (H.partitionZT d T) + -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  Real.log (H.partitionZ d (1 / T)) + -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T
  congr 1e_aD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T
  simp_rw [e_aD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -(-T * deriv (fun T => Real.log (H.partitionZT d T)) T) =
  -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))partitionZTe_aD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ -(-T * deriv (fun T => Real.log (H.partitionZ d (1 / T))) T) =
  -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))]
  have hdc := deriv_comp (h := fun T ↦ T⁻¹) (h₂ := fun β => Real.log (H.partitionZ d β)) T ?_ ?_e_a.refine_3D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)hdc:deriv ((fun β => Real.log (H.partitionZ d β)) ∘ fun T => T⁻¹) T =
  deriv (fun β => Real.log (H.partitionZ d β)) T⁻¹ * deriv (fun T => T⁻¹) T⊢ -(-T * deriv (fun T => Real.log (H.partitionZ d (1 / T))) T) =
  -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))e_a.refine_1D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun β => Real.log (H.partitionZ d β)) T⁻¹e_a.refine_2D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => T⁻¹) ThcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T
  unfold Function.comp at hdce_a.refine_3D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)hdc:deriv (fun x => (fun β => Real.log (H.partitionZ d β)) ((fun T => T⁻¹) x)) T =
  deriv (fun β => Real.log (H.partitionZ d β)) T⁻¹ * deriv (fun T => T⁻¹) T⊢ -(-T * deriv (fun T => Real.log (H.partitionZ d (1 / T))) T) =
  -(1 / T * deriv (fun β' => Real.log (H.partitionZ d β')) (1 / T))e_a.refine_1D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun β => Real.log (H.partitionZ d β)) T⁻¹e_a.refine_2D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => T⁻¹) ThcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T
  simp only [hdc, one_div, deriv_inv', mul_neg, neg_inj]e_a.refine_3D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)hdc:deriv (fun x => (fun β => Real.log (H.partitionZ d β)) ((fun T => T⁻¹) x)) T =
  deriv (fun β => Real.log (H.partitionZ d β)) T⁻¹ * deriv (fun T => T⁻¹) T⊢ -(-T * (deriv (fun β => Real.log (H.partitionZ d β)) T⁻¹ * (T ^ 2)⁻¹)) =
  T⁻¹ * deriv (fun β => Real.log (H.partitionZ d β)) T⁻¹e_a.refine_1D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun β => Real.log (H.partitionZ d β)) T⁻¹e_a.refine_2D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => T⁻¹) ThcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T
  field_simpe_a.refine_1D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun β => Real.log (H.partitionZ d β)) T⁻¹e_a.refine_2D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => T⁻¹) ThcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T
  ring_nfe_a.refine_1D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun β => Real.log (H.partitionZ d β)) T⁻¹e_a.refine_2D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => T⁻¹) ThcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg ThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T
  --Show the differentiability side-goals
  ·e_a.refine_1D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun β => Real.log (H.partitionZ d β)) T⁻¹ rw [← one_dive_a.refine_1D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun β => Real.log (H.partitionZ d β)) (1 / T)e_a.refine_1D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun β => Real.log (H.partitionZ d β)) (1 / T)]e_a.refine_1D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun β => Real.log (H.partitionZ d β)) (1 / T)
    fun_prop (disch := assumption)All goals completed! 🐙
  ·e_a.refine_2D:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => T⁻¹) T fun_prop (disch := assumption)All goals completed! 🐙
  ·hcD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ Neg.neg T fun_propAll goals completed! 🐙
  ·hdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) T simp_rw [hdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZT d T)) TpartitionZThdD:TypeH:MicroHamiltonian Dd:DT:ℝhT:T ≠ 0hZne:H.partitionZ d (1 / T) ≠ 0hZint:↑(1 / T) ∈ interior (H.ZComplexConvergenceDomain d)hZdiff:DifferentiableAt ℝ (H.partitionZ d) (1 / T)⊢ DifferentiableAt ℝ (fun T => Real.log (H.partitionZ d (1 / T))) T]
    fun_prop (disch := assumption)All goals completed! 🐙

--! Specializing to a system of particles in space

namespace NVEHamiltonian

Pressure, as a function of T. Defined as the conjugate variable to volume.

def pressure (T : ℝ) : ℝ :=
  let (n, V) := d;
  - deriv (fun V' ↦ helmholtzA H (n, V') T) V