diff --git a/QuantumInfo/ForMathlib.lean b/QuantumInfo/ForMathlib.lean
index 41867d407..45ab823dc 100644
--- a/QuantumInfo/ForMathlib.lean
+++ b/QuantumInfo/ForMathlib.lean
@@ -6,6 +6,7 @@ Authors: Alex Meiburg
 module
 
 public import QuantumInfo.ForMathlib.ContinuousLinearMap
+public import QuantumInfo.ForMathlib.ComplexLaplaceTransform
 public import QuantumInfo.ForMathlib.ContinuousSup
 public import QuantumInfo.ForMathlib.Filter
 public import QuantumInfo.ForMathlib.HermitianMat
diff --git a/QuantumInfo/ForMathlib/ComplexLaplaceTransform.lean b/QuantumInfo/ForMathlib/ComplexLaplaceTransform.lean
new file mode 100644
index 000000000..5676ae10e
--- /dev/null
+++ b/QuantumInfo/ForMathlib/ComplexLaplaceTransform.lean
@@ -0,0 +1,340 @@
+/-
+Copyright (c) 2025 Dennj Osele. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dennj Osele
+-/
+module
+
+public import Mathlib.Analysis.Complex.HasPrimitives
+public import Mathlib.Analysis.Complex.RealDeriv
+public import Mathlib.Analysis.SpecialFunctions.Log.Deriv
+public import Mathlib.Data.Real.StarOrdered
+public import Mathlib.MeasureTheory.Constructions.Pi
+public import Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
+public import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
+public import Mathlib.MeasureTheory.Integral.Bochner.Basic
+public import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
+public import Mathlib.MeasureTheory.Integral.Bochner.L1
+public import Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
+public import Mathlib.MeasureTheory.Integral.DominatedConvergence
+public import Mathlib.MeasureTheory.Measure.Prod
+public import Mathlib.MeasureTheory.Measure.Haar.OfBasis
+public import Mathlib.Order.CompletePartialOrder
+
+@[expose] public section
+
+noncomputable section
+
+/-- The integrand of the complex Laplace transform of a possibly infinite-valued energy function. -/
+def ComplexLaplaceIntegrand {α : Type*} (E : α → WithTop ℝ) (z : ℂ) (x : α) : ℂ :=
+  if h : E x = ⊤ then 0 else Complex.exp (-z * (E x).untop h : ℂ)
+
+/-- The complex Laplace transform of a possibly infinite-valued energy function. -/
+def ComplexLaplaceTransform {α : Type*} [MeasurableSpace α] [MeasureTheory.MeasureSpace α]
+    (E : α → WithTop ℝ) (z : ℂ) : ℂ :=
+  ∫ x, ComplexLaplaceIntegrand E z x
+
+/-- The complex convergence domain of a Laplace transform. -/
+def ComplexLaplaceConvergenceDomain {α : Type*} [MeasurableSpace α] [MeasureTheory.MeasureSpace α]
+    (E : α → WithTop ℝ) : Set ℂ :=
+  {z | MeasureTheory.Integrable (μ := MeasureTheory.volume) (ComplexLaplaceIntegrand E z)}
+
+/-- A two-sided exponential envelope controlling the Laplace integrand near `z`. -/
+private def ComplexLaplaceEnvelope {α : Type*} (E : α → WithTop ℝ) (z : ℂ) (δ : ℝ)
+    (x : α) : ℝ :=
+  ‖ComplexLaplaceIntegrand E (z - (δ : ℂ)) x‖ +
+    ‖ComplexLaplaceIntegrand E (z + (δ : ℂ)) x‖
+
+private def ComplexLaplaceEndpointEnvelope {α : Type*} (E : α → WithTop ℝ) (z w : ℂ)
+    (x : α) : ℝ :=
+  ‖ComplexLaplaceIntegrand E z x‖ + ‖ComplexLaplaceIntegrand E w x‖
+
+private theorem norm_complexLaplaceIntegrand_le_envelope
+    {α : Type*} {E : α → WithTop ℝ} {z w : ℂ} {δ : ℝ}
+    (hw : w ∈ Metric.closedBall z δ) (x : α) :
+    ‖ComplexLaplaceIntegrand E w x‖ ≤ ComplexLaplaceEnvelope E z δ x := by
+  unfold ComplexLaplaceEnvelope ComplexLaplaceIntegrand
+  by_cases h : E x = ⊤
+  · simp [h]
+  · simp only [h, dite_false]
+    set e : ℝ := (E x).untop h
+    have hdist : ‖w - z‖ ≤ δ := by
+      simpa [Metric.mem_closedBall, dist_eq_norm, norm_sub_rev] using hw
+    have hre_abs : |w.re - z.re| ≤ δ := by
+      exact (Complex.abs_re_le_norm (w - z)).trans (by simpa [Complex.sub_re] using hdist)
+    rw [Complex.norm_exp, Complex.norm_exp, Complex.norm_exp]
+    rcases le_total 0 e with he | he
+    · refine le_add_of_le_of_nonneg ?_ (Real.exp_pos _).le
+      exact Real.exp_le_exp.mpr (by
+        simp only [neg_mul, Complex.mul_re, Complex.neg_re, Complex.ofReal_re, Complex.ofReal_im,
+          mul_zero, sub_zero, Complex.sub_re]
+        nlinarith [abs_le.mp hre_abs |>.1])
+    · refine le_add_of_nonneg_of_le (Real.exp_pos _).le ?_
+      exact Real.exp_le_exp.mpr (by
+        simp only [neg_mul, Complex.mul_re, Complex.neg_re, Complex.ofReal_re, Complex.ofReal_im,
+          mul_zero, sub_zero, Complex.add_re]
+        nlinarith [abs_le.mp hre_abs |>.2])
+
+private theorem norm_complexLaplaceIntegrand_horizontal_le_endpointEnvelope
+    {α : Type*} {E : α → WithTop ℝ} {a b : ℂ} {t : ℝ}
+    (ht : t ∈ Set.uIcc a.re b.re) (x : α) :
+    ‖ComplexLaplaceIntegrand E (t + a.im * Complex.I) x‖ ≤
+      ComplexLaplaceEndpointEnvelope E a (b.re + a.im * Complex.I) x := by
+  unfold ComplexLaplaceEndpointEnvelope ComplexLaplaceIntegrand
+  by_cases h : E x = ⊤
+  · simp [h]
+  · simp only [h, dite_false]
+    set e : ℝ := (E x).untop h
+    rw [Complex.norm_exp, Complex.norm_exp, Complex.norm_exp]
+    rcases Set.mem_uIcc.mp ht with ⟨hat, htb⟩ | ⟨hbt, hta⟩ <;> rcases le_total 0 e with he | he
+    · refine le_add_of_le_of_nonneg ?_ (Real.exp_pos _).le
+      exact Real.exp_le_exp.mpr (by
+        simp only [neg_mul, Complex.mul_re, Complex.neg_re, Complex.ofReal_re, Complex.ofReal_im,
+          mul_zero, sub_zero, Complex.add_re, Complex.I_re]
+        nlinarith)
+    · refine le_add_of_nonneg_of_le (Real.exp_pos _).le ?_
+      exact Real.exp_le_exp.mpr (by
+        simp only [neg_mul, Complex.mul_re, Complex.neg_re, Complex.ofReal_re, Complex.ofReal_im,
+          mul_zero, sub_zero, Complex.add_re, Complex.I_re]
+        nlinarith)
+    · refine le_add_of_nonneg_of_le (Real.exp_pos _).le ?_
+      exact Real.exp_le_exp.mpr (by
+        simp only [neg_mul, Complex.mul_re, Complex.neg_re, Complex.ofReal_re, Complex.ofReal_im,
+          mul_zero, sub_zero, Complex.add_re, Complex.I_re]
+        nlinarith)
+    · refine le_add_of_le_of_nonneg ?_ (Real.exp_pos _).le
+      exact Real.exp_le_exp.mpr (by
+        simp only [neg_mul, Complex.mul_re, Complex.neg_re, Complex.ofReal_re, Complex.ofReal_im,
+          mul_zero, sub_zero, Complex.add_re, Complex.I_re]
+        nlinarith)
+
+private theorem norm_complexLaplaceIntegrand_vertical_le_endpointEnvelope
+    {α : Type*} {E : α → WithTop ℝ} {a b : ℂ} {t : ℝ}
+    (x : α) :
+    ‖ComplexLaplaceIntegrand E (b.re + t * Complex.I) x‖ ≤
+      ComplexLaplaceEndpointEnvelope E b (b.re + a.im * Complex.I) x := by
+  unfold ComplexLaplaceEndpointEnvelope ComplexLaplaceIntegrand
+  by_cases h : E x = ⊤
+  · simp [h]
+  · simp only [h, dite_false]
+    rw [Complex.norm_exp, Complex.norm_exp, Complex.norm_exp]
+    refine le_add_of_le_of_nonneg (le_of_eq ?_) (Real.exp_pos _).le
+    congr 1
+    simp only [neg_mul, Complex.mul_re, Complex.neg_re, Complex.ofReal_re, Complex.ofReal_im,
+      mul_zero, zero_mul, sub_zero, add_zero, Complex.add_re, Complex.I_re]
+
+/-- For each configuration, the complex Laplace integrand is analytic in the parameter. -/
+theorem analyticAt_complexLaplaceIntegrand
+    {α : Type*} (E : α → WithTop ℝ) (x : α) (z : ℂ) :
+    AnalyticAt ℂ (fun w : ℂ => ComplexLaplaceIntegrand E w x) z := by
+  unfold ComplexLaplaceIntegrand
+  split_ifs
+  · fun_prop
+  · fun_prop
+
+theorem measurable_complexLaplaceIntegrand
+    {α : Type*} [MeasurableSpace α] {E : α → WithTop ℝ} (hE : Measurable E) (z : ℂ) :
+    Measurable (ComplexLaplaceIntegrand E z) := by
+  rw [show ComplexLaplaceIntegrand E z =
+      fun x => if E x = ⊤ then 0 else Complex.exp (-z * (((E x).untopD 0 : ℝ) : ℂ)) by
+    funext x
+    unfold ComplexLaplaceIntegrand
+    by_cases hx : E x = ⊤
+    · simp [hx]
+    · simp only [hx, dite_false, ite_false]
+      congr 2
+      let y := E x
+      have hy : y ≠ ⊤ := by simpa [y] using hx
+      change ((y.untop hy : ℝ) : ℂ) = ((y.untopD 0 : ℝ) : ℂ)
+      obtain ⟨e, he⟩ := WithTop.ne_top_iff_exists.mp hy
+      have hUntop : y.untop hy = e := by
+        apply WithTop.coe_inj.mp
+        rw [WithTop.coe_untop, ← he]
+      have hUntopD : y.untopD 0 = e := by
+        rw [← he]
+        rfl
+      rw [hUntop, hUntopD]]
+  exact Measurable.ite (hE (measurableSet_singleton (⊤ : WithTop ℝ))) measurable_const
+    (Complex.continuous_exp.measurable.comp (by fun_prop :
+      Measurable fun x => -z * (((E x).untopD 0 : ℝ) : ℂ)))
+
+/-- Interior convergence gives integrability throughout a neighborhood of the parameter. -/
+theorem eventually_integrable_complexLaplaceIntegrand_of_mem_interior_convergenceDomain
+    {α : Type*} [MeasurableSpace α] [MeasureTheory.MeasureSpace α] {E : α → WithTop ℝ} {z : ℂ}
+    (hz : z ∈ interior (ComplexLaplaceConvergenceDomain E)) :
+    ∀ᶠ w in nhds z,
+      MeasureTheory.Integrable (μ := MeasureTheory.volume) (ComplexLaplaceIntegrand E w) :=
+  Filter.mem_of_superset (IsOpen.mem_nhds isOpen_interior hz) _root_.interior_subset
+
+theorem continuousAt_complexLaplaceTransform_of_mem_interior_convergenceDomain
+    {α : Type*} [MeasurableSpace α] [MeasureTheory.MeasureSpace α] {E : α → WithTop ℝ} {z : ℂ}
+    (hz : z ∈ interior (ComplexLaplaceConvergenceDomain E)) :
+    ContinuousAt (ComplexLaplaceTransform E) z := by
+  rcases Metric.isOpen_iff.mp isOpen_interior z hz with ⟨ε, hε_pos, hε⟩
+  have hint {w : ℂ} (hw : w ∈ Metric.ball z ε) :
+      MeasureTheory.Integrable (μ := MeasureTheory.volume) (ComplexLaplaceIntegrand E w) :=
+    _root_.interior_subset (s := ComplexLaplaceConvergenceDomain E) (hε hw)
+  have hbound_int : MeasureTheory.Integrable (μ := MeasureTheory.volume)
+      (ComplexLaplaceEnvelope E z (ε / 2)) := by
+    unfold ComplexLaplaceEnvelope
+    simpa [Pi.add_apply] using (hint (by
+      rw [Metric.mem_ball, dist_eq_norm]
+      simpa [abs_of_pos hε_pos] using show ε / 2 < ε by linarith)).norm.add (hint (by
+        rw [Metric.mem_ball, dist_eq_norm]
+        simpa [abs_of_pos hε_pos] using show ε / 2 < ε by linarith)).norm
+  simpa [ComplexLaplaceTransform] using
+    MeasureTheory.tendsto_integral_filter_of_dominated_convergence
+      (μ := MeasureTheory.volume) (l := nhds z)
+      (F := fun w x => ComplexLaplaceIntegrand E w x)
+      (f := fun x => ComplexLaplaceIntegrand E z x)
+      (ComplexLaplaceEnvelope E z (ε / 2))
+      ((eventually_integrable_complexLaplaceIntegrand_of_mem_interior_convergenceDomain (E := E) hz).mono
+        fun _ hw => hw.aestronglyMeasurable)
+      (Filter.Eventually.mono (Metric.ball_mem_nhds z (by positivity : 0 < ε / 2)) fun w hw =>
+        Filter.Eventually.of_forall fun x => norm_complexLaplaceIntegrand_le_envelope
+          (Metric.mem_closedBall.mpr (le_of_lt (Metric.mem_ball.mp hw))) x)
+      hbound_int
+      (Filter.Eventually.of_forall fun x => (analyticAt_complexLaplaceIntegrand E x z).continuousAt)
+
+theorem continuousOn_complexLaplaceTransform_interior_convergenceDomain
+    {α : Type*} [MeasurableSpace α] [MeasureTheory.MeasureSpace α] {E : α → WithTop ℝ} :
+    ContinuousOn (ComplexLaplaceTransform E) (interior (ComplexLaplaceConvergenceDomain E)) := by
+  intro z hz
+  exact (continuousAt_complexLaplaceTransform_of_mem_interior_convergenceDomain hz).continuousWithinAt
+
+private theorem integrable_uncurry_complexLaplaceIntegrand_horizontal
+    {α : Type*} [MeasureTheory.MeasureSpace α]
+    [MeasureTheory.SFinite (MeasureTheory.volume : MeasureTheory.Measure α)] {E : α → WithTop ℝ}
+    {a b : ℂ}
+    (hE : Measurable E)
+    (ha : MeasureTheory.Integrable (μ := MeasureTheory.volume) (ComplexLaplaceIntegrand E a))
+    (hb : MeasureTheory.Integrable (μ := MeasureTheory.volume)
+      (ComplexLaplaceIntegrand E (b.re + a.im * Complex.I))) :
+    MeasureTheory.Integrable
+      (Function.uncurry fun t : ℝ => fun x : α =>
+        ComplexLaplaceIntegrand E (t + a.im * Complex.I) x)
+      ((MeasureTheory.volume.restrict (Set.uIoc a.re b.re)).prod MeasureTheory.volume) := by
+  let μI := MeasureTheory.volume.restrict (Set.uIoc a.re b.re)
+  haveI : MeasureTheory.IsFiniteMeasure μI := ⟨by
+    rw [MeasureTheory.Measure.restrict_apply_univ]
+    simp [Set.uIoc]⟩
+  have hsm : MeasureTheory.StronglyMeasurable (Function.uncurry fun t : ℝ => fun x : α =>
+      ComplexLaplaceIntegrand E (t + a.im * Complex.I) x) := by
+    refine MeasureTheory.stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable ?_ ?_
+    · intro x
+      unfold ComplexLaplaceIntegrand
+      split_ifs <;> fun_prop
+    · intro t
+      exact (measurable_complexLaplaceIntegrand hE (t + a.im * Complex.I)).stronglyMeasurable
+  have henv : MeasureTheory.Integrable
+      (fun p : ℝ × α => ComplexLaplaceEndpointEnvelope E a (b.re + a.im * Complex.I) p.2)
+      (μI.prod MeasureTheory.volume) :=
+    (ha.norm.add hb.norm).comp_snd μI
+  refine henv.mono' hsm.aestronglyMeasurable ?_
+  simp only [Function.uncurry]
+  rw [MeasureTheory.Measure.ae_prod_iff_ae_ae (measurableSet_le
+    (show Measurable fun p : ℝ × α =>
+      ‖ComplexLaplaceIntegrand E (p.1 + a.im * Complex.I) p.2‖ from hsm.measurable.norm)
+    (show Measurable fun p : ℝ × α =>
+      ComplexLaplaceEndpointEnvelope E a (b.re + a.im * Complex.I) p.2 from
+        ((measurable_complexLaplaceIntegrand hE a).norm.add
+          (measurable_complexLaplaceIntegrand hE (b.re + a.im * Complex.I)).norm).comp measurable_snd))]
+  filter_upwards [MeasureTheory.ae_restrict_mem measurableSet_uIoc] with t ht
+  exact Filter.Eventually.of_forall fun x =>
+    norm_complexLaplaceIntegrand_horizontal_le_endpointEnvelope (Set.uIoc_subset_uIcc ht) x
+
+private theorem integrable_uncurry_complexLaplaceIntegrand_vertical
+    {α : Type*} [MeasureTheory.MeasureSpace α]
+    [MeasureTheory.SFinite (MeasureTheory.volume : MeasureTheory.Measure α)] {E : α → WithTop ℝ}
+    {a b : ℂ}
+    (hE : Measurable E)
+    (hb : MeasureTheory.Integrable (μ := MeasureTheory.volume) (ComplexLaplaceIntegrand E b))
+    (hba : MeasureTheory.Integrable (μ := MeasureTheory.volume)
+      (ComplexLaplaceIntegrand E (b.re + a.im * Complex.I))) :
+    MeasureTheory.Integrable
+      (Function.uncurry fun t : ℝ => fun x : α =>
+        ComplexLaplaceIntegrand E (b.re + t * Complex.I) x)
+      ((MeasureTheory.volume.restrict (Set.uIoc a.im b.im)).prod MeasureTheory.volume) := by
+  let μI := MeasureTheory.volume.restrict (Set.uIoc a.im b.im)
+  haveI : MeasureTheory.IsFiniteMeasure μI := ⟨by
+    rw [MeasureTheory.Measure.restrict_apply_univ]
+    simp [Set.uIoc]⟩
+  have hsm : MeasureTheory.StronglyMeasurable (Function.uncurry fun t : ℝ => fun x : α =>
+      ComplexLaplaceIntegrand E (b.re + t * Complex.I) x) := by
+    refine MeasureTheory.stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable ?_ ?_
+    · intro x
+      unfold ComplexLaplaceIntegrand
+      split_ifs <;> fun_prop
+    · intro t
+      exact (measurable_complexLaplaceIntegrand hE (b.re + t * Complex.I)).stronglyMeasurable
+  refine ((hb.norm.add hba.norm).comp_snd μI).mono'
+    hsm.aestronglyMeasurable ?_
+  exact Filter.Eventually.of_forall fun p =>
+    norm_complexLaplaceIntegrand_vertical_le_endpointEnvelope (a := a) (b := b) (t := p.1) p.2
+
+private theorem wedgeIntegral_complexLaplaceTransform_eq_integral
+    {α : Type*} [MeasureTheory.MeasureSpace α]
+    [MeasureTheory.SFinite (MeasureTheory.volume : MeasureTheory.Measure α)] {E : α → WithTop ℝ}
+    {a b : ℂ}
+    (hE : Measurable E)
+    (hab : Complex.Rectangle a b ⊆ interior (ComplexLaplaceConvergenceDomain E)) :
+    Complex.wedgeIntegral a b (ComplexLaplaceTransform E) =
+      ∫ x, Complex.wedgeIntegral a b (fun w : ℂ => ComplexLaplaceIntegrand E w x) := by
+  have hint {z : ℂ} (hz : z ∈ Complex.Rectangle a b) :
+      MeasureTheory.Integrable (μ := MeasureTheory.volume) (ComplexLaplaceIntegrand E z) :=
+    _root_.interior_subset (s := ComplexLaplaceConvergenceDomain E) (hab hz)
+  have ha : MeasureTheory.Integrable (μ := MeasureTheory.volume) (ComplexLaplaceIntegrand E a) :=
+    hint (by simp [Complex.Rectangle, Complex.mem_reProdIm])
+  have hb : MeasureTheory.Integrable (μ := MeasureTheory.volume) (ComplexLaplaceIntegrand E b) :=
+    hint (by simp [Complex.Rectangle, Complex.mem_reProdIm])
+  have hcorner : MeasureTheory.Integrable (μ := MeasureTheory.volume)
+      (ComplexLaplaceIntegrand E (b.re + a.im * Complex.I)) :=
+    hint (by simp [Complex.Rectangle, Complex.mem_reProdIm])
+  have hH := MeasureTheory.intervalIntegral_integral_swap
+    (μ := MeasureTheory.volume)
+    (f := fun t x => ComplexLaplaceIntegrand E (t + a.im * Complex.I) x)
+    (integrable_uncurry_complexLaplaceIntegrand_horizontal hE ha hcorner)
+  have hV := MeasureTheory.intervalIntegral_integral_swap
+    (μ := MeasureTheory.volume)
+    (f := fun t x => ComplexLaplaceIntegrand E (b.re + t * Complex.I) x)
+    (integrable_uncurry_complexLaplaceIntegrand_vertical hE hb hcorner)
+  simp only [Complex.wedgeIntegral, ComplexLaplaceTransform]
+  rw [hH, hV]
+  rw [← MeasureTheory.integral_smul, ← MeasureTheory.integral_add]
+  · rcases le_total a.re b.re with hab | hba
+    · simpa [intervalIntegral.integral_of_le hab, Function.uncurry, Set.uIoc_of_le hab]
+        using (integrable_uncurry_complexLaplaceIntegrand_horizontal hE ha hcorner).integral_prod_right
+    · simpa [intervalIntegral.integral_of_ge hba, Function.uncurry, Set.uIoc_of_ge hba]
+        using (integrable_uncurry_complexLaplaceIntegrand_horizontal hE ha hcorner).integral_prod_right.neg
+  · refine (?_ : MeasureTheory.Integrable _ MeasureTheory.volume).smul Complex.I
+    rcases le_total a.im b.im with hab | hba
+    · simpa [intervalIntegral.integral_of_le hab, Function.uncurry, Set.uIoc_of_le hab]
+        using (integrable_uncurry_complexLaplaceIntegrand_vertical hE hb hcorner).integral_prod_right
+    · simpa [intervalIntegral.integral_of_ge hba, Function.uncurry, Set.uIoc_of_ge hba]
+        using (integrable_uncurry_complexLaplaceIntegrand_vertical hE hb hcorner).integral_prod_right.neg
+
+/-- A complex Laplace transform is analytic on the interior of its convergence domain. -/
+theorem analyticAt_complexLaplaceTransform_of_mem_interior_convergenceDomain
+    {α : Type*} [MeasureTheory.MeasureSpace α]
+    [MeasureTheory.SFinite (MeasureTheory.volume : MeasureTheory.Measure α)] {E : α → WithTop ℝ} {z : ℂ}
+    (hE : Measurable E)
+    (hz : z ∈ interior (ComplexLaplaceConvergenceDomain E)) :
+    AnalyticAt ℂ (ComplexLaplaceTransform E) z := by
+  rcases Metric.isOpen_iff.mp isOpen_interior z hz with ⟨r, hr_pos, hr⟩
+  have hcons : Complex.IsConservativeOn (ComplexLaplaceTransform E) (Metric.ball z r) := by
+    intro a b hab
+    rw [wedgeIntegral_complexLaplaceTransform_eq_integral hE (hab.trans hr),
+      wedgeIntegral_complexLaplaceTransform_eq_integral hE (by
+        simpa [Complex.Rectangle, Set.uIcc_comm] using hab.trans hr)]
+    · rw [← MeasureTheory.integral_neg]
+      apply MeasureTheory.integral_congr_ae
+      filter_upwards with x
+      exact (DifferentiableOn.isConservativeOn
+        (fun y _hy => (analyticAt_complexLaplaceIntegrand E x y).differentiableAt.differentiableWithinAt))
+        a b (Set.subset_univ _)
+  exact ((Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn Metric.isOpen_ball).1
+    ⟨hcons, continuousOn_complexLaplaceTransform_interior_convergenceDomain.mono hr⟩).analyticAt
+      (Metric.ball_mem_nhds z hr_pos)
+
+
+end
diff --git a/QuantumInfo/StatMech/Hamiltonian.lean b/QuantumInfo/StatMech/Hamiltonian.lean
index 28213a86f..8b4633f69 100644
--- a/QuantumInfo/StatMech/Hamiltonian.lean
+++ b/QuantumInfo/StatMech/Hamiltonian.lean
@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Data.Fintype.Defs
 public import Mathlib.Data.Real.Basic
+public import Mathlib.MeasureTheory.Constructions.BorelSpace.Real
+public import Mathlib.MeasureTheory.Constructions.Pi
+public import Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
 
 @[expose] public section
 
@@ -27,6 +30,8 @@ structure MicroHamiltonian (D : Type) where
   [dim_fin : ∀ d, Fintype (dim d)]
   --Given the configuration, what is its energy?
   H : {d : D} → (dim d → ℝ) → WithTop ℝ
+  --The energy function must be measurable (else the partition function integral is meaningless).
+  measurable_H : ∀ d, Measurable (@H d)
 
 /-- We add the dim_fin to the instance cache so that things like the measure can be synthesized -/
 instance microHamiltonianFintype (H : MicroHamiltonian D) (d : D) : Fintype (H.dim d) :=
diff --git a/QuantumInfo/StatMech/IdealGas.lean b/QuantumInfo/StatMech/IdealGas.lean
index 9128f61a9..f20d85740 100644
--- a/QuantumInfo/StatMech/IdealGas.lean
+++ b/QuantumInfo/StatMech/IdealGas.lean
@@ -27,6 +27,23 @@ def IdealGas : NVEHamiltonian where
       ∑ (i : Fin n) (ax : Fin 3), config (i,.inr ax)^2 / (2 : ℝ)
     else
       ⊤
+  measurable_H := by
+    rintro ⟨n, V⟩
+    dsimp
+    refine Measurable.ite ?_ ?_ measurable_const
+    · rw [Set.setOf_forall]
+      apply MeasurableSet.iInter
+      intro i
+      rw [Set.setOf_forall]
+      exact MeasurableSet.iInter fun ax => measurableSet_le
+        (show Measurable fun config : Fin n × (Fin 3 ⊕ Fin 3) → ℝ =>
+          |config (i, Sum.inl ax)| by fun_prop) measurable_const
+    · convert WithTop.isOpenEmbedding_coe.measurableEmbedding.measurable.comp
+        (Finset.measurable_sum _ fun (x : Fin n × Fin 3) _ => (show Measurable fun config : Fin n × (Fin 3 ⊕ Fin 3) → ℝ =>
+          config (x.1, Sum.inr x.2) ^ 2 / (2 : ℝ) by fun_prop)) using 1
+      ext config
+      rw [← WithTop.coe_sum]
+      rfl
 
 namespace IdealGas
 open MicroHamiltonian
diff --git a/QuantumInfo/StatMech/ThermoQuantities.lean b/QuantumInfo/StatMech/ThermoQuantities.lean
index e8e3a70fe..4b9e00618 100644
--- a/QuantumInfo/StatMech/ThermoQuantities.lean
+++ b/QuantumInfo/StatMech/ThermoQuantities.lean
@@ -6,12 +6,20 @@ Authors: Alex Meiburg
 module
 
 public import QuantumInfo.StatMech.Hamiltonian
+public import QuantumInfo.ForMathlib.ComplexLaplaceTransform
+public import Mathlib.Analysis.Complex.HasPrimitives
+public import Mathlib.Analysis.Complex.RealDeriv
 public import Mathlib.Analysis.SpecialFunctions.Log.Deriv
 public import Mathlib.Data.Real.StarOrdered
 public import Mathlib.MeasureTheory.Constructions.Pi
+public import Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
+public import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
 public import Mathlib.MeasureTheory.Integral.Bochner.Basic
+public import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
 public import Mathlib.MeasureTheory.Integral.Bochner.L1
 public import Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
+public import Mathlib.MeasureTheory.Integral.DominatedConvergence
+public import Mathlib.MeasureTheory.Measure.Prod
 public import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 public import Mathlib.Order.CompletePartialOrder
 
@@ -32,6 +40,48 @@ def PartitionZ (β : ℝ) : ℝ :=
     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 := by
+  have hInt : MeasureTheory.Integrable (μ := MeasureTheory.volume)
+      (ComplexLaplaceIntegrand (fun config : H.dim d → ℝ => H.H config) (β : ℂ)) := hβ
+  rw [PartitionZ, PartitionZComplex, ComplexLaplaceTransform]
+  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) := by
+      apply MeasureTheory.integral_congr_ae
+      filter_upwards with config
+      unfold ComplexLaplaceIntegrand
+      by_cases h : H.H config = ⊤
+      · simp [h]
+      · simp only [h, dite_false]
+        set e : ℝ := (H.H config).untop h
+        simpa [Complex.ofReal_mul] using (Complex.exp_ofReal_re (-(β * e))).symm
+    _ = RCLike.re (∫ x, ComplexLaplaceIntegrand
+        (fun config : H.dim d → ℝ => H.H config) (β : ℂ) x) := integral_re hInt
+
+open scoped ContDiff Topology in
+theorem contDiffAt_partitionZ_of_mem_interior_convergenceDomain {β : ℝ}
+    (hβ : (β : ℂ) ∈ interior (H.ZComplexConvergenceDomain d)) :
+    ContDiffAt ℝ ⊤ (H.PartitionZ d) β := by
+  refine (analyticAt_complexLaplaceTransform_of_mem_interior_convergenceDomain
+    (E := fun config : H.dim d → ℝ => H.H config) (H.measurable_H d) hβ).contDiffAt
+    |>.real_of_complex |>.congr_of_eventuallyEq ?_
+  filter_upwards [(Complex.continuous_ofReal.tendsto β).eventually
+    (IsOpen.mem_nhds isOpen_interior hβ)] with x hx
+  exact H.partitionZ_eq_re_partitionZComplex d (_root_.interior_subset hx)
+
 /-- The partition function as a function of temperature T instead of β. -/
 def PartitionZT (T : ℝ) : ℝ :=
   PartitionZ H d (1/T)
@@ -85,66 +135,73 @@ so this will be differentiable if
 is, aka if the Laplace transform is differentiable.
 See e.g. https://math.stackexchange.com/q/84382/127777
 For this we really want the fact that the Laplace transform is analytic wherever it's absolutely convergent,
-which is (as Wikipedia informs) an easy consequence of Fubini's theorem + Morera's theorem. However, Morera's
-theorem isn't in mathlib yet. So this is a sorry for now
+which follows from the local domination estimate above, Fubini's theorem, and Morera's theorem.
 -/
-open scoped ContDiff in
-theorem DifferentiableAt_Z_if_ZIntegrable {β : ℝ} (h : H.ZIntegrable d β) : ContDiffAt ℝ ω (H.PartitionZ d) β :=
-  sorry
-
-/-- The two definitions of entropy, in terms of T or β, are equivalent. -/
-theorem entropy_A_eq_entropy_Z (T β : ℝ) (hβT : T * β = 1) (hi : H.ZIntegrable d β)
-    : EntropyS H d T = EntropySβ H d β := by
-  have hTnz : T ≠ 0 := left_ne_zero_of_mul_eq_one hβT
-  have hβnz : β ≠ 0 := right_ne_zero_of_mul_eq_one hβT
-  have hβT' := eq_one_div_of_mul_eq_one_right hβT
+/-- 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) := by
+  have hZdiff : DifferentiableAt ℝ (H.PartitionZ d) (1 / T) :=
+    (H.contDiffAt_partitionZ_of_mem_interior_convergenceDomain d hZint).differentiableAt
+      (by simp)
   dsimp [EntropyS, EntropySβ, InternalU, PartitionZT]
   unfold HelmholtzA
   erw [deriv_mul]
   rw [deriv_neg'', neg_mul, one_mul, neg_add_rev, neg_neg, mul_neg, add_comm]
   congr 1
-  · rw [PartitionZT, hβT']
   simp_rw [PartitionZT]
   have hdc := deriv_comp (h := fun T ↦ T⁻¹) (h₂ := fun β => Real.log (H.PartitionZ d β)) T ?_ ?_
   unfold Function.comp at hdc
-  simp only [hdc, one_div, deriv_inv', mul_neg, neg_inj, hβT']
+  simp only [hdc, one_div, deriv_inv', mul_neg, neg_inj]
   field_simp
   ring_nf
   --Show the differentiability side-goals
-  · rw [← one_div, ← hβT']
-    have h₁ := hi.2
-    have := (DifferentiableAt_Z_if_ZIntegrable hi).differentiableAt WithTop.top_ne_zero
+  · rw [← one_div]
     fun_prop (disch := assumption)
   · fun_prop (disch := assumption)
   · fun_prop
   · simp_rw [PartitionZT]
-    rw [hβT'] at hi
-    have := hi.2
-    have := (DifferentiableAt_Z_if_ZIntegrable hi).differentiableAt WithTop.top_ne_zero
     fun_prop (disch := assumption)
 
+
 set_option backward.isDefEq.respectTransparency false in
+open scoped ContDiff in
 /--
 The "definition of temperature from entropy":
 1/T = (∂S/∂U), when the derivative is at constant extrinsic d (typically N/V).
 Here we use β instead of 1/T on the left, and express the right actually as (∂S/∂β)/(∂U/∂β),
 as all our things are ultimately parameterized by β.
+
+This identity requires the denominator `∂U/∂β` to be nonzero.
 -/
-theorem β_eq_deriv_S_U {β : ℝ} (hi : H.ZIntegrable d β) : β = (deriv (H.EntropySβ d) β) / deriv (H.InternalU d) β := by
+theorem β_eq_deriv_S_U {β : ℝ}
+    (hZne : H.PartitionZ d β ≠ 0)
+    (hZint : (β : ℂ) ∈ interior (H.ZComplexConvergenceDomain d))
+    (hU' : deriv (H.InternalU d) β ≠ 0) :
+    β = (deriv (H.EntropySβ d) β) / deriv (H.InternalU d) β := by
+  have hZ : ContDiffAt ℝ ⊤ (H.PartitionZ d) β :=
+    H.contDiffAt_partitionZ_of_mem_interior_convergenceDomain d hZint
   unfold EntropySβ
   unfold InternalU
 
   --Show the differentiability side-goals
-  have : DifferentiableAt ℝ (fun β => Real.log (H.PartitionZ d β)) β := by
-    have := hi.2
-    have := (DifferentiableAt_Z_if_ZIntegrable hi).differentiableAt WithTop.top_ne_zero
+  have hlogDiff : DifferentiableAt ℝ (fun β => Real.log (H.PartitionZ d β)) β := by
+    have := hZne
+    have := hZ.differentiableAt (by simp)
     fun_prop (disch := assumption)
-  have : DifferentiableAt ℝ (deriv fun β => Real.log (H.PartitionZ d β)) β := by
-    have this := (DifferentiableAt_Z_if_ZIntegrable hi).log hi.2
+  have hlogDerivDiff : DifferentiableAt ℝ (deriv fun β => Real.log (H.PartitionZ d β)) β := by
+    have this := hZ.log hZne
     replace this :=
-      (this.fderiv_right (m := ⊤) (OrderTop.le_top _)).differentiableAt WithTop.top_ne_zero
+      (this.fderiv_right (m := ⊤) (OrderTop.le_top _)).differentiableAt (by simp)
     unfold deriv
     fun_prop
+  have hderiv : deriv (deriv fun β => Real.log (H.PartitionZ d β)) β ≠ 0 := by
+    intro hzero
+    apply hU'
+    change deriv (-fun β => deriv (fun β' => Real.log (H.PartitionZ d β')) β) β = 0
+    rw [deriv.neg]
+    simp [hzero]
 
   --Main goal
   simp only [mul_neg]
@@ -152,19 +209,17 @@ theorem β_eq_deriv_S_U {β : ℝ} (hi : H.ZIntegrable d β) : β = (deriv (H.En
   dsimp
   erw [deriv_mul]
   simp only [deriv_id'', one_mul, neg_add_rev, add_neg_cancel_comm_assoc, neg_div_neg_eq]
-  have : deriv (deriv fun β => Real.log (H.PartitionZ d β)) β ≠ 0 := ?_
-  exact (mul_div_cancel_right₀ β this).symm
+  exact (mul_div_cancel_right₀ β hderiv).symm
   --Discharge those side-goals
-  · sorry
-  · fun_prop (disch := assumption)
-  · fun_prop (disch := assumption)
+  · exact differentiableAt_id
+  · exact hlogDerivDiff
   · fun_prop (disch := assumption)
   · fun_prop (disch := assumption)
 
 set_option backward.isDefEq.respectTransparency false in
 open scoped ContDiff in
-example (x : ℝ) (f : ℝ → ℝ) (hf : ContDiffAt ℝ ω f x) : DifferentiableAt ℝ (deriv f) x := by
-  have := (hf.fderiv_right (m := ⊤) (OrderTop.le_top _)).differentiableAt WithTop.top_ne_zero
+example (x : ℝ) (f : ℝ → ℝ) (hf : ContDiffAt ℝ ⊤ f x) : DifferentiableAt ℝ (deriv f) x := by
+  have := (hf.fderiv_right (m := ⊤) (OrderTop.le_top _)).differentiableAt (by simp)
   unfold deriv
   fun_prop